From 76528ee2fb5726cfe0455154b93cacde6a95f1be Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Mon, 8 Feb 2010 18:00:24 +0100
Subject: [PATCH] Simplify {#e}[]->Exp and {#e}<>->Exp.

* src/ltlast/binop.cc: Add simplification rules.
---
 src/ltlast/binop.cc | 14 +++++++++-----
 1 file changed, 9 insertions(+), 5 deletions(-)

diff --git a/src/ltlast/binop.cc b/src/ltlast/binop.cc
index fe89c9ea2..770fd920e 100644
--- a/src/ltlast/binop.cc
+++ b/src/ltlast/binop.cc
@@ -258,13 +258,15 @@ namespace spot
 	case EConcat:
 	  //   - 0 <>-> Exp = 0
 	  //   - 1 <>-> Exp = Exp
+	  //   - #e <>-> Exp = 0
 	  //   - Exp <>-> 0 = 0
 	  if (first == constant::true_instance())
 	    return second;
-	  if (first == constant::false_instance())
+	  if (first == constant::false_instance()
+	      || first == constant::empty_word_instance())
 	    {
 	      second->destroy();
-	      return first;
+	      return constant::false_instance();
 	    }
 	  if (second == constant::false_instance())
 	    {
@@ -275,13 +277,15 @@ namespace spot
 	case UConcat:
 	  //   - 0 []-> Exp = 1
 	  //   - 1 []-> Exp = Exp
+	  //   - #e []-> Exp = 1
 	  //   - Exp []-> 1 = 1
-	  if (first == constant::false_instance())
-	    return constant::true_instance();
 	  if (first == constant::true_instance())
+	    return second;
+	  if (first == constant::false_instance()
+	      || first == constant::empty_word_instance())
 	    {
 	      second->destroy();
-	      return first;
+	      return constant::true_instance();
 	    }
 	  if (second == constant::true_instance())
 	    {