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

diff --git a/src/simplifier/bvsolver.h b/src/simplifier/bvsolver.h
index ee477ff8c623ca6ab73120db0fdb89a495e8e4a4..47738244f1b81c699f5f02261a3d1a26883e932e 100644 (file)
--- 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 b048e706264fa83971e9059a9f951f5152638871..68a494685e1840a4e43a2f5447da89d8a2bf56dd 100644 (file)
--- 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 d9b62b5ec87d3f45f7ae004532164264253e4afe..fbf237f1b230f8d367bcfaacaf3ae3fc6cb9e876 100644 (file)
--- 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();
     };
   }
 }