From 8498bcf3d48f7c8eee14318b3cb847cc83a6210b Mon Sep 17 00:00:00 2001
From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Fri, 3 Feb 2012 14:28:35 +0000
Subject: [PATCH] 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
---
 src/STPManager/STP.cpp            | 1 +
 src/STPManager/UserDefinedFlags.h | 2 ++
 src/simplifier/simplifier.cpp     | 2 +-
 src/to-sat/BitBlaster.cpp         | 4 ++--
 4 files changed, 6 insertions(+), 3 deletions(-)

diff --git a/src/STPManager/STP.cpp b/src/STPManager/STP.cpp
index fabb50a..50c8adf 100644
--- 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 d817dee..40084d6 100644
--- 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 5edf37f..d667b8e 100644
--- 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 dc872e7..739e7eb 100644
--- 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;
-- 
2.47.3