From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Sat, 10 Jul 2010 09:45:19 +0000 (+0000)
Subject: Extra code (not enabled), for constant bit propagation.
X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=fd7367fc76f8699e38b188be91bc639e93e7683c;p=francis%2Fstp.git

Extra code (not enabled), for constant bit propagation.



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

diff --git a/src/to-sat/BitBlaster.cpp b/src/to-sat/BitBlaster.cpp
index e21e158..7f0fc2a 100644
--- a/src/to-sat/BitBlaster.cpp
+++ b/src/to-sat/BitBlaster.cpp
@@ -33,6 +33,7 @@ namespace BEEV {
  ********************************************************************/
 
 using simplifier::constantBitP::FixedBits;
+using simplifier::constantBitP::NodeToFixedBitsMap;
 
 #define BBNodeVec vector<BBNode>
 #define BBNodeVecMap map<ASTNode, vector<BBNode> >
@@ -51,6 +52,8 @@ vector<BBNodeAIG> _empty_BBNodeAIGVec;
 const bool debug_do_check = false;
 const bool debug_bitblaster = false;
 
+const bool conjoin_to_top = true;
+
 template <class BBNode, class BBNodeManagerT>
 void BitBlaster<BBNode,BBNodeManagerT>::commonCheck(const ASTNode& n) {
         cerr << "Non constant is constant:";
@@ -96,11 +99,13 @@ bool BitBlaster<BBNode,BBNodeManagerT>::update(const ASTNode&n, const int i, sim
         if (b->isFixed(i) && (!(bb == BBTrue || bb == BBFalse)))
         {
                 //We have a fixed bit, but the bitblasted values aren't constant true or false.
-
-                //if (b->getValue(i))
-                        //support.insert(bb);
-                //else
-                  //      support.insert(nf->CreateNode(NOT,bb));
+            if (conjoin_to_top && (fixedFromBottom.find(n) == fixedFromBottom.end()))
+            {
+              if (b->getValue(i))
+                support.insert(bb);
+              else
+                support.insert(nf->CreateNode(NOT, bb));
+            }
 
                 bb = b->getValue(i) ? BBTrue : BBFalse;
         }
@@ -391,6 +396,7 @@ const BBNodeVec BitBlaster<BBNode,BBNodeManagerT>::BBTerm(const ASTNode& term, B
 	}
 	case BVMULT: {
 		assert(BVTypeCheck(term));
+		assert(term.Degree() == 2);
 
 		const ASTNode& t0 = term[0];
 		const ASTNode& t1 = term[1];
@@ -515,21 +521,39 @@ const BBNodeVec BitBlaster<BBNode,BBNodeManagerT>::BBTerm(const ASTNode& term, B
 template <class BBNode, class BBNodeManagerT>
 const BBNode BitBlaster<BBNode,BBNodeManagerT>::BBForm(const ASTNode& form)
 {
+
+      if (conjoin_to_top && cb != NULL)
+        {
+          ASTNodeMap n =  cb->getAllFixed();
+          for (ASTNodeMap::const_iterator it = n.begin(); it != n.end(); it++)
+            fixedFromBottom.insert(it->first);
+
+          // Mark the top node as true.
+          cb->setNodeToTrue(form);
+          cb->propagate();
+        }
+
     BBNodeSet support;
     BBNode r= BBForm(form,support);
-    //vector<BBNode> v;
-    //v.insert(v.end(), support.begin(), support.end());
-    //v.push_back(r);
-    assert(support.size() ==0);
 
+    vector<BBNode> v;
+    v.insert(v.end(), support.begin(), support.end());
+    v.push_back(r);
+
+    if (!conjoin_to_top)
+        {
+          assert(support.size() ==0);
+        }
 
     if (cb != NULL && !cb->isUnsatisfiable())
       {
       ASTNodeSet visited;
       assert(cb->checkAtFixedPoint(form,visited));
       }
-    //    return nf->CreateNode(AND,v);
-    return r;
+    if (v.size() == 1)
+        return v[0];
+      else
+        return nf->CreateNode(AND, v);
 }
 
 // bit blast a formula (boolean term).  Result is one bit wide,
diff --git a/src/to-sat/BitBlaster.h b/src/to-sat/BitBlaster.h
index 6278c1b..a580149 100644
--- a/src/to-sat/BitBlaster.h
+++ b/src/to-sat/BitBlaster.h
@@ -134,6 +134,10 @@ class BitBlaster {
 
         const BBNode BBForm(const ASTNode& form, set<BBNode>& support);
 
+        // Nodes in this set can be replaced by their constant values, without being
+        // conjoined to the top..
+        ASTNodeSet fixedFromBottom;
+
 public:
 	BBNodeManagerT* nf;