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

diff --git a/src/simplifier/simplifier.cpp b/src/simplifier/simplifier.cpp
index dfc5ee6b9da3c83c07ec372e5d585b3dc15d00cb..78eff9166be56cbd6c078263704ef54a49fc277c 100644 (file)
--- 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 (file)
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)
+