Extra tests for inactive by-default code

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

diff --git a/src/to-sat/BitBlaster.cpp b/src/to-sat/BitBlaster.cpp
index 553d9a7302b4f6be5f673e275f008efaa2a6c8f1..718008dd5263ec2e5517a22f161643f972c87490 100644 (file)
--- a/src/to-sat/BitBlaster.cpp
+++ b/src/to-sat/BitBlaster.cpp
@@ -98,7 +98,7 @@ bool BitBlaster<BBNode,BBNodeManagerT>::update(const ASTNode&n, const int i, sim
 {
         if (b->isFixed(i) && (!(bb == BBTrue || bb == BBFalse)))
         {
-                //We have a fixed bit, but the bitblasted values aren't constant true or false.
+          //We have a fixed bit, but the bitblasted values aren't constant true or false.
             if (conjoin_to_top && (fixedFromBottom.find(n) == fixedFromBottom.end()))
             {
               if (b->getValue(i))
@@ -193,9 +193,27 @@ void BitBlaster<BBNode,BBNodeManagerT>::updateTerm(const ASTNode&n, BBNodeVec& b
                 cb->propagate();
                 //cerr << "##!!" << endl;
         }
+
+        if (!cb->isUnsatisfiable())
+          for (int i = 0; i < (int) bb.size(); i++)
+          {
+            if (b->isFixed(i) && b->getValue(i))
+              assert(bb[i] == BBTrue);
+
+            if (b->isFixed(i) && !b->getValue(i))
+              assert(bb[i] == BBFalse);
+
+            if (bb[i] == BBFalse)
+              assert( b->isFixed(i) && !b->getValue(i));
+
+            if (bb[i] == BBTrue)
+              assert( b->isFixed(i) && b->getValue(i));
+          }
 }
 
 
+
+
 template <class BBNode, class BBNodeManagerT>
 const BBNodeVec BitBlaster<BBNode,BBNodeManagerT>::BBTerm(const ASTNode& term, BBNodeSet& support) {
         typename BBNodeVecMap::iterator it = BBTermMemo.find(term);
@@ -399,8 +417,9 @@ const BBNodeVec BitBlaster<BBNode,BBNodeManagerT>::BBTerm(const ASTNode& term, B
                assert(BVTypeCheck(term));
                assert(term.Degree() == 2);
 
-               const BBNodeVec& mpcd1 = BBTerm(term[0], support);
-               const BBNodeVec& mpcd2 = BBTerm(term[1], support);
+               const BBNodeVec& mpcd1 = BBTerm(term[0], support);
+               const BBNodeVec& mpcd2 = BBTerm(term[1], support);
+
                assert(mpcd1.size() == mpcd2.size());
                result = BBMult(mpcd1, mpcd2, support,term);
                break;
@@ -1247,6 +1266,9 @@ BBNodeVec BitBlaster<BBNode,BBNodeManagerT>::mult_normal(const BBNodeVec& x,
     if (cb == NULL)
       return;
 
+    if (cb->isUnsatisfiable())
+      return;
+
     if (cb->fixedMap->map->find(n) != cb->fixedMap->map->end())
       {
         FixedBits* b = cb->fixedMap->map->find(n)->second;