From: trevor_hansen Date: Wed, 2 Feb 2011 05:39:54 +0000 (+0000) Subject: Improvement. Use ABC's CNF converter by default when solving array problems using... X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=3d6b33fa13f4f6f7b1c78e6bdfc797cd0636671a;p=francis%2Fstp.git Improvement. Use ABC's CNF converter by default when solving array problems using minisat. git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1114 e59a4935-1847-0410-ae03-e826735625c1 --- diff --git a/src/STPManager/STP.cpp b/src/STPManager/STP.cpp index 7b53c9d..e1ea855 100644 --- a/src/STPManager/STP.cpp +++ b/src/STPManager/STP.cpp @@ -15,6 +15,7 @@ #include "../sat/SimplifyingMinisat.h" #include "../sat/MinisatCore.h" #include "../sat/CryptoMinisat.h" +#include namespace BEEV { @@ -169,8 +170,8 @@ namespace BEEV { bm->start_abstracting = false; bm->TermsAlreadySeenMap_Clear(); do - { - inputToSAT = simplified_solved_InputToSAT; + { + inputToSAT = simplified_solved_InputToSAT; if(bm->UserFlags.optimize_flag) { @@ -194,7 +195,7 @@ namespace BEEV { bm->ASTNodeStats("after simplification: ", simplified_solved_InputToSAT); } - + // The word level solver uses the simplifier to apply the rewrites it makes, // without optimisations enabled. It will enter infinite loops on some input. // Instead it could use the apply function of the substitution map, but it @@ -205,8 +206,8 @@ namespace BEEV { bvsolver->TopLevelBVSolve(simplified_solved_InputToSAT); bm->ASTNodeStats("after solving: ", simplified_solved_InputToSAT); } - } while (inputToSAT != simplified_solved_InputToSAT); - + } while (inputToSAT != simplified_solved_InputToSAT); + bm->ASTNodeStats("After SimplifyWrites_Inplace: ", simplified_solved_InputToSAT); @@ -273,83 +274,92 @@ namespace BEEV { if(bm->UserFlags.stats_flag) simp->printCacheStatus(); + const bool useAIGToCNF = !arrayops || !bm->UserFlags.arrayread_refinement_flag || bm->UserFlags.solver_to_use == UserDefinedFlags::MINISAT_SOLVER; + const bool maybeRefinement = arrayops && bm->UserFlags.arrayread_refinement_flag; - // If it doesn't contain array operations, use ABC's CNF generation. - if (!arrayops || !bm->UserFlags.arrayread_refinement_flag) - { - simplifier::constantBitP::ConstantBitPropagation* cb = NULL; + simplifier::constantBitP::ConstantBitPropagation* cb = NULL; + std::auto_ptr cleaner; 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,simplified_solved_InputToSAT); + { + bm->ASTNodeStats("Before Constant Bit Propagation begins: ", + simplified_solved_InputToSAT); - bm->GetRunTimes()->stop(RunTimes::ConstantBitPropagation); + bm->GetRunTimes()->start(RunTimes::ConstantBitPropagation); + cb = new simplifier::constantBitP::ConstantBitPropagation(simp, bm->defaultNodeFactory,simplified_solved_InputToSAT); + cleaner.reset(cb); + bm->GetRunTimes()->stop(RunTimes::ConstantBitPropagation); - if (cb->isUnsatisfiable()) - simplified_solved_InputToSAT = bm->ASTFalse; - } + if (cb->isUnsatisfiable()) + simplified_solved_InputToSAT = bm->ASTFalse; + } ToSATAIG toSATAIG(bm,cb); + ToSATBase* satBase = useAIGToCNF? ((ToSAT*)&toSATAIG) : tosat; + + // If it doesn't contain array operations, use ABC's CNF generation. res = Ctr_Example->CallSAT_ResultCheck(NewSolver, simplified_solved_InputToSAT, orig_input, - &toSATAIG - ); - - } - else - { - res = - Ctr_Example->CallSAT_ResultCheck(NewSolver, - simplified_solved_InputToSAT, - orig_input, - tosat - ); - - } + satBase, + maybeRefinement); if (SOLVER_UNDECIDED != res) { - CountersAndStats("print_func_stats", bm); + // If the aig converter knows that it is never going to be called again, + // it deletes the constant bit stuff before calling the SAT solver. + if (toSATAIG.cbIsDestructed()) + cleaner.release(); + + CountersAndStats("print_func_stats", bm); return res; } assert(arrayops); // should only go to abstraction refinement if there are array ops. assert(bm->UserFlags.arrayread_refinement_flag); // Refinement must be enabled too. + // Unfortunately how I implemented the incremental CNF generator in ABC means that + // cryptominisat and simplifying minisat may simplify away variables that we later need. + res = Ctr_Example->SATBased_ArrayReadRefinement(NewSolver, simplified_solved_InputToSAT, orig_input, - tosat); + satBase); if (SOLVER_UNDECIDED != res) { - CountersAndStats("print_func_stats", bm); + if (toSATAIG.cbIsDestructed()) + cleaner.release(); + + CountersAndStats("print_func_stats", bm); return res; } res = - Ctr_Example->SATBased_ArrayWriteRefinement(NewSolver, orig_input,tosat); + Ctr_Example->SATBased_ArrayWriteRefinement(NewSolver, orig_input,satBase); if (SOLVER_UNDECIDED != res) { - CountersAndStats("print_func_stats", bm); + if (toSATAIG.cbIsDestructed()) + cleaner.release(); + + CountersAndStats("print_func_stats", bm); return res; } res = Ctr_Example->SATBased_ArrayReadRefinement(NewSolver, simplified_solved_InputToSAT, - orig_input,tosat); + orig_input, + satBase); if (SOLVER_UNDECIDED != res) { - CountersAndStats("print_func_stats", bm); + if (toSATAIG.cbIsDestructed()) + cleaner.release(); + + + CountersAndStats("print_func_stats", bm); return res; } diff --git a/src/absrefine_counterexample/AbsRefine_CounterExample.h b/src/absrefine_counterexample/AbsRefine_CounterExample.h index efd2e91..4edefcd 100644 --- a/src/absrefine_counterexample/AbsRefine_CounterExample.h +++ b/src/absrefine_counterexample/AbsRefine_CounterExample.h @@ -124,7 +124,8 @@ namespace BEEV CallSAT_ResultCheck(SATSolver& SatSolver, const ASTNode& modified_input, const ASTNode& original_input, - ToSATBase* tosat); + ToSATBase* tosat, + bool refinement); //creates array write axiom only for the input term or formula, if //necessary. If there are no axioms to produce then it simply diff --git a/src/absrefine_counterexample/AbstractionRefinement.cpp b/src/absrefine_counterexample/AbstractionRefinement.cpp index eb419e8..ffd7641 100644 --- a/src/absrefine_counterexample/AbstractionRefinement.cpp +++ b/src/absrefine_counterexample/AbstractionRefinement.cpp @@ -90,10 +90,12 @@ namespace BEEV assert ((SYMBOL == arrsym.GetKind() || BVCONST == arrsym.GetKind())); read_node_symbols.push_back(arrsym); + jKind.push_back(listOfIndices[i].GetKind()); concreteIndexes.push_back(TermToConstTermUsingModel(the_index)); concreteValues.push_back(TermToConstTermUsingModel(arrsym)); + } //loop over the list of indices for the array and create LA, @@ -152,7 +154,8 @@ namespace BEEV res2 = CallSAT_ResultCheck(SatSolver, FalseAxioms, original_input, - tosat); + tosat, + true); FalseAxiomsVec.clear(); if (SOLVER_UNDECIDED != res2) @@ -172,9 +175,11 @@ namespace BEEV RemainingAxioms); bm->GetRunTimes()->stop(RunTimes::ArrayReadRefinement); return CallSAT_ResultCheck(SatSolver, RemainingAxioms, original_input, - tosat); + tosat,true); } + bm->GetRunTimes()->stop(RunTimes::ArrayReadRefinement); + return SOLVER_UNDECIDED; } //end of SATBased_ArrayReadRefinement @@ -220,7 +225,7 @@ namespace BEEV writeAxiom = (FalseAxioms.size() != 1) ? bm->CreateNode(AND, FalseAxioms) : FalseAxioms[0]; bm->ASTNodeStats("adding false writeaxiom to SAT: ", writeAxiom); - res2 = CallSAT_ResultCheck(SatSolver, writeAxiom, original_input, tosat); + res2 = CallSAT_ResultCheck(SatSolver, writeAxiom, original_input, tosat,true); } if (SOLVER_UNDECIDED != res2) @@ -237,7 +242,7 @@ namespace BEEV res2 = CallSAT_ResultCheck(SatSolver, writeAxiom, original_input, - tosat); + tosat, true); } return res2; } //end of SATBased_ArrayWriteRefinement diff --git a/src/absrefine_counterexample/CounterExample.cpp b/src/absrefine_counterexample/CounterExample.cpp index 2edeefe..d40c7fb 100644 --- a/src/absrefine_counterexample/CounterExample.cpp +++ b/src/absrefine_counterexample/CounterExample.cpp @@ -169,7 +169,7 @@ namespace BEEV } else { - return val; + return val; } } @@ -239,8 +239,6 @@ namespace BEEV } else { - cerr << "TermToConstTermUsingModel: termITE: " - "value of conditional is wrong: " << condcompute << endl; FatalError(" TermToConstTermUsingModel: termITE: " "cannot compute ITE conditional against model: ", term); } @@ -302,8 +300,6 @@ namespace BEEV } else { - cerr << "TermToConstTermUsingModel: termITE: " - << "value of conditional is wrong: " << condcompute << endl; FatalError(" TermToConstTermUsingModel: termITE: cannot " "compute ITE conditional against model: ", term); } @@ -320,11 +316,9 @@ namespace BEEV ASTNode ff = TermToConstTermUsingModel(*it, ArrayReadFlag); o.push_back(ff); } - output = bm->hashingNodeFactory->CreateTerm(k, term.GetValueWidth(), o); - //output is a CONST expression. compute its value and store it - //in the CounterExampleMap - output = simp->BVConstEvaluator(output); - break; + + output = NonMemberBVConstEvaluator(term.GetSTPMgr() , k, o, term.GetValueWidth()); + break; } } @@ -414,7 +408,6 @@ namespace BEEV ASTNode AbsRefine_CounterExample::ComputeFormulaUsingModel(const ASTNode& form) { - const ASTNode& in = form; const Kind k = form.GetKind(); if (!(is_Form_kind(k) && BOOLEAN_TYPE == form.GetType())) { @@ -423,10 +416,10 @@ namespace BEEV } //cerr << "Input to ComputeFormulaUsingModel:" << form << endl; - ASTNodeMap::iterator it1; + ASTNodeMap::const_iterator it1; if ((it1 = ComputeFormulaMap.find(form)) != ComputeFormulaMap.end()) { - ASTNode res = it1->second; + const ASTNode& res = it1->second; if (ASTTrue == res || ASTFalse == res) { return res; @@ -482,11 +475,11 @@ namespace BEEV for (ASTVec::const_iterator it = form.begin(), itend = form.end(); it != itend; it++) - { + { children.push_back(TermToConstTermUsingModel(*it, false)); } - output = simp->BVConstEvaluator(bm->CreateNode(k, children)); + output = NonMemberBVConstEvaluator(form.GetSTPMgr() , k, children, form.GetValueWidth()); //evaluate formula to false if bvdiv execption occurs while //counterexample is being checked during refinement. @@ -517,7 +510,7 @@ namespace BEEV children.push_back( ComputeFormulaUsingModel(*it)); } - output = simp->BVConstEvaluator(bm->CreateNode(k, children)); + output = NonMemberBVConstEvaluator(form.GetSTPMgr() , k, children, form.GetValueWidth()); //evaluate formula to false if bvdiv execption occurs while //counterexample is being checked during refinement. @@ -557,7 +550,6 @@ namespace BEEV break; } - //cout << "ComputeFormulaUsingModel output is:" << output << endl; assert(ASTUndefined != output); assert(output.isConstant()); ComputeFormulaMap[form] = output; @@ -864,10 +856,10 @@ namespace BEEV SOLVER_RETURN_TYPE AbsRefine_CounterExample::CallSAT_ResultCheck(SATSolver& SatSolver, - const ASTNode& modified_input, const ASTNode& original_input, ToSATBase* tosat) + const ASTNode& modified_input, const ASTNode& original_input, ToSATBase* tosat, bool refinement) { - bool sat = tosat->CallSAT(SatSolver, modified_input); + bool sat = tosat->CallSAT(SatSolver, modified_input, refinement); if (!sat) { diff --git a/src/to-sat/AIG/BBNodeManagerAIG.cpp b/src/to-sat/AIG/BBNodeManagerAIG.cpp index 60c1ca7..d24e5c7 100644 --- a/src/to-sat/AIG/BBNodeManagerAIG.cpp +++ b/src/to-sat/AIG/BBNodeManagerAIG.cpp @@ -3,94 +3,8 @@ namespace BEEV { - void - BBNodeManagerAIG::toCNF(const BBNodeAIG& top, Cnf_Dat_t*& cnfData, ToSATBase::ASTNodeToSATVar& nodeToVar, const UserDefinedFlags& uf) - { - assert(cnfData == NULL); - - Aig_ObjCreatePo(aigMgr, top.n); - Aig_ManCleanup(aigMgr); // remove nodes not connected to the PO. - Aig_ManCheck(aigMgr); // check that AIG looks ok. - - assert(Aig_ManPoNum(aigMgr) == 1); - - // UseZeroes gives assertion errors. - // Rewriting is sometimes very slow. Can it be configured to be faster? - // What about refactoring??? - - int nodeCount = aigMgr->nObjs[AIG_OBJ_AND]; - if (uf.stats_flag) - cerr << "Nodes before AIG rewrite:" << nodeCount <nObjs[AIG_OBJ_AND] < 5000) - { - Dar_LibStart(); - Aig_Man_t * pTemp; - Dar_RwrPar_t Pars, * pPars = &Pars; - Dar_ManDefaultRwrParams( pPars ); - - // Assertion errors occur with this enabled. - // pPars->fUseZeros = 1; - - // For mul63bit.smt2 with iterations =3 & nCutsMax = 8 - // CNF generation was taking 139 seconds, solving 10 seconds. - - // With nCutsMax =2, CNF generation takes 16 seconds, solving 10 seconds. - // The rewriting doesn't remove as many nodes of course.. - int iterations = 3; - - for (int i=0; i < iterations;i++) - { - aigMgr = Aig_ManDup( pTemp = aigMgr, 0 ); - Aig_ManStop( pTemp ); - Dar_ManRewrite( aigMgr, pPars ); - - aigMgr = Aig_ManDup( pTemp = aigMgr, 0 ); - Aig_ManStop( pTemp ); - - if (uf.stats_flag) - cerr << "After rewrite [" << i << "] nodes:" << aigMgr->nObjs[AIG_OBJ_AND] << endl; - - if (nodeCount == aigMgr->nObjs[AIG_OBJ_AND]) - break; - } - } - if (aigMgr->nObjs[AIG_OBJ_AND] < 2000000) - cnfData = Cnf_Derive(aigMgr, 0); - else - cnfData = Cnf_DeriveSimple(aigMgr, 0); - - BBNodeManagerAIG::SymbolToBBNode::const_iterator it; - - assert(nodeToVar.size() ==0); - - // Each symbol maps to a vector of CNF variables. - for (it = symbolToBBNode.begin(); it != symbolToBBNode.end(); it++) - { - const ASTNode& n = it->first; - const vector &b = it->second; - assert (nodeToVar.find(n) == nodeToVar.end()); - - const int width = (n.GetType() == BOOLEAN_TYPE) ? 1: n.GetValueWidth(); - - // INT_MAX for parts of symbols that didn't get encoded. - vector v(width, ~((unsigned) 0)); +} - for (unsigned i = 0; i < b.size(); i++) - { - if (!b[i].IsNull()) - { - Aig_Obj_t * pObj; - pObj = (Aig_Obj_t*)Vec_PtrEntry( aigMgr->vPis, b[i].symbol_index ); - v[i] = cnfData->pVarNums[pObj->Id]; - } - } - nodeToVar.insert(make_pair(n, v)); - } - assert(cnfData != NULL); - } -} diff --git a/src/to-sat/AIG/BBNodeManagerAIG.h b/src/to-sat/AIG/BBNodeManagerAIG.h index 451199b..d176f88 100644 --- a/src/to-sat/AIG/BBNodeManagerAIG.h +++ b/src/to-sat/AIG/BBNodeManagerAIG.h @@ -31,12 +31,14 @@ extern vector _empty_BBNodeAIGVec; // Creates AIG nodes with ABC and wraps them in BBNodeAIG's. class BBNodeManagerAIG { +public: Aig_Man_t *aigMgr; // Map from symbols to their AIG nodes. typedef map > SymbolToBBNode; - SymbolToBBNode symbolToBBNode; + SymbolToBBNode symbolToBBNode; +private: // AIGs can only take two parameters. This makes a log_2 height // tower of varadic inputs. Aig_Obj_t * makeTower(Aig_Obj_t * (*t)(Aig_Man_t *, Aig_Obj_t *, @@ -107,13 +109,11 @@ public: return BBNodeAIG(Aig_ManConst0(aigMgr)); } - void toCNF(const BBNodeAIG& top, Cnf_Dat_t*& cnfData, ToSATBase::ASTNodeToSATVar& nodeToVar, const UserDefinedFlags& uf); - // The same symbol always needs to return the same AIG node, // if it doesn't you will get the wrong answer. BBNodeAIG CreateSymbol(const ASTNode& n, unsigned i) { - assert(n.GetKind() == SYMBOL); + assert(n.GetKind() == SYMBOL); // booleans have width 0. const unsigned width = std::max((unsigned)1, n.GetValueWidth()); diff --git a/src/to-sat/AIG/ToCNFAIG.cpp b/src/to-sat/AIG/ToCNFAIG.cpp new file mode 100644 index 0000000..ee36150 --- /dev/null +++ b/src/to-sat/AIG/ToCNFAIG.cpp @@ -0,0 +1,138 @@ +#include "ToCNFAIG.h" + +namespace BEEV +{ + + + +// Can it only add in the new variables somehow?? +void addVariables(BBNodeManagerAIG& mgr, Cnf_Dat_t*& cnfData , ToSATBase::ASTNodeToSATVar& nodeToVar) +{ + BBNodeManagerAIG::SymbolToBBNode::const_iterator it; + // Each symbol maps to a vector of CNF variables. + for (it = mgr.symbolToBBNode.begin(); it != mgr.symbolToBBNode.end(); it++) { + const ASTNode& n = it->first; + const vector &b = it->second; + + const int width = (n.GetType() == BOOLEAN_TYPE) ? 1 : n.GetValueWidth(); + + // INT_MAX for parts of symbols that didn't get encoded. + vector v(width, ~((unsigned) 0)); + + for (unsigned i = 0; i < b.size(); i++) { + if (!b[i].IsNull()) { + Aig_Obj_t * pObj; + pObj = (Aig_Obj_t*) Vec_PtrEntry(mgr.aigMgr->vPis, + b[i].symbol_index); + v[i] = cnfData->pVarNums[pObj->Id]; + } + } + nodeToVar.insert(make_pair(n, v)); + } + +} + + +// When we need abstraction refinement. +void ToCNFAIG::toCNF_renter(const BBNodeAIG& top, Cnf_Dat_t*& cnfData, + ToSATBase::ASTNodeToSATVar& nodeToVar, BBNodeManagerAIG& mgr) { + assert(priorCnfData != NULL); + Aig_ObjCreatePo(mgr.aigMgr, top.n); // A new PO. + + cnfData = Cnf_DeriveSimple_Additional(mgr.aigMgr, priorCnfData); + Cnf_DataFree(priorCnfData); + priorCnfData = cnfData; + + addVariables( mgr, cnfData , nodeToVar); +} + +void ToCNFAIG::toCNF(const BBNodeAIG& top, Cnf_Dat_t*& cnfData, + ToSATBase::ASTNodeToSATVar& nodeToVar, + bool needAbsRef, BBNodeManagerAIG& mgr) { + assert(cnfData == NULL); + + Aig_ObjCreatePo(mgr.aigMgr, top.n); + if (!needAbsRef) { + Aig_ManCleanup( mgr.aigMgr); // remove nodes not connected to the PO. + } + Aig_ManCheck( mgr.aigMgr); // check that AIG looks ok. + + assert(Aig_ManPoNum(mgr.aigMgr) == 1); + + // UseZeroes gives assertion errors. + // Rewriting is sometimes very slow. Can it be configured to be faster? + // What about refactoring??? + + int nodeCount = mgr.aigMgr->nObjs[AIG_OBJ_AND]; + if (uf.stats_flag) + cerr << "Nodes before AIG rewrite:" << nodeCount << endl; + + if (!needAbsRef && uf.enable_AIG_rewrites_flag + && mgr.aigMgr->nObjs[AIG_OBJ_AND] < 5000) { + Dar_LibStart(); + Aig_Man_t * pTemp; + Dar_RwrPar_t Pars, *pPars = &Pars; + Dar_ManDefaultRwrParams(pPars); + + // Assertion errors occur with this enabled. + // pPars->fUseZeros = 1; + + // For mul63bit.smt2 with iterations =3 & nCutsMax = 8 + // CNF generation was taking 139 seconds, solving 10 seconds. + + // With nCutsMax =2, CNF generation takes 16 seconds, solving 10 seconds. + // The rewriting doesn't remove as many nodes of course.. + int iterations = 3; + + for (int i = 0; i < iterations; i++) { + mgr.aigMgr = Aig_ManDup(pTemp = mgr.aigMgr, 0); + Aig_ManStop(pTemp); + Dar_ManRewrite(mgr.aigMgr, pPars); + + mgr.aigMgr = Aig_ManDup(pTemp = mgr.aigMgr, 0); + Aig_ManStop(pTemp); + + if (uf.stats_flag) + cerr << "After rewrite [" << i << "] nodes:" + << mgr.aigMgr->nObjs[AIG_OBJ_AND] << endl; + + if (nodeCount == mgr.aigMgr->nObjs[AIG_OBJ_AND]) + break; + } + } + if (!needAbsRef && mgr.aigMgr->nObjs[AIG_OBJ_AND] < 2000000) { + cnfData = Cnf_Derive(mgr.aigMgr, 0); + } else { + cnfData = Cnf_DeriveSimple(mgr.aigMgr, 0); + } + + BBNodeManagerAIG::SymbolToBBNode::const_iterator it; + + assert(nodeToVar.size() == 0); + + //todo. cf. with addvariables above... + // Each symbol maps to a vector of CNF variables. + for (it = mgr.symbolToBBNode.begin(); it != mgr.symbolToBBNode.end(); it++) { + const ASTNode& n = it->first; + const vector &b = it->second; + assert(nodeToVar.find(n) == nodeToVar.end()); + + const int width = (n.GetType() == BOOLEAN_TYPE) ? 1 : n.GetValueWidth(); + + // INT_MAX for parts of symbols that didn't get encoded. + vector v(width, ~((unsigned) 0)); + + for (unsigned i = 0; i < b.size(); i++) { + if (!b[i].IsNull()) { + Aig_Obj_t * pObj; + pObj = (Aig_Obj_t*) Vec_PtrEntry(mgr.aigMgr->vPis, + b[i].symbol_index); + v[i] = cnfData->pVarNums[pObj->Id]; + } + } + + nodeToVar.insert(make_pair(n, v)); + } + assert(cnfData != NULL); +} +}; diff --git a/src/to-sat/AIG/ToCNFAIG.h b/src/to-sat/AIG/ToCNFAIG.h new file mode 100644 index 0000000..0a2b8cd --- /dev/null +++ b/src/to-sat/AIG/ToCNFAIG.h @@ -0,0 +1,51 @@ +#ifndef TOCNFAIG_H_ +#define TOCNFAIG_H_ + +#include "../../extlib-abc/aig.h" +#include "../../extlib-abc/cnf_short.h" +#include "../../extlib-abc/dar.h" +#include "../ToSATBase.h" +#include "BBNodeManagerAIG.h" + +namespace BEEV { + +class ToCNFAIG { + Cnf_Dat_t* priorCnfData; + + // no copy. no assignment. + ToCNFAIG& operator = (const ToCNFAIG& other); + ToCNFAIG(const ToCNFAIG& other); + + const UserDefinedFlags& uf; + + +public: + ToCNFAIG(const UserDefinedFlags& _uf): + uf(_uf) + { + priorCnfData = NULL; + } + + ~ToCNFAIG() { + if (NULL != priorCnfData) + Cnf_DataFree(priorCnfData); + } + + void toCNF(const BBNodeAIG& top, Cnf_Dat_t*& cnfData, + ToSATBase::ASTNodeToSATVar& nodeToVar, + bool needAbsRef, BBNodeManagerAIG& _mgr); + + // assumes the above function was called first. + void toCNF_renter(const BBNodeAIG& top, Cnf_Dat_t*& cnfData, + ToSATBase::ASTNodeToSATVar& nodeToVar, BBNodeManagerAIG& _mgr); + + // The piror must be set before toCNF_reenter is called. + void setPrior(Cnf_Dat_t* prior) + { + priorCnfData = prior; + } + +}; + +} +#endif /* TOCNFAIG_H_ */ diff --git a/src/to-sat/AIG/ToSATAIG.cpp b/src/to-sat/AIG/ToSATAIG.cpp index 1578115..2d42c37 100644 --- a/src/to-sat/AIG/ToSATAIG.cpp +++ b/src/to-sat/AIG/ToSATAIG.cpp @@ -5,37 +5,39 @@ namespace BEEV { - // Can not be used with abstraction refinement. bool - ToSATAIG::CallSAT(SATSolver& satSolver, const ASTNode& input) + ToSATAIG::CallSAT(SATSolver& satSolver, const ASTNode& input, bool needAbsRef) { if (cb != NULL && cb->isUnsatisfiable()) return false; - BBNodeManagerAIG mgr; - Simplifier *simp = new Simplifier(bm); - BitBlaster *bb = new BitBlaster(&mgr,cb,simp,bm->defaultNodeFactory,&bm->UserFlags); + if (simp == NULL) + simp = new Simplifier(bm); - // Even if we cleared the tables we could still have the hash table's buckets sitting around. - delete simp; - simp = NULL; + if (bb== NULL) + bb = new BitBlaster(&mgr,cb,simp,bm->defaultNodeFactory,&bm->UserFlags); bm->GetRunTimes()->start(RunTimes::BitBlasting); BBNodeAIG BBFormula = bb->BBForm(input); bm->GetRunTimes()->stop(RunTimes::BitBlasting); - delete bb; - bb = NULL; - //Clear out all the constant bit stuff before sending the SAT. - if (cb != NULL) - { - delete cb; - cb = NULL; - } + // It's not incremental. + delete cb; + cb = NULL; + bb->cb = NULL; + + if (!needAbsRef) + { + delete simp; + simp = NULL; + delete bb; + bb = NULL; + } - assert(satSolver.nVars() ==0); + if (first) + assert(satSolver.nVars() ==0); // Oddly the substitution map, which is necessary to output a model is kept in the simplifier. // The bitblaster should never enter anything into the solver map. @@ -44,18 +46,41 @@ namespace BEEV Cnf_Dat_t* cnfData = NULL; bm->GetRunTimes()->start(RunTimes::CNFConversion); - mgr.toCNF(BBFormula, cnfData, nodeToSATVar,bm->UserFlags); + if (first) + { + toCNF.toCNF(BBFormula, cnfData, nodeToSATVar,needAbsRef,mgr); + } + else + { + assert(needAbsRef); + toCNF.toCNF_renter(BBFormula, cnfData, nodeToSATVar,mgr); + } bm->GetRunTimes()->stop(RunTimes::CNFConversion); - // Free the memory in the AIGs. - BBFormula = BBNodeAIG(); // null node - mgr.stop(); + if (!needAbsRef) + { + // Free the memory in the AIGs. + BBFormula = BBNodeAIG(); // null node + mgr.stop(); + } + + if (bm->UserFlags.output_CNF_flag) + { + stringstream fileName; + fileName << "output_" << CNFFileNameCounter++ << ".cnf"; + Cnf_DataWriteIntoFile(cnfData, (char*)fileName.str().c_str(), 0); + } + first = false; + bm->GetRunTimes()->start(RunTimes::SendingToSAT); - for (int i = 0; i < cnfData->nVars; i++) + // Create a new sat variable for each of the variables in the CNF. + int satV = satSolver.nVars(); + for (int i = 0; i < cnfData->nVars - satV ; i++) satSolver.newVar(); + SATSolver::vec_literals satSolverClause; for (int i = 0; i < cnfData->nClauses; i++) { @@ -64,7 +89,12 @@ namespace BEEV + 1]; pLit < pStop; pLit++) { SATSolver::Var var = (*pLit) >> 1; - assert(var < satSolver.nVars()); + if (!(var < satSolver.nVars())) + { + cerr << var << " "; + cerr << satSolver.nVars(); + exit(1); + } Minisat::Lit l = SATSolver::mkLit(var, (*pLit) & 1); satSolverClause.push(l); } @@ -75,14 +105,19 @@ namespace BEEV } bm->GetRunTimes()->stop(RunTimes::SendingToSAT); - if (bm->UserFlags.output_CNF_flag) - Cnf_DataWriteIntoFile(cnfData, "output_0.cnf", 0); - if (bm->UserFlags.output_bench_flag) cerr << "Converting to CNF via ABC's AIG package can't yet print out bench format" << endl; - Cnf_ClearMemory(); - Cnf_DataFree(cnfData); + if (!needAbsRef) + { + Cnf_ClearMemory(); + Cnf_DataFree(cnfData); + cnfData = NULL; + } + else + { + toCNF.setPrior(cnfData); + } if (bm->UserFlags.exit_after_CNF) { @@ -101,4 +136,12 @@ namespace BEEV return satSolver.okay(); } + ToSATAIG::~ToSATAIG() + { + delete bb; + delete simp; + ClearAllTables(); + } + + } diff --git a/src/to-sat/AIG/ToSATAIG.h b/src/to-sat/AIG/ToSATAIG.h index 4329257..06380c8 100644 --- a/src/to-sat/AIG/ToSATAIG.h +++ b/src/to-sat/AIG/ToSATAIG.h @@ -16,11 +16,11 @@ #include "../STPManager/STPManager.h" #include "../BitBlaster.h" #include "BBNodeManagerAIG.h" +#include "ToCNFAIG.h" namespace BEEV { - // NB You can't use this with abstraction refinement!!! class ToSATAIG : public ToSATBase { private: @@ -32,20 +32,48 @@ namespace BEEV ToSATAIG& operator = (const ToSATAIG& other); ToSATAIG(const ToSATAIG& other); + int count; + bool first; + BitBlaster *bb; + int CNFFileNameCounter; + BBNodeManagerAIG mgr; + Simplifier *simp; + + ToCNFAIG toCNF; + + void init() + { + count = 0; + first = true; + bb = NULL; + CNFFileNameCounter =0; + simp = NULL; + } + public: + bool cbIsDestructed() + { + return cb == NULL; + } + + ToSATAIG(STPMgr * bm) : - ToSATBase(bm) + ToSATBase(bm), toCNF(bm->UserFlags) { cb = NULL; + init(); } ToSATAIG(STPMgr * bm, simplifier::constantBitP::ConstantBitPropagation* cb_) : - ToSATBase(bm) + ToSATBase(bm), cb(cb_), toCNF(bm->UserFlags) { cb = cb_; + init(); } + ~ToSATAIG(); + void ClearAllTables() { @@ -59,8 +87,7 @@ namespace BEEV return nodeToSATVar; } - // Can not be used with abstraction refinement. - bool CallSAT(SATSolver& satSolver, const ASTNode& input); + bool CallSAT(SATSolver& satSolver, const ASTNode& input, bool needAbsRef); }; } diff --git a/src/to-sat/ASTNode/ToSAT.cpp b/src/to-sat/ASTNode/ToSAT.cpp index 3377189..7ea4b40 100644 --- a/src/to-sat/ASTNode/ToSAT.cpp +++ b/src/to-sat/ASTNode/ToSAT.cpp @@ -331,7 +331,7 @@ namespace BEEV //can return one of 3 values, SOLVER_VALID, SOLVER_INVALID or //SOLVER_UNDECIDED bool ToSAT::CallSAT(SATSolver& SatSolver, - const ASTNode& input) + const ASTNode& input, bool refinement) { bm->GetRunTimes()->start(RunTimes::BitBlasting); diff --git a/src/to-sat/ASTNode/ToSAT.h b/src/to-sat/ASTNode/ToSAT.h index acbba5e..eae5e7e 100644 --- a/src/to-sat/ASTNode/ToSAT.h +++ b/src/to-sat/ASTNode/ToSAT.h @@ -93,7 +93,7 @@ namespace BEEV // Bitblasts, CNF conversion and calls toSATandSolve() bool CallSAT(SATSolver& SatSolver, - const ASTNode& input); + const ASTNode& input, bool refinement); ASTNodeToSATVar& SATVar_to_SymbolIndexMap() { diff --git a/src/to-sat/BitBlaster.h b/src/to-sat/BitBlaster.h index e37f466..f20c7f2 100644 --- a/src/to-sat/BitBlaster.h +++ b/src/to-sat/BitBlaster.h @@ -38,8 +38,6 @@ class BitBlaster { BBNode BBTrue, BBFalse; - simplifier::constantBitP::ConstantBitPropagation* cb; - // Memo table for bit blasted terms. If a node has already been // bitblasted, it is mapped to a vector of Boolean formulas for // the @@ -166,6 +164,8 @@ class BitBlaster { public: + simplifier::constantBitP::ConstantBitPropagation* cb; + // Bit blast a bitvector term. The term must have a kind for a // bitvector term. Result is a ref to a vector of formula nodes // representing the boolean formula. diff --git a/src/to-sat/ToSATBase.h b/src/to-sat/ToSATBase.h index 9460606..d2378be 100644 --- a/src/to-sat/ToSATBase.h +++ b/src/to-sat/ToSATBase.h @@ -38,7 +38,7 @@ namespace BEEV void PrintOutput(SOLVER_RETURN_TYPE ret); // Bitblasts, CNF conversion and calls toSATandSolve() - virtual bool CallSAT(SATSolver& SatSolver, const ASTNode& input) =0; + virtual bool CallSAT(SATSolver& SatSolver, const ASTNode& input, bool doesAbsRef) =0; virtual ASTNodeToSATVar& SATVar_to_SymbolIndexMap()= 0;