Fix to the bvsolver. Some cases were missing when identifying monomials.

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

diff --git a/src/simplifier/bvsolver.cpp b/src/simplifier/bvsolver.cpp
index 44d85d36cbc0b12c98bd16da594e6d1f7412afff..ef73f88e4ff93a290f176169b58f79db62191e33 100644 (file)
--- a/src/simplifier/bvsolver.cpp
+++ b/src/simplifier/bvsolver.cpp
@@ -251,7 +251,35 @@ namespace BEEV
                 outmonom = monom;
                 chosen_symbol = true;
               }
+            else if (
+                !chosen_symbol
+                && monom.GetKind() == BVEXTRACT
+                && SYMBOL == monom[0].GetKind()
+                && BVCONST == monom[1].GetKind()
+                && zero == monom[2]
+                && !DoNotSolveThis(monom[0])
+                && count.single(monom[0])
+            )
+              {
+              outmonom = monom;
+              chosen_symbol = true;
+              }
+            else if (
+                       !chosen_symbol
+                       && monom.GetKind() == BVUMINUS
+                       && monom[0].GetKind() == BVEXTRACT
+                       && SYMBOL == monom[0][0].GetKind()
+                       && BVCONST == monom[0][1].GetKind()
+                       && zero == monom[0][2]
+                       && !DoNotSolveThis(monom[0][0])
+                       && count.single(monom[0][0])
+                   )
+                     {
+                     outmonom = monom;
+                     chosen_symbol = true;
+                     }
             else
+
               {
                 o.push_back(monom);
               }
@@ -833,7 +861,8 @@ namespace BEEV
        _bm->CreateNode(AND, o) : 
        o[0]) : 
       ASTTrue;
-    output = _bm->CreateNode(AND, output, evens);
+    if (evens != ASTTrue)
+      output = _bm->CreateNode(AND, output, evens);
 
     output = solveForAndOfXOR(output);
 

diff --git a/unit_test/bvsolver.smt b/unit_test/bvsolver.smt
new file mode 100644 (file)
index 0000000..1f391f1
--- /dev/null
+++ b/unit_test/bvsolver.smt
@@ -0,0 +1,15 @@
+(benchmark r
+  :status sat
+  :category { crafted }
+  :difficulty { 0 }
+  :logic QF_BV
+  :extrafuns ((x BitVec[3]))
+  :extrafuns ((y BitVec[3]))
+  :extrafuns ((z BitVec[3]))
+
+  :assumption (= (bvadd (bvadd (bvmul bv3[3] x) (bvmul bv4[3] y)) (bvmul bv2[3] z)) bv0[3])
+  :assumption (= (bvadd (bvadd (bvmul bv2[3] x) (bvmul bv2[3] y)) (bvmul bv0[3] z)) bv6[3])
+  :assumption (= (bvadd (bvadd (bvmul bv2[3] x) (bvmul bv4[3] y)) (bvmul bv2[3] z)) bv0[3])
+
+  :formula true
+)

diff --git a/unit_test/unit_test.sh b/unit_test/unit_test.sh
index cdd1cec4a8fa31e1b0d26154bb607dc2b76788f0..ba04404b3c38864479484d5d548d434c17de7f3f 100755 (executable)
--- a/unit_test/unit_test.sh
+++ b/unit_test/unit_test.sh
@@ -5,12 +5,12 @@
 
 rm -f output_*.cnf
 
-files=`ls -1 -S *.smt2`
+files=`ls -1 -S *.smt2 *.smt`
 for f in $files; do
        stp --output-CNF $f
        cnf=`cat output_*.cnf  | grep -v "^c" | grep -v "^$" |  wc -l`
        if [ $cnf -gt 3 ] ; then
-               echo --fail
+               echo --fail $f
                exit 10
        fi