More getting ready for constant bit propagation. This code doesn't run, so nothing...

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

diff --git a/src/AST/RunTimes.cpp b/src/AST/RunTimes.cpp
index d8efe428ae8c2b4980298fba5b9beadbfe1e12f3..d08383a84bc6afe4e002ce269189f4a6abdd30f8 100644 (file)
--- a/src/AST/RunTimes.cpp
+++ b/src/AST/RunTimes.cpp
@@ -15,7 +15,7 @@
 #include "RunTimes.h"
 
 // BE VERY CAREFUL> Update the Category Names to match.
-std::string RunTimes::CategoryNames[] = { "Transforming", "Simplifying", "Parsing", "CNF Conversion", "Bit Blasting", "SAT Solving", "Bitvector Solving","Create SubstitutionMap", "Sending to SAT Solver", "Counter Example Generation","SAT Simplification"};
+std::string RunTimes::CategoryNames[] = { "Transforming", "Simplifying", "Parsing", "CNF Conversion", "Bit Blasting", "SAT Solving", "Bitvector Solving","Create SubstitutionMap", "Sending to SAT Solver", "Counter Example Generation","SAT Simplification", "Constant Bit Propagation"};
 
 namespace BEEV
 {

diff --git a/src/AST/RunTimes.h b/src/AST/RunTimes.h
index fbf686bf1170190948ae59c3d3e813a43bb984ab..59ced64b6ff3023f5ce3fa7deda912dfaae76eb4 100644 (file)
--- a/src/AST/RunTimes.h
+++ b/src/AST/RunTimes.h
@@ -29,7 +29,8 @@ public:
       CreateSubstitutionMap, 
       SendingToSAT,
       CounterExampleGeneration,
-      SATSimplifying
+      SATSimplifying,
+      ConstantBitPropagation
     };
 
   static std::string CategoryNames[];

diff --git a/src/STPManager/STP.cpp b/src/STPManager/STP.cpp
index 5fe9d261bd745ac697d56d648e7a3030ab51dfcb..e4e942bdc45d555490226f2274d3a272376b96db 100644 (file)
--- a/src/STPManager/STP.cpp
+++ b/src/STPManager/STP.cpp
@@ -10,6 +10,8 @@
 #include "STP.h"
 #include "DifficultyScore.h"
 #include "../to-sat/AIG/ToSATAIG.h"
+#include "../simplifier/constantBitP/ConstantBitPropagation.h"
+#include "../simplifier/constantBitP/NodeToFixedBitsMap.h"
 
 namespace BEEV {
 
@@ -124,6 +126,22 @@ namespace BEEV {
       } 
     while (inputToSAT != simplified_solved_InputToSAT);
 
+#ifdef WITHCBITP
+    if (bm->UserFlags.bitConstantProp_flag)
+      {
+        bm->ASTNodeStats("Before Constant Bit Propagation begins: ",
+            simplified_solved_InputToSAT);
+
+        bm->GetRunTimes()->start(RunTimes::ConstantBitPropagation);
+        simplifier::constantBitP::ConstantBitPropagation cb(simp, bm->defaultNodeFactory
+            );
+        simplified_solved_InputToSAT = cb.topLevelBothWays(
+            simplified_solved_InputToSAT);
+        bm->GetRunTimes()->stop(RunTimes::ConstantBitPropagation);
+      }
+#endif
+
+
     bm->ASTNodeStats("Before SimplifyWrites_Inplace begins: ", 
                      simplified_solved_InputToSAT);
 
@@ -232,17 +250,47 @@ namespace BEEV {
     delete bvsolver;
     bvsolver = new BVSolver(bm,simp);
 
+    // If it doesn't contain array operations, use ABC's CNF generation.
+    if (!arrayops)
     {
-    ToSATAIG toSATAIG(bm);
+      simplifier::constantBitP::ConstantBitPropagation* cb = NULL;
 
-    // If it doesn't contain array operations, use ABC's CNF generation.
-    res = 
-      Ctr_Example->CallSAT_ResultCheck(NewSolver, 
-                                       simplified_solved_InputToSAT, 
+#ifdef WITHCBITP
+    if (bm->UserFlags.bitConstantProp_flag)
+      {
+        bm->ASTNodeStats("Before Constant Bit Propagation begins: ",
+            simplified_solved_InputToSAT);
+
+        bm->GetRunTimes()->start(RunTimes::ConstantBitPropagation);
+
+        cb = new simplifier::constantBitP::ConstantBitPropagation(simp, bm->defaultNodeFactory);
+        cb->getFixedMap(simplified_solved_InputToSAT);
+
+        bm->GetRunTimes()->stop(RunTimes::ConstantBitPropagation);
+      }
+#endif
+
+    ToSATAIG toSATAIG(bm,cb);
+
+    res =
+      Ctr_Example->CallSAT_ResultCheck(NewSolver,
+                                       simplified_solved_InputToSAT,
                                        orig_input,
-                                       (arrayops ? ((ToSATBase*)tosat): ((ToSATBase*)&toSATAIG))
+                                       &toSATAIG
                                        );
+
+    delete cb;
     }
+    else
+      {
+      res =
+        Ctr_Example->CallSAT_ResultCheck(NewSolver,
+                                         simplified_solved_InputToSAT,
+                                         orig_input,
+                                         tosat
+                                         );
+
+      }
 
     if (SOLVER_UNDECIDED != res)
       {

diff --git a/src/main/main.cpp b/src/main/main.cpp
index 678861c092d31966bd31f2b0e9acb48bc1789929..04098e7e3365c6276a0f163dc911e89a5d1ab769 100644 (file)
--- a/src/main/main.cpp
+++ b/src/main/main.cpp
@@ -61,7 +61,7 @@ static const intptr_t INITIAL_MEMORY_PREALLOCATION_SIZE = 4000000;
  * step 5. Call SAT to determine if input is SAT or UNSAT
  ********************************************************************/
 
-typedef enum {PRINT_BACK_C=1, PRINT_BACK_CVC, PRINT_BACK_SMTLIB2,PRINT_BACK_SMTLIB1, PRINT_BACK_GDL, PRINT_BACK_DOT, OUTPUT_BENCH, OUTPUT_CNF, USE_SIMPLIFYING_SOLVER, SMT_LIB2_FORMAT, SMT_LIB1_FORMAT} OptionType;
+typedef enum {PRINT_BACK_C=1, PRINT_BACK_CVC, PRINT_BACK_SMTLIB2,PRINT_BACK_SMTLIB1, PRINT_BACK_GDL, PRINT_BACK_DOT, OUTPUT_BENCH, OUTPUT_CNF, USE_SIMPLIFYING_SOLVER, SMT_LIB2_FORMAT, SMT_LIB1_FORMAT, DISABLE_CBITP} OptionType;
 
 int main(int argc, char ** argv) {
   char * infile = NULL;
@@ -107,6 +107,8 @@ int main(int argc, char ** argv) {
   helpstring +=  
     "-d  : check counterexample\n";
   helpstring +=  
+      "--disable-cbitp  : disable constant bit propagation\n";
+  helpstring +=
     "-e  : expand finite-for construct\n";
   helpstring +=  
     "-f  : number of abstraction-refinement loops\n";
@@ -181,9 +183,13 @@ helpstring +=
                          lookup.insert(make_pair(tolower("--simplifying-minisat"),USE_SIMPLIFYING_SOLVER));
                          lookup.insert(make_pair(tolower("--SMTLIB2"),SMT_LIB2_FORMAT));
                          lookup.insert(make_pair(tolower("--SMTLIB1"),SMT_LIB1_FORMAT));
+                         lookup.insert(make_pair(tolower("--disable-cbitp"),DISABLE_CBITP));
 
                          switch(lookup[tolower(argv[i])])
                          {
+                         case DISABLE_CBITP:
+                                  bm->UserFlags.bitConstantProp_flag = false;
+                                  break;
                          case PRINT_BACK_C:
                                  bm->UserFlags.print_STPinput_back_C_flag = true;
                                  onePrintBack = true;

diff --git a/src/simplifier/constantBitP/ConstantBitPropagation.h b/src/simplifier/constantBitP/ConstantBitPropagation.h
index 3b246d384fbfbe9afe202b96cf49d2902f2960ef..745e907e103fa76bb45b70dde465ea25dcb64045 100644 (file)
--- a/src/simplifier/constantBitP/ConstantBitPropagation.h
+++ b/src/simplifier/constantBitP/ConstantBitPropagation.h
@@ -6,6 +6,7 @@
 #include <map>
 #include "FixedBits.h"
 #include "../../AST/AST.h"
+#include "NodeToFixedBitsMap.h"
 
 namespace BEEV
 {
@@ -58,7 +59,11 @@ namespace simplifier
     public:
 
       NodeToFixedBitsMap* fixedMap;
-      //MultiplicationStatsMap* multiplicationStats;
+
+#ifdef WITHCBITP
+      MultiplicationStatsMap* multiplicationStats;
+#endif
+
       WorkList *workList;
       Dependencies * dependents;
       Simplifier *simplifier;
@@ -75,6 +80,8 @@ namespace simplifier
 
       ~ConstantBitPropagation()
       {
+        if (fixedMap != NULL)
+          delete fixedMap;
       }
       ;
 

diff --git a/src/to-sat/AIG/ToSATAIG.h b/src/to-sat/AIG/ToSATAIG.h
index d09176fdf9b3c3cd1daf188037725e9547e7a2fe..588f4ec42d1fd86135395d4c648e3c49dff63d3b 100644 (file)
--- a/src/to-sat/AIG/ToSATAIG.h
+++ b/src/to-sat/AIG/ToSATAIG.h
@@ -26,6 +26,7 @@ namespace BEEV
   private:
 
     ASTNodeToSATVar nodeToSATVar;
+    simplifier::constantBitP::ConstantBitPropagation* cb;
 
     // don't assign or copy construct.
     ToSATAIG&  operator = (const ToSATAIG& other);
@@ -36,8 +37,16 @@ namespace BEEV
     ToSATAIG(STPMgr * bm) :
       ToSATBase(bm)
     {
+      cb = NULL;
     }
 
+    ToSATAIG(STPMgr * bm, simplifier::constantBitP::ConstantBitPropagation* cb_) :
+      ToSATBase(bm)
+    {
+      cb = cb_;
+    }
+
+
     void
     ClearAllTables()
     {
@@ -56,18 +65,17 @@ namespace BEEV
     CallSAT(MINISAT::Solver& satSolver, const ASTNode& input)
     {
       BBNodeManagerAIG mgr;
-      BitBlaster<BBNodeAIG, BBNodeManagerAIG> bb(&mgr);
-      set<BBNodeAIG> support;
+      BitBlaster<BBNodeAIG, BBNodeManagerAIG> bb(&mgr,cb);
 
       bm->GetRunTimes()->start(RunTimes::BitBlasting);
-      BBNodeAIG BBFormula = bb.BBForm(input, support);
+      BBNodeAIG BBFormula = bb.BBForm(input);
       bm->GetRunTimes()->stop(RunTimes::BitBlasting);
 
-      assert(support.size() ==0); // hot handled yet..
       assert(satSolver.nVars() ==0);
 
       Cnf_Dat_t* cnfData = NULL;
 
+
       mgr.toCNF(BBFormula, cnfData, nodeToSATVar);
 
       // Free the memory in the AIGs.

diff --git a/src/to-sat/BitBlaster.cpp b/src/to-sat/BitBlaster.cpp
index 8387083ea5c588ed4ffd8d261973370a088a306c..a62233ef35d6d6e175279e9f4b7f2d75a1952f34 100644 (file)
--- a/src/to-sat/BitBlaster.cpp
+++ b/src/to-sat/BitBlaster.cpp
@@ -32,7 +32,7 @@ namespace BEEV {
  * the vector corresponds to bit 0 -- the low-order bit.
  ********************************************************************/
 
-  using simplifier::constantBitP::FixedBits;
+using simplifier::constantBitP::FixedBits;
 
 #define BBNodeVec vector<BBNode>
 #define BBNodeVecMap map<ASTNode, vector<BBNode> >
@@ -123,6 +123,7 @@ void BitBlaster<BBNode,BBNodeManagerT>::updateForm(const ASTNode&n, BBNode& bb,
         v.reserve(1);
         v.push_back(bb);
         bb = v[0];
+        updateTerm(n, v, support);
 }
 
 template <class BBNode, class BBNodeManagerT>
@@ -491,9 +492,21 @@ const BBNodeVec BitBlaster<BBNode,BBNodeManagerT>::BBTerm(const ASTNode& term, B
        if (debug_do_check)
                check(result, term);
 
+       updateTerm(term,result,support);
        return (BBTermMemo[term] = result);
 }
 
+template <class BBNode, class BBNodeManagerT>
+const BBNode BitBlaster<BBNode,BBNodeManagerT>::BBForm(const ASTNode& form)
+{
+    BBNodeSet support;
+    BBNode r= BBForm(form,support);
+    vector<BBNode> v;
+    v.insert(v.end(), support.begin(), support.end());
+    v.push_back(r);
+    return nf->CreateNode(AND,v);
+}
+
 // bit blast a formula (boolean term).  Result is one bit wide,
 template <class BBNode, class BBNodeManagerT>
 const BBNode BitBlaster<BBNode,BBNodeManagerT>::BBForm(const ASTNode& form, BBNodeSet& support) {
@@ -588,6 +601,8 @@ const BBNode BitBlaster<BBNode,BBNodeManagerT>::BBForm(const ASTNode& form, BBNo
        if (debug_do_check)
                check(result, form);
 
+       updateForm(form,result,support);
+
        return (BBFormMemo[form] = result);
 }
 

diff --git a/src/to-sat/BitBlaster.h b/src/to-sat/BitBlaster.h
index 7e03456c30f70b927bf12d0cd29ea1ba92192d5b..6278c1b1a612546ed5a6ab844633f4d4fa95bec1 100644 (file)
--- a/src/to-sat/BitBlaster.h
+++ b/src/to-sat/BitBlaster.h
@@ -132,6 +132,8 @@ class BitBlaster {
         void updateTerm(const ASTNode&n, vector<BBNode>& bb, set<BBNode>& support);
         void updateForm(const ASTNode&n, BBNode& bb, set<BBNode>& support);
 
+        const BBNode BBForm(const ASTNode& form, set<BBNode>& support);
+
 public:
        BBNodeManagerT* nf;
 
@@ -169,7 +171,7 @@ public:
        }
 
        //Bitblast a formula
-       const BBNode BBForm(const ASTNode& form, set<BBNode>& support);
+       const BBNode BBForm(const ASTNode& form);
 
 }; //end of class BitBlaster
 }

diff --git a/src/to-sat/ToSAT.cpp b/src/to-sat/ToSAT.cpp
index 9fba030cbf1ad55b952b076e4c3a6a77159af035..3c58272deef4f856c08eb0d6a537cb7db21d0f72 100644 (file)
--- a/src/to-sat/ToSAT.cpp
+++ b/src/to-sat/ToSAT.cpp
@@ -347,9 +347,7 @@ namespace BEEV
     {
         BBNodeManagerASTNode nm(bm);
         BitBlaster<ASTNode,BBNodeManagerASTNode> BB(&nm);
-       set<ASTNode> set;
-       BBFormula = BB.BBForm(input,set);
-       assert(set.size() == 0); // doesn't yet work.
+       BBFormula = BB.BBForm(input);
     }
 
     bm->ASTNodeStats("after bitblasting: ", BBFormula);