Combine Boolean formulae in Fusion arguments.

* src/ltlast/multop.cc (multop::instance): Implement
the rewriting.   "a🅱️c[*]:d:e" becomes "{{a&&b}&c[*]}:{d&&e}".
* src/ltlast/multop.hh: Document it.
* src/ltltest/equals.test, src/ltltest/kind.test: Add test cases.

src/ltlast/multop.cc

@@ -271,6 +271,41 @@ namespace spot
 	  abs = constant::false_instance();
 	  abs2 = constant::empty_word_instance();
 	  weak_abs = 0;
+
+	  // Make a first pass to gather Boolean formulae.
+	  // - Fusion(Exps1...,BoolExp1...BoolExpN,Exps2,Exps3...) =
+	  //   Fusion(Exps1...,AndNLM(And(BoolExp1...BoolExpN),Exps2),Exps3...)
+	  {
+	    vec* b = 0;
+	    vec::iterator i = v->begin();
+	    while (i != v->end())
+	      {
+		if ((*i)->is_boolean())
+		  {
+		    if (!b)
+		      b = new vec;
+		    b->push_back(*i);
+		    i = v->erase(i);
+		  }
+		else
+		  {
+		    if (b)
+		      {
+			// We have found a non-Boolean Exp.  "AndNLM" it
+			// with all the previous Boolean formulae.
+			*i = instance(AndNLM, instance(And, b), *i);
+			b = 0;
+		      }
+		    ++i;
+		  }
+	      }
+	    if (b)
+	      {
+		// Group all trailing Boolean formulae.
+		v->push_back(instance(And, b));
+	      }
+	  }
+
 	  break;
 
 	default:

src/ltlast/multop.hh

@@ -101,6 +101,8 @@ namespace spot
       /// - Fusion(Exps1...,0,Exps2...) = 0
       /// - Fusion(Exps1...,[*0],Exps2...) = 0
       /// - Fusion(Exp) = Exp
+      /// - Fusion(Exps1...,BoolExp1...BoolExpN,Exps2,Exps3...) =
+      ///     Fusion(Exps1...,AndNLM(And(BoolExp1...BoolExpN),Exps2),Exps3...)
       static formula* instance(type op, vec* v);
 
       virtual void accept(visitor& v);

src/ltltest/equals.test

@@ -50,10 +50,6 @@ run 0 ../equals 'a & a & true' 'a'
 run 0 ../equals 'a & false & a' 'false'
 run 0 ../equals 'a | false | a' 'a'
 run 0 ../equals 'true | a | a' 'true'
-run 0 ../equals '{a*}!' '{a*}<>->1'
-run 0 ../equals '{a -> b} (c)' '(a->b)->c'
-run 0 ../equals '{a & !b}!' 'a & !b'
-run 0 ../equals '{a;[*0]}|->!Xb' 'a -> !Xb'
 
 # other formulae which are not
 run 1 ../equals 'a' 'b'
@@ -144,6 +140,13 @@ run 0 ../equals '{x;x}[]->GX(1)' '1'
 run 0 ../equals '{x;x}[]->FF(0)' '{x;x}[]->0'
 run 0 ../equals '{x;x}[]->y' '{x;x}|->y'
 run 0 ../equals '{x;x}[]->y' '{x;x}(y)'
+run 0 ../equals '{a*}!' '{a*}<>->1'
+run 0 ../equals '{a -> b} (c)' '(a->b)->c'
+run 0 ../equals '{a & !b}!' 'a & !b'
+run 0 ../equals '{a;[*0]}|->!Xb' 'a -> !Xb'
+run 0 ../equals '{{a;b}:b:c:d*:e:f}!' '{{a;b}:{{b && c } & d[*]}:{e && f}}!'
+run 0 ../equals '{a:b:c}|->!Xb' '(a&b&c) -> !Xb'
+run 0 ../equals '{a:b:c*}|->!Xb' '{(a&&b)&c*}|-> !Xb'
 
 run 0 ../equals '{a[*0]}' '{[*0]}'
 run 0 ../equals '{a[*..]}' '{a[*]}'

src/ltltest/kind.test

@@ -53,6 +53,8 @@ check '{a;b}|->!Xb' '&fP'
 check '{a;b}|->X!b' '&!fP'
 check '{a;b}|->!Gb' '&xP'
 check '{a;b}|->F!b' '&!xP'
+check '{a:b:c:d}!' 'B&!xfLEPS'  # Equivalent to a&b&c&d
+check 'a&b&c&d'    'B&!xfLEPS'
 
 run 0 ../consterm '1'
 run 0 ../consterm '0'