From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Sun, 22 Aug 2010 06:43:22 +0000 (+0000)
Subject: Bugfix. STP returned the wrong answer when something like bitwidth of 1: (0 = (1... 
X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=9211fcfc9e06702d3c124c95963b1309ed28a2d4;p=francis%2Fstp.git

Bugfix. STP returned the wrong answer when something like bitwidth of 1: (0 = (1+1)) made it to the bitblaster. Simplifying terms collapses (as we do now), collapses this down to (0 =0) which returns the correct answer. The bitvector solver didn't expect to see two constant in a plus.



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

diff --git a/src/simplifier/bvsolver.cpp b/src/simplifier/bvsolver.cpp
index fa3d4cd..44d85d3 100644
--- a/src/simplifier/bvsolver.cpp
+++ b/src/simplifier/bvsolver.cpp
@@ -40,6 +40,7 @@ namespace BEEV
 {
 	const bool flatten_ands = true;
 	const bool sort_extracts_last = false;
+	const bool debug_bvsolver = false;
 
   //check the solver map for 'key'. If key is present, then return the
   //value by reference in the argument 'output'
@@ -262,6 +263,13 @@ namespace BEEV
       _bm->CreateTerm(BVPLUS, lhs.GetValueWidth(), o) : 
       o[0];
 
+    if (debug_bvsolver)
+      {
+        cerr << "Initial:" << eq;
+        cerr << "Chosen Monomial:" << outmonom;
+        cerr << "Output LHS:" << modifiedlhs;
+      }
+
     // can be SYMBOL or (BVUMINUS SYMBOL) or (BVMULT ODD_BVCONST SYMBOL) or
     // (BVMULT ODD_BVCONST (EXTRACT SYMBOL BV_CONST ZERO))
     return outmonom;
@@ -742,8 +750,8 @@ namespace BEEV
     	 don't have time. Trev.
 		  */
 #if 1
-      ASTNode aaa = (any_solved && EQ == it->GetKind()) ? _simp->applySubstitutionMapUntilArrays(*it) : *it;
-#else
+        ASTNode aaa = (any_solved && EQ == it->GetKind()) ? _simp->SimplifyFormula(_simp->applySubstitutionMapUntilArrays(*it),false,NULL) : *it;
+      #else
           ASTNode aaa = *it;
 
           if (any_solved && EQ == aaa.GetKind())
@@ -871,6 +879,8 @@ namespace BEEV
 
         if (BVCONST == itk)
           {
+            assert(savetheconst == rhs); // Returns the wrong result if there are >1 constants.
+
             //check later if the constant is even or not
             savetheconst = aaa;
             continue;
diff --git a/src/simplifier/constantBitP/ConstantBitPropagation.cpp b/src/simplifier/constantBitP/ConstantBitPropagation.cpp
index f8848ab..b81f023 100644
--- a/src/simplifier/constantBitP/ConstantBitPropagation.cpp
+++ b/src/simplifier/constantBitP/ConstantBitPropagation.cpp
@@ -339,14 +339,19 @@ namespace simplifier
             }
         }
 
-
      // Write the constants into the main graph.
       ASTNodeMap cache;
       ASTNode result = SubstitutionMap::replace(top, fromTo, cache,nf);
 
       if (0 != toConjoin.size())
         {
-          result = nf->CreateNode(AND, result, toConjoin); // conjoin the new conditions.
+          // It doesn't happen very often. But the "toConjoin" might contain a variable
+          // that was added to the substitution map (because the value was determined just now
+          // during propagation.
+          ASTNode conjunct = (1 == toConjoin.size())? toConjoin[0]: nf->CreateNode(AND,toConjoin);
+          conjunct = simplifier->applySubstitutionMap(conjunct);
+
+          result = nf->CreateNode(AND, result, conjunct); // conjoin the new conditions.
         }