From 9e85b66d1cdbaa6b38dd30773593f18dd1b085d2 Mon Sep 17 00:00:00 2001
From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Sat, 10 Jul 2010 09:55:19 +0000
Subject: [PATCH] Fix the build + extra options for constant bit propagation
 (not currently enabled).

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@949 e59a4935-1847-0410-ae03-e826735625c1
---
 src/simplifier/bvsolver.h                     |  1 +
 .../constantBitP/ConstantBitPropagation.cpp   | 26 ++++++++++++++++---
 .../constantBitP/ConstantBitPropagation.h     |  5 ++++
 3 files changed, 28 insertions(+), 4 deletions(-)

diff --git a/src/simplifier/bvsolver.h b/src/simplifier/bvsolver.h
index ee477ff..4773824 100644
--- a/src/simplifier/bvsolver.h
+++ b/src/simplifier/bvsolver.h
@@ -99,6 +99,7 @@ namespace BEEV
     //this function return true if the var occurs in term, else the
     //function returns false
     bool VarSeenInTerm(const ASTNode& var, const ASTNode& term);
+    void SetofVarsSeenInTerm(const ASTNode& term, ASTNodeSet& symbols);
 
     void VarSeenInTerm(Symbols* term, SymbolPtrSet& visited, ASTNodeSet& found, vector<Symbols*>& av);
 
diff --git a/src/simplifier/constantBitP/ConstantBitPropagation.cpp b/src/simplifier/constantBitP/ConstantBitPropagation.cpp
index b048e70..68a4946 100644
--- a/src/simplifier/constantBitP/ConstantBitPropagation.cpp
+++ b/src/simplifier/constantBitP/ConstantBitPropagation.cpp
@@ -5,6 +5,8 @@
 #include "../../AST/NodeFactory/NodeFactory.h"
 #include "../../simplifier/simplifier.h"
 #include "ConstantBitP_Utility.h"
+#include <iostream>
+#include <fstream>
 
 #ifdef WITHCBITP
   #include "ConstantBitP_TransferFunctions.h"
@@ -38,8 +40,9 @@ namespace simplifier
     dispatchToMaximallyPrecise(const Kind k, vector<FixedBits*>& children,
         FixedBits& output, const ASTNode n);
 
-    const bool debug_cBitProp_messages = true;
-    const bool output_mult_like = true;
+    const bool debug_cBitProp_messages = false;
+    const bool output_mult_like = false;
+    const bool debug_print_graph_after = false;
 
     ////////////////////
 
@@ -108,7 +111,7 @@ namespace simplifier
 
     // Put anything that's entirely fixed into a from->to map.
     ASTNodeMap
-    getAllFixed(NodeToFixedBitsMap* fixedMap)
+    ConstantBitPropagation::getAllFixed()
     {
       NodeToFixedBitsMap::NodeToFixedBitsMapType::iterator it;
 
@@ -140,6 +143,9 @@ namespace simplifier
     void
     ConstantBitPropagation::setNodeToTrue(const ASTNode& top)
     {
+      assert(!topFixed);
+      topFixed = true;
+
       FixedBits & topFB = *getCurrentFixedBits(top);
       topFB.setFixed(0, true);
       topFB.setValue(0, true);
@@ -195,6 +201,7 @@ namespace simplifier
         }
 #endif
 
+      topFixed = false;
     }
 
     // Both way propagation. Initialising the top to "true".
@@ -214,7 +221,7 @@ namespace simplifier
       status = NO_CHANGE;
 
       //Determine what must always be true.
-      ASTNodeMap fromTo = getAllFixed(fixedMap);
+      ASTNodeMap fromTo = getAllFixed();
 
       if (debug_cBitProp_messages)
         {
@@ -343,6 +350,17 @@ namespace simplifier
           result = nf->CreateNode(AND, result, toConjoin); // conjoin the new conditions.
         }
 
+
+  	if (debug_print_graph_after)
+		{
+			ofstream file;
+			file.open("afterCbitp.gdl");
+			PrintingHackfixedMap = fixedMap;
+			printer::GDL_Print(file,top,&toString);
+			file.close();
+		}
+
+
       assert(BVTypeCheck(result));
       assert(status != CONFLICT); // conflict should have been seen earlier.
       return result;
diff --git a/src/simplifier/constantBitP/ConstantBitPropagation.h b/src/simplifier/constantBitP/ConstantBitPropagation.h
index d9b62b5..fbf237f 100644
--- a/src/simplifier/constantBitP/ConstantBitPropagation.h
+++ b/src/simplifier/constantBitP/ConstantBitPropagation.h
@@ -40,6 +40,8 @@ namespace simplifier
       Dependencies * dependents;
       MultiplicationStatsMap* msm;
 
+      bool topFixed;
+
       void
       printNodeWithFixings();
 
@@ -100,6 +102,9 @@ public:
 
       void
       setNodeToTrue(const ASTNode& top);
+
+      ASTNodeMap
+      getAllFixed();
     };
   }
 }
-- 
2.47.3