Add an extra simplification rule to the simplifying node factory.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1265 e59a4935-1847-0410-ae03-e826735625c1

diff --git a/src/AST/NodeFactory/SimplifyingNodeFactory.cpp b/src/AST/NodeFactory/SimplifyingNodeFactory.cpp
index 1cd2d523fb530da5117daf0d85a2d8cede040592..85ec1d1839cb1a16b5c457755838e7030ed00f1f 100644 (file)
--- a/src/AST/NodeFactory/SimplifyingNodeFactory.cpp
+++ b/src/AST/NodeFactory/SimplifyingNodeFactory.cpp
@@ -340,6 +340,16 @@ ASTNode SimplifyingNodeFactory::CreateSimpleEQ(const ASTVec& children)
         if (k2 == BEEV::BVUMINUS && k1 == BEEV::BVCONST || (k2 == BEEV::BVNEG && k1 == BEEV::BVCONST))
           return NodeFactory::CreateNode(BEEV::EQ, in2[0], NodeFactory::CreateTerm(k2,width, in1 ));
 
+        if ((k1 == BEEV::BVNEG && in1[0] == in2) || (k2 == BEEV::BVNEG && in2[0] == in1))
+          return in1.GetSTPMgr()->ASTFalse;
+
+        if (k2 == BEEV::BVDIV && k1 == BEEV::BVCONST && (in1 == bm.CreateZeroConst(width)))
+            return NodeFactory::CreateNode(BEEV::BVGT, in2[1], in2[0]);
+
+        if (k1 == BEEV::BVDIV && k2 == BEEV::BVCONST && (in2 == bm.CreateZeroConst(width)))
+            return NodeFactory::CreateNode(BEEV::BVGT, in1[1], in1[0]);
+
+
        // This increases the number of nodes. So disable for now.
        if (false && BEEV::BVCONCAT == k1 && BEEV::BVCONCAT == k2 && in1[0].GetValueWidth() == in2[0].GetValueWidth())
          {

diff --git a/unit_test/bvge1.smt2 b/unit_test/bvge1.smt2
new file mode 100644 (file)
index 0000000..35afd3e
--- /dev/null
+++ b/unit_test/bvge1.smt2
@@ -0,0 +1,22 @@
+(set-logic QF_BV)
+(set-info :smt-lib-version 2.0)
+(set-info :category "check")
+(set-info :status unsat)
+(declare-fun x () (_ BitVec 10))
+(declare-fun y () (_ BitVec 10))
+
+
+; 
+(assert 
+        (bvult
+               (bvudiv x  y )
+               (_ bv1 10)
+       )
+)
+
+(assert (not (bvult x y)))
+
+
+(check-sat)
+(exit)
+