Improvement. Change how the bitblast equivalence checking is enabled.

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

diff --git a/src/STPManager/UserDefinedFlags.h b/src/STPManager/UserDefinedFlags.h
index 179b85117871d79ba1672d615b6912ac0e9ad8f3..1653bc3edcd0081a034c7d9f3e9cec593070dae6 100644 (file)
--- a/src/STPManager/UserDefinedFlags.h
+++ b/src/STPManager/UserDefinedFlags.h
@@ -294,8 +294,6 @@ namespace BEEV
       // If the bit-blaster discovers new constants, should the term simplifier be re-run.
       simplify_during_BB_flag=false;
 
-      set("bb-equiv","1");
-
     } //End of constructor for UserDefinedFlags
 
   }; //End of struct UserDefinedFlags

diff --git a/src/simplifier/simplifier.cpp b/src/simplifier/simplifier.cpp
index 25a6a9f0bf470b6832ceac4eddd1f38e5f3e2889..edcefaebd6316f9cf09db66ad5c4407d2c852671 100644 (file)
--- a/src/simplifier/simplifier.cpp
+++ b/src/simplifier/simplifier.cpp
@@ -219,7 +219,7 @@ namespace BEEV
     // leaves just one instance of the constraint, so it we replace it with true/false
     // the constraint is lost. This is subsumed by constant bit propagation, so I suspect
     // it's not a big loss.
-    if (!_bm->UserFlags.isSet("bb-equiv",""))
+    if (!_bm->UserFlags.isSet("bb-equiv","1"))
       AlwaysTrueHashSet.insert(key.GetNodeNum());
   }
 

diff --git a/src/to-sat/BitBlaster.cpp b/src/to-sat/BitBlaster.cpp
index 959566333e51eca5edb94bfeca065beddc67ab4e..8083007976f0461e1979eac7e1f0bbb822fa962b 100644 (file)
--- a/src/to-sat/BitBlaster.cpp
+++ b/src/to-sat/BitBlaster.cpp
@@ -167,7 +167,7 @@ namespace BEEV
           fromTo.insert(make_pair(n, r));
         }
 
-      if (form.GetSTPMgr()->UserFlags.isSet("bb-equiv",""))
+      if (form.GetSTPMgr()->UserFlags.isSet("bb-equiv","1"))
       {
         HASHMAP <intptr_t ,ASTNode> nodeToFn;
         typename map<ASTNode, BBNode>::iterator it;
@@ -203,7 +203,7 @@ namespace BEEV
       }
 
       typedef HASHMAP<vector<BBNode>, ASTNode,BBVecHasher <BBNode>, BBVecEquals<BBNode> > M;
-      if (form.GetSTPMgr()->UserFlags.isSet("bb-equiv",""))
+      if (form.GetSTPMgr()->UserFlags.isSet("bb-equiv","1"))
         {
           M lookup;
           typename std::map<ASTNode, vector<BBNode> >::iterator it;
@@ -791,7 +791,7 @@ namespace BEEV
             results.push_back(BBTerm(term[i], support));
 
           const int bitWidth = term[0].GetValueWidth();
-          std::vector<list<BBNode> > products(bitWidth);
+          std::vector<list<BBNode> > products(bitWidth+1);
           for (int i = 0; i < bitWidth; i++)
             {
             for (int j = 0; j < results.size(); j++)