Improvement. Cleanup how the bb equivalent vector operations are enabled.

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

diff --git a/src/STPManager/STP.cpp b/src/STPManager/STP.cpp
index fabb50a41c103b1e3172f3d77f3c89e577212603..50c8adf71c93d053179eb7fc99efc2981209a110 100644 (file)
--- a/src/STPManager/STP.cpp
+++ b/src/STPManager/STP.cpp
@@ -123,6 +123,7 @@ namespace BEEV {
              * TODO: I replace with the lower id node, sometimes though we replace with much more
              * difficult looking ASTNodes.
             */
+            //cerr << "eQUIV";
 #if 0
             ASTNodeMap::iterator it = equivs.begin();
             while (it!=equivs.end())

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

diff --git a/src/simplifier/simplifier.cpp b/src/simplifier/simplifier.cpp
index 5edf37fb0382c8fd487fb21249eab772fd5fb8f2..d667b8ec9186edf219a38329f42a044947074106 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","0"))
+    if (!_bm->UserFlags.isSet("bb-equiv",""))
       AlwaysTrueHashSet.insert(key.GetNodeNum());
   }
 

diff --git a/src/to-sat/BitBlaster.cpp b/src/to-sat/BitBlaster.cpp
index dc872e75edabccc3af2b86a70f3f9095ca3a7a39..739e7ebeae35f91d078c010f2ee24daf5d379976 100644 (file)
--- a/src/to-sat/BitBlaster.cpp
+++ b/src/to-sat/BitBlaster.cpp
@@ -166,7 +166,7 @@ namespace BEEV
           fromTo.insert(make_pair(n, r));
         }
 
-      if (form.GetSTPMgr()->UserFlags.isSet("bb-equiv","0"))
+      if (form.GetSTPMgr()->UserFlags.isSet("bb-equiv",""))
       {
         HASHMAP <intptr_t ,ASTNode> nodeToFn;
         typename map<ASTNode, BBNode>::iterator it;
@@ -202,7 +202,7 @@ namespace BEEV
       }
 
       typedef HASHMAP<vector<BBNode>, ASTNode,BBVecHasher <BBNode>, BBVecEquals<BBNode> > M;
-      if (form.GetSTPMgr()->UserFlags.isSet("bb-equiv", "0"))
+      if (form.GetSTPMgr()->UserFlags.isSet("bb-equiv",""))
         {
           M lookup;
           typename std::map<ASTNode, vector<BBNode> >::iterator it;