From e89b48215fa5b3c2249870f460e3dfca65a11a56 Mon Sep 17 00:00:00 2001 From: trevor_hansen Date: Mon, 5 Jul 2010 13:26:19 +0000 Subject: [PATCH] More getting ready for constant bit propagation. This code doesn't run, so nothing should change. git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@926 e59a4935-1847-0410-ae03-e826735625c1 --- src/AST/RunTimes.cpp | 2 +- src/AST/RunTimes.h | 3 +- src/STPManager/STP.cpp | 60 +++++++++++++++++-- src/main/main.cpp | 8 ++- .../constantBitP/ConstantBitPropagation.h | 9 ++- src/to-sat/AIG/ToSATAIG.h | 16 +++-- src/to-sat/BitBlaster.cpp | 17 +++++- src/to-sat/BitBlaster.h | 4 +- src/to-sat/ToSAT.cpp | 4 +- 9 files changed, 104 insertions(+), 19 deletions(-) diff --git a/src/AST/RunTimes.cpp b/src/AST/RunTimes.cpp index d8efe42..d08383a 100644 --- 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 fbf686b..59ced64 100644 --- 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 5fe9d26..e4e942b 100644 --- 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 678861c..04098e7 100644 --- 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 3b246d3..745e907 100644 --- a/src/simplifier/constantBitP/ConstantBitPropagation.h +++ b/src/simplifier/constantBitP/ConstantBitPropagation.h @@ -6,6 +6,7 @@ #include #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 d09176f..588f4ec 100644 --- 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 bb(&mgr); - set support; + BitBlaster 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 8387083..a62233e 100644 --- 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 #define BBNodeVecMap map > @@ -123,6 +123,7 @@ void BitBlaster::updateForm(const ASTNode&n, BBNode& bb, v.reserve(1); v.push_back(bb); bb = v[0]; + updateTerm(n, v, support); } template @@ -491,9 +492,21 @@ const BBNodeVec BitBlaster::BBTerm(const ASTNode& term, B if (debug_do_check) check(result, term); + updateTerm(term,result,support); return (BBTermMemo[term] = result); } +template +const BBNode BitBlaster::BBForm(const ASTNode& form) +{ + BBNodeSet support; + BBNode r= BBForm(form,support); + vector 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 const BBNode BitBlaster::BBForm(const ASTNode& form, BBNodeSet& support) { @@ -588,6 +601,8 @@ const BBNode BitBlaster::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 7e03456..6278c1b 100644 --- a/src/to-sat/BitBlaster.h +++ b/src/to-sat/BitBlaster.h @@ -132,6 +132,8 @@ class BitBlaster { void updateTerm(const ASTNode&n, vector& bb, set& support); void updateForm(const ASTNode&n, BBNode& bb, set& support); + const BBNode BBForm(const ASTNode& form, set& support); + public: BBNodeManagerT* nf; @@ -169,7 +171,7 @@ public: } //Bitblast a formula - const BBNode BBForm(const ASTNode& form, set& 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 9fba030..3c58272 100644 --- a/src/to-sat/ToSAT.cpp +++ b/src/to-sat/ToSAT.cpp @@ -347,9 +347,7 @@ namespace BEEV { BBNodeManagerASTNode nm(bm); BitBlaster BB(&nm); - set set; - BBFormula = BB.BBForm(input,set); - assert(set.size() == 0); // doesn't yet work. + BBFormula = BB.BBForm(input); } bm->ASTNodeStats("after bitblasting: ", BBFormula); -- 2.47.3