From 1671aa5da1789bcd197bf1fad9502d7cdf94f045 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Mon, 25 Oct 2010 17:46:26 +0200
Subject: [PATCH] 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     | 16 ++++++++++++----
 src/ltlast/binop.hh     |  4 ++++
 src/ltltest/equals.test | 11 +++++++++++
 3 files changed, 27 insertions(+), 4 deletions(-)

diff --git a/src/ltlast/binop.cc b/src/ltlast/binop.cc
index 1222e8820..b2c8391d8 100644
--- a/src/ltlast/binop.cc
+++ b/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;
diff --git a/src/ltlast/binop.hh b/src/ltlast/binop.hh
index d9e87a5b3..12b36cabc 100644
--- a/src/ltlast/binop.hh
+++ b/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);
diff --git a/src/ltltest/equals.test b/src/ltltest/equals.test
index 9e5118241..006df3f4b 100755
--- a/src/ltltest/equals.test
+++ b/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