From 9881370e3717cd3aba5f41d2559fb381dc51d3e1 Mon Sep 17 00:00:00 2001
From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Sun, 10 Apr 2011 11:37:02 +0000
Subject: [PATCH] Adds code, that's not currently enabled, to read-out all the
 nodes that the bitblaster discovers should be constant.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1263 e59a4935-1847-0410-ae03-e826735625c1
---
 src/to-sat/BitBlaster.cpp | 80 +++++++++++++++++++++++++++++++++++++++
 src/to-sat/BitBlaster.h   |  3 ++
 2 files changed, 83 insertions(+)

diff --git a/src/to-sat/BitBlaster.cpp b/src/to-sat/BitBlaster.cpp
index d7a4cb0..37d4ba4 100644
--- 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 f20c7f2..42d0dfd 100644
--- 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
-- 
2.47.3