Simplify fUf, fRf, fWf, and fRF as f.

* src/ltlast/binop.cc (binop::instance): Simplify fUf, fRf, fWf,
and fRF.
* src/ltlast/binop.hh: Document it.
* src/ltltest/equals.test: Add new tests for 'Exp U Exp'
and 'Exp R Exp', and all missing tests for W and M.

src/ltlast/binop.cc

@@ -225,9 +225,11 @@ namespace spot
 	  //   - (Exp U 1) = 1
 	  //   - (Exp U 0) = 0
 	  //   - (0 U Exp) = Exp
+	  //   - (Exp U Exp) = Exp
 	  if (second == constant::true_instance()
 	      || second == constant::false_instance()
-	      || first == constant::false_instance())
+	      || first == constant::false_instance()
+	      || first == second)
 	    {
 	      first->destroy();
 	      return second;
@@ -237,8 +239,10 @@ namespace spot
 	  //   - (Exp W 1) = 1
 	  //   - (0 W Exp) = Exp
 	  //   - (1 W Exp) = 1
+	  //   - (Exp W Exp) = Exp
 	  if (second == constant::true_instance()
-	      || first == constant::false_instance())
+	      || first == constant::false_instance()
+	      || first == second)
 	    {
 	      first->destroy();
 	      return second;
@@ -253,9 +257,11 @@ namespace spot
 	  //   - (Exp R 1) = 1
 	  //   - (Exp R 0) = 0
 	  //   - (1 R Exp) = Exp
+	  //   - (Exp R Exp) = Exp
 	  if (second == constant::true_instance()
 	      || second == constant::false_instance()
-	      || first == constant::true_instance())
+	      || first == constant::true_instance()
+	      || first == second)
 	    {
 	      first->destroy();
 	      return second;
@@ -265,8 +271,10 @@ namespace spot
 	  //   - (Exp M 0) = 0
 	  //   - (1 M Exp) = Exp
 	  //   - (0 M Exp) = 0
+	  //   - (Exp M Exp) = Exp
 	  if (second == constant::false_instance()
-	      || first == constant::true_instance())
+	      || first == constant::true_instance()
+	      || first == second)
 	    {
 	      first->destroy();
 	      return second;

src/ltlast/binop.hh

@@ -83,15 +83,19 @@ namespace spot
       ///   - (Exp U 1) = 1
       ///   - (Exp U 0) = 0
       ///   - (0 U Exp) = Exp
+      ///   - (Exp U Exp) = Exp
       ///   - (Exp W 1) = 1
       ///   - (0 W Exp) = Exp
       ///   - (1 W Exp) = 1
+      ///   - (Exp W Exp) = Exp
       ///   - (Exp R 1) = 1
       ///   - (Exp R 0) = 0
       ///   - (1 R Exp) = Exp
+      ///   - (Exp R Exp) = Exp
       ///   - (Exp M 0) = 0
       ///   - (1 M Exp) = Exp
       ///   - (0 M Exp) = 0
+      ///   - (Exp M Exp) = Exp
       static formula* instance(type op, formula* first, formula* second);
 
       virtual void accept(visitor& v);

src/ltltest/equals.test

@@ -100,9 +100,20 @@ run 0 ../equals '(1 <=> Exp)' 'Exp'
 run 0 ../equals '(Exp <=> Exp)' '1'
 run 0 ../equals '(Exp U 1)' '1'
 run 0 ../equals '(Exp U 0)' '0'
+run 0 ../equals '(0 U Exp)' 'Exp'
+run 0 ../equals '(Exp U Exp)' 'Exp'
 run 0 ../equals '(Exp R 1)' '1'
 run 0 ../equals '(Exp R 0)' '0'
+run 0 ../equals '(Exp R Exp)' 'Exp'
 run 0 ../equals '(1 R Exp)' 'Exp'
+run 0 ../equals '(Exp W 1)' '1'
+run 0 ../equals '(0 W Exp)' 'Exp'
+run 0 ../equals '(1 W Exp)' '1'
+run 0 ../equals '(Exp W Exp)' 'Exp'
+run 0 ../equals '(Exp M 0)' '0'
+run 0 ../equals '(1 M Exp)' 'Exp'
+run 0 ../equals '(0 M Exp)' '0'
+run 0 ../equals '(Exp M Exp)' 'Exp'
 
 run 0 ../equals FFx Fx
 run 0 ../equals FFFFFx Fx