Adds code, that's not currently enabled, to read-out all the nodes that the bitblaste...

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

diff --git a/src/to-sat/BitBlaster.cpp b/src/to-sat/BitBlaster.cpp
index d7a4cb0b9007aeec8c1aa38a53834333c00d3546..37d4ba4893b2971b557d8493b98d18a9e64f18d5 100644 (file)
--- a/src/to-sat/BitBlaster.cpp
+++ b/src/to-sat/BitBlaster.cpp
@@ -55,6 +55,86 @@ const bool debug_bitblaster = false;
 
 const bool conjoin_to_top = true;
 
+
+// Look through the maps to see what the bitblaster has discovered (if anything) is constant.
+template <class BBNode, class BBNodeManagerT>
+void BitBlaster<BBNode,BBNodeManagerT>::getConsts(const ASTNode& form, ASTNodeMap& fromTo)
+{
+  assert(form.GetType() == BOOLEAN_TYPE);
+
+  BBNodeSet support;
+  BBForm(form, support);
+
+  assert(support.size() ==0);
+
+  {
+      typename map<ASTNode, BBNode>::iterator it;
+      for (it = BBFormMemo.begin(); it != BBFormMemo.end(); it++)
+        {
+          const ASTNode& n = it->first;
+          const BBNode& x = it->second;
+          if (n.isConstant())
+            continue;
+
+          if (x != BBTrue && x != BBFalse)
+            continue;
+
+          assert (n.GetType() == BOOLEAN_TYPE);
+
+          ASTNode result;
+          if (x == BBTrue)
+            result = n.GetSTPMgr()->ASTTrue;
+          else
+            result = n.GetSTPMgr()->ASTFalse;
+
+          if (n.GetKind() != SYMBOL)
+            fromTo.insert(make_pair(n, result));
+          else
+            simp->UpdateSubstitutionMap(n, result);
+        }
+    }
+
+  typename BBNodeVecMap::iterator it;
+  for (it = BBTermMemo.begin(); it != BBTermMemo.end(); it++)
+        {
+          const ASTNode& n = it->first;
+          assert (n.GetType() == BITVECTOR_TYPE);
+
+          if (n.isConstant())
+            continue;
+
+          vector<BBNode>& x = it->second;
+          assert(x.size() == n.GetValueWidth());
+
+          bool constNode= true;
+          for (int i = 0; i < (int) x.size(); i++)
+            {
+              if (x[i] != BBTrue && x[i] != BBFalse)
+                {
+                  constNode = false;
+                break;
+                }
+            }
+          if (!constNode)
+            continue;
+
+          CBV val = CONSTANTBV::BitVector_Create(n.GetValueWidth(), true);
+          for (int i = 0; i < (int) x.size(); i++)
+            {
+              if (x[i] == BBTrue)
+                CONSTANTBV::BitVector_Bit_On(val, i);
+            }
+
+          ASTNode r = n.GetSTPMgr()->CreateBVConst(val, n.GetValueWidth());
+          if (n.GetKind() == SYMBOL)
+            simp->UpdateSubstitutionMap(n, r);
+          else
+            fromTo.insert(make_pair(n, r));
+
+
+        }
+}
+
 template <class BBNode, class BBNodeManagerT>
 void BitBlaster<BBNode,BBNodeManagerT>::commonCheck(const ASTNode& n) {
         cerr << "Non constant is constant:";

diff --git a/src/to-sat/BitBlaster.h b/src/to-sat/BitBlaster.h
index f20c7f2498474f5f278d3a8e9187a8b663edc9fc..42d0dfde9c547fa0cb2246f0b901cfaea5d006cf 100644 (file)
--- a/src/to-sat/BitBlaster.h
+++ b/src/to-sat/BitBlaster.h
@@ -211,6 +211,9 @@ public:
        //Bitblast a formula
        const BBNode BBForm(const ASTNode& form);
 
+       void getConsts(const ASTNode& n, ASTNodeMap& fromTo);
+
+
 }; //end of class BitBlaster
 }
 ; //end of namespace