From 45cdbb54b38f64401e85f15affc5d99126048b0a Mon Sep 17 00:00:00 2001
From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Tue, 1 Mar 2011 12:30:42 +0000
Subject: [PATCH] Improvement. Add an equality simplification.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1180 e59a4935-1847-0410-ae03-e826735625c1
---
 src/simplifier/simplifier.cpp | 17 ++++++++++++++++-
 unit_test/eq2.smt2            | 25 +++++++++++++++++++++++++
 2 files changed, 41 insertions(+), 1 deletion(-)
 create mode 100644 unit_test/eq2.smt2

diff --git a/src/simplifier/simplifier.cpp b/src/simplifier/simplifier.cpp
index dfc5ee6..78eff91 100644
--- a/src/simplifier/simplifier.cpp
+++ b/src/simplifier/simplifier.cpp
@@ -993,9 +993,24 @@ namespace BEEV
         ASTNode r =  nf->CreateNode(AND, nf->CreateNode(EQ, top, in2[0]), nf->CreateNode(EQ, bottom, in2[1]));
 
         return r;
-
     }
 
+    {
+      // If it can only evaluate to constants on the LHS and the RHS, and those constants are never equal,
+      // then it must be false. e.g.   ite( f, 10 , 20 ) = ite (g, 30 ,12)
+      ASTNodeSet visited0, visited1;
+      vector<ASTNode> l0, l1;
+
+      if  (getPossibleValues(in1, visited0, l0) && getPossibleValues(in2, visited1, l1))
+        {
+            sort(l0.begin(), l0.end());
+            sort(l1.begin(), l1.end());
+            vector<ASTNode> result(l0.size() + l1.size());
+            vector<ASTNode>::iterator it = set_intersection(l0.begin(), l0.end(), l1.begin(), l1.end(), result.begin());
+            if (it == result.begin())
+              return ASTFalse;
+        }
+    }
 
     //last resort is to CreateNode
     return nf->CreateNode(EQ, in1, in2);
diff --git a/unit_test/eq2.smt2 b/unit_test/eq2.smt2
new file mode 100644
index 0000000..6994c29
--- /dev/null
+++ b/unit_test/eq2.smt2
@@ -0,0 +1,25 @@
+
+(set-logic QF_BV)
+(set-info :smt-lib-version 2.0)
+(set-info :category "check")
+(set-info :status sat)
+
+; These can be simplified by considering the context
+; of the ITES they contain. 
+
+(declare-fun v0 () (_ BitVec 20))
+(declare-fun v1 () (_ BitVec 20))
+(declare-fun v2 () (_ BitVec 20))
+
+; The first disjunct is unsatisfiable. So it should be removed. Making v0 or v1 unconstrained.
+
+(assert (or 
+			 (= (_ bv1 20) (ite (= (_ bv2 20) (bvudiv v0 v1)) (_ bv3 20) (_ bv5 20)  ) )
+			 (= (bvadd v0 v1) (_ bv1 20) )
+	    )
+)
+
+
+(check-sat)
+(exit)
+
-- 
2.47.3