Fix trivial identity (0 => Exp) == 1, and add rewritings for =>.

The new rewriting are (Exp => Exp) = 1, (Exp <=> Exp) == 1,
and (Exp ^ Exp) == 0.

* src/ltlast/binop.hh: Fix documentation.
* src/ltlast/binop.cc: Fix implementation.
* src/ltltest/equals.test: More tests.
* src/tgbatest/emptchk.test: Remove a useless test.

src/ltlast/binop.cc

@@ -158,6 +158,12 @@ namespace spot
 	    return unop::instance(unop::Not, second);
 	  if (first == constant::false_instance())
 	    return second;
+	  if (first == second)
+	    {
+	      first->destroy();
+	      second->destroy();
+	      return constant::false_instance();
+	    }
 	  // We expect constants to appear first, because they are
 	  // instantiated first.
 	  assert(second != constant::false_instance());
@@ -172,10 +178,17 @@ namespace spot
 	  }
 	  //   - (0 <=> Exp) = !Exp
 	  //   - (1 <=> Exp) = Exp
+	  //   - (Exp <=> Exp) = 1
 	  if (first == constant::false_instance())
 	    return unop::instance(unop::Not, second);
 	  if (first == constant::true_instance())
 	    return second;
+	  if (first == second)
+	    {
+	      first->destroy();
+	      second->destroy();
+	      return constant::true_instance();
+	    }
 	  // We expect constants to appear first, because they are
 	  // instantiated first.
 	  assert(second != constant::false_instance());
@@ -183,15 +196,16 @@ namespace spot
 	  break;
 	case Implies:
 	  //   - (1 => Exp) = Exp
-	  //   - (0 => Exp) = 0
+	  //   - (0 => Exp) = 1
 	  //   - (Exp => 1) = 1
 	  //   - (Exp => 0) = !Exp
+	  //   - (Exp => Exp) = 1
 	  if (first == constant::true_instance())
 	    return second;
 	  if (first == constant::false_instance())
 	    {
 	      second->destroy();
-	      return first;
+	      return constant::true_instance();
 	    }
 	  if (second == constant::true_instance())
 	    {
@@ -200,6 +214,12 @@ namespace spot
 	    }
 	  if (second == constant::false_instance())
 	    return unop::instance(unop::Not, first);
+	  if (first == second)
+	    {
+	      first->destroy();
+	      second->destroy();
+	      return constant::true_instance();
+	    }
 	  break;
 	case U:
 	  //   - (Exp U 1) = 1

src/ltlast/binop.hh

@@ -70,13 +70,16 @@ namespace spot
       /// performed (the left formula is rewritten as the right
       /// formula):
       ///   - (1 => Exp) = Exp
-      ///   - (0 => Exp) = 0
+      ///   - (0 => Exp) = 1
       ///   - (Exp => 1) = 1
       ///   - (Exp => 0) = !Exp
+      ///   - (Exp => Exp) = 1
       ///   - (1 ^ Exp) = !Exp
       ///   - (0 ^ Exp) = Exp
+      ///   - (Exp ^ Exp) = 0
       ///   - (0 <=> Exp) = !Exp
       ///   - (1 <=> Exp) = Exp
+      ///   - (Exp <=> Exp) = Exp
       ///   - (Exp U 1) = 1
       ///   - (Exp U 0) = 0
       ///   - (0 U Exp) = Exp

src/ltltest/equals.test

@@ -88,13 +88,16 @@ run 0 ../equals '!0' '1'
 run 0 ../equals '!!Exp' 'Exp'
 
 run 0 ../equals '(1 => Exp)' 'Exp'
-run 0 ../equals '(0 => Exp)' '0'
+run 0 ../equals '(0 => Exp)' '1'
 run 0 ../equals '(Exp => 1)' '1'
 run 0 ../equals '(Exp => 0)' '!Exp'
+run 0 ../equals '(Exp => Exp)' '1'
 run 0 ../equals '(1 ^ Exp)' '!Exp'
 run 0 ../equals '(0 ^ Exp)' 'Exp'
+run 0 ../equals '(Exp ^ Exp)' '0'
 run 0 ../equals '(0 <=> Exp)' '!Exp'
 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 '(Exp R 1)' '1'

src/tgbatest/emptchk.test

@@ -96,6 +96,5 @@ expect_ce 'Fa & Xb & GFc & Gd' 1
 expect_ce 'Fa & Xa & GFc & Gc' 2
 expect_ce 'Fc & X(a | Xb) & GF(a | Xb) & Gc' 1
 expect_ce '!((FF a) <=> (F x))' 3
-expect_no '!((FF a) <=> (F a))' 3
 expect_no 'Xa && (!a U b) && !b && X!b' 4
 expect_no '(a U !b) && Gb' 3