From 710ac6af30a04a6fb36c22230e5c033fa63fde8d Mon Sep 17 00:00:00 2001 From: trevor_hansen Date: Sun, 7 Mar 2010 14:18:48 +0000 Subject: [PATCH] Cosmetic changes. * Make some methods private. * Move the contents of CallSat into ToSat * ifdef out some declarations. git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@627 e59a4935-1847-0410-ae03-e826735625c1 --- src/to-sat/CallSAT.cpp | 190 ----------------------------------------- src/to-sat/ToSAT.cpp | 175 +++++++++++++++++++++++++++++++++++++ src/to-sat/ToSAT.h | 37 +++++--- 3 files changed, 199 insertions(+), 203 deletions(-) delete mode 100644 src/to-sat/CallSAT.cpp diff --git a/src/to-sat/CallSAT.cpp b/src/to-sat/CallSAT.cpp deleted file mode 100644 index eae8831..0000000 --- a/src/to-sat/CallSAT.cpp +++ /dev/null @@ -1,190 +0,0 @@ -// -*- c++ -*- -/******************************************************************** - * AUTHORS: Vijay Ganesh - * - * BEGIN DATE: November, 2005 - * - * LICENSE: Please view LICENSE file in the home dir of this Program - ********************************************************************/ -#include "ToSAT.h" -#include "BitBlastNew.h" - -namespace BEEV -{ - //Bucketize clauses into buckets of size 1,2,...CLAUSAL_BUCKET_LIMIT - static ClauseBuckets * Sort_ClauseList_IntoBuckets(ClauseList * cl) - { - ClauseBuckets * cb = new ClauseBuckets(); - - //Sort the clauses, and bucketize by the size of the clauses - for(ClauseList::iterator it = cl->begin(), itend = cl->end(); - it!=itend; it++) - { - ClausePtr cptr = *it; - int cl_size = cptr->size(); - if(cl_size >= CLAUSAL_BUCKET_LIMIT) - { - cl_size = CLAUSAL_BUCKET_LIMIT; - } -// else -// { -// cl_size = CLAUSAL_BUCKET_LIMIT-1; -// } - - //If no clauses of size cl_size have been seen, then create a - //bucket for that size - if(cb->find(cl_size) == cb->end()) - { - ClauseList * cllist = new ClauseList(); - cllist->push_back(cptr); - (*cb)[cl_size] = cllist; - } - else - { - ClauseList * cllist = (*cb)[cl_size]; - cllist->push_back(cptr); - } - } - - return cb; - } //End of SortClauseList_IntoBuckets() - - bool ToSAT::CallSAT_On_ClauseBuckets(MINISAT::Solver& SatSolver, - ClauseBuckets * cb) - { - ClauseBuckets::iterator it = cb->begin(); - ClauseBuckets::iterator itend = cb->end(); - - bool sat = false; - for(int count=1;it!=itend;it++, count++) - { - ClauseList *cl = (*it).second; -// if(CLAUSAL_BUCKET_LIMIT == count) -// { -// sat = toSATandSolve(SatSolver,*cl, false, true); -// } -// else - { - sat = toSATandSolve(SatSolver,*cl); - } - if(!sat) - { - return sat; - } - } - return sat; - } - - - - //Call the SAT solver, and check the result before returning. This - //can return one of 3 values, SOLVER_VALID, SOLVER_INVALID or - //SOLVER_UNDECIDED - bool ToSAT::CallSAT(MINISAT::Solver& SatSolver, - const ASTNode& modified_input, - const ASTNode& original_input) - { - bm->GetRunTimes()->start(RunTimes::BitBlasting); - -#if 1 - BitBlasterNew BB(bm); - BBNodeSet set; - ASTNode BBFormula = BB.BBForm(modified_input,set); - assert(set.size() == 0); // doesn't yet work. -#else - BitBlaster BB(bm); - ASTNode BBFormula = BB.BBForm(modified_input); -#endif - - bm->ASTNodeStats("after bitblasting: ", BBFormula); - bm->GetRunTimes()->stop(RunTimes::BitBlasting); - - CNFMgr* cm = new CNFMgr(bm); - ClauseList* cl = cm->convertToCNF(BBFormula); - - ClauseList* xorcl = cm->ReturnXorClauses(); - - ClauseBuckets * cb = Sort_ClauseList_IntoBuckets(cl); - bool sat = CallSAT_On_ClauseBuckets(SatSolver, cb); - //bool sat = toSATandSolve(SatSolver, *cl); - - for (ClauseBuckets::iterator it = cb->begin(); it != cb->end(); it++) - delete it->second; - delete cb; - - if(!sat) - { - cm->DELETE(cl); - cm->DELETE(xorcl); - delete cm; - return sat; - } - -#if defined CRYPTOMINISAT || defined CRYPTOMINISAT2 - if(!xorcl->empty()) - { - sat = toSATandSolve(SatSolver, *xorcl, true); - } -#endif - - cm->DELETE(cl); - cm->DELETE(xorcl); - delete cm; - return sat; - } - - //################################################## - //################################################## - - /******************************************************************* - * Helper Functions - *******************************************************************/ - - //This function prints the output of the STP solver - void ToSAT::PrintOutput(SOLVER_RETURN_TYPE ret) - { - bool true_iff_valid = (SOLVER_VALID == ret); - - if (bm->UserFlags.print_output_flag) - { - if (bm->UserFlags.smtlib_parser_flag) - { - if (true_iff_valid && - (input_status == TO_BE_SATISFIABLE)) - { - cerr << "Warning. Expected satisfiable,"\ - " FOUND unsatisfiable" << endl; - } - else if (!true_iff_valid && - (input_status == TO_BE_UNSATISFIABLE)) - { - cerr << "Warning. Expected unsatisfiable,"\ - " FOUND satisfiable" << endl; - } - } - } - - if (true_iff_valid) - { - bm->ValidFlag = true; - if (bm->UserFlags.print_output_flag) - { - if (bm->UserFlags.smtlib_parser_flag) - cout << "unsat\n"; - else - cout << "Valid.\n"; - } - } - else - { - bm->ValidFlag = false; - if (bm->UserFlags.print_output_flag) - { - if (bm->UserFlags.smtlib_parser_flag) - cout << "sat\n"; - else - cout << "Invalid.\n"; - } - } - } //end of PrintOutput() -};//end of namespace diff --git a/src/to-sat/ToSAT.cpp b/src/to-sat/ToSAT.cpp index 4d7f9f6..d5146d2 100644 --- a/src/to-sat/ToSAT.cpp +++ b/src/to-sat/ToSAT.cpp @@ -7,6 +7,8 @@ * LICENSE: Please view LICENSE file in the home dir of this Program ********************************************************************/ #include "ToSAT.h" +#include "ToSAT.h" +#include "BitBlastNew.h" namespace BEEV { @@ -184,6 +186,179 @@ namespace BEEV return false; } //end of toSATandSolve() + //Bucketize clauses into buckets of size 1,2,...CLAUSAL_BUCKET_LIMIT + static ClauseBuckets * Sort_ClauseList_IntoBuckets(ClauseList * cl) + { + ClauseBuckets * cb = new ClauseBuckets(); + + //Sort the clauses, and bucketize by the size of the clauses + for(ClauseList::iterator it = cl->begin(), itend = cl->end(); + it!=itend; it++) + { + ClausePtr cptr = *it; + int cl_size = cptr->size(); + if(cl_size >= CLAUSAL_BUCKET_LIMIT) + { + cl_size = CLAUSAL_BUCKET_LIMIT; + } +// else +// { +// cl_size = CLAUSAL_BUCKET_LIMIT-1; +// } + + //If no clauses of size cl_size have been seen, then create a + //bucket for that size + if(cb->find(cl_size) == cb->end()) + { + ClauseList * cllist = new ClauseList(); + cllist->push_back(cptr); + (*cb)[cl_size] = cllist; + } + else + { + ClauseList * cllist = (*cb)[cl_size]; + cllist->push_back(cptr); + } + } + + return cb; + } //End of SortClauseList_IntoBuckets() + + bool ToSAT::CallSAT_On_ClauseBuckets(MINISAT::Solver& SatSolver, + ClauseBuckets * cb) + { + ClauseBuckets::iterator it = cb->begin(); + ClauseBuckets::iterator itend = cb->end(); + + bool sat = false; + for(int count=1;it!=itend;it++, count++) + { + ClauseList *cl = (*it).second; +// if(CLAUSAL_BUCKET_LIMIT == count) +// { +// sat = toSATandSolve(SatSolver,*cl, false, true); +// } +// else + { + sat = toSATandSolve(SatSolver,*cl); + } + if(!sat) + { + return sat; + } + } + return sat; + } + + + + //Call the SAT solver, and check the result before returning. This + //can return one of 3 values, SOLVER_VALID, SOLVER_INVALID or + //SOLVER_UNDECIDED + bool ToSAT::CallSAT(MINISAT::Solver& SatSolver, + const ASTNode& modified_input, + const ASTNode& original_input) + { + bm->GetRunTimes()->start(RunTimes::BitBlasting); + + + BitBlasterNew BB(bm); + BBNodeSet set; + ASTNode BBFormula = BB.BBForm(modified_input,set); + assert(set.size() == 0); // doesn't yet work. + + bm->ASTNodeStats("after bitblasting: ", BBFormula); + bm->GetRunTimes()->stop(RunTimes::BitBlasting); + + CNFMgr* cm = new CNFMgr(bm); + ClauseList* cl = cm->convertToCNF(BBFormula); + + ClauseList* xorcl = cm->ReturnXorClauses(); + + ClauseBuckets * cb = Sort_ClauseList_IntoBuckets(cl); + bool sat = CallSAT_On_ClauseBuckets(SatSolver, cb); + //bool sat = toSATandSolve(SatSolver, *cl); + + for (ClauseBuckets::iterator it = cb->begin(); it != cb->end(); it++) + delete it->second; + delete cb; + + if(!sat) + { + cm->DELETE(cl); + cm->DELETE(xorcl); + delete cm; + return sat; + } + +#if defined CRYPTOMINISAT || defined CRYPTOMINISAT2 + if(!xorcl->empty()) + { + sat = toSATandSolve(SatSolver, *xorcl, true); + } +#endif + + cm->DELETE(cl); + cm->DELETE(xorcl); + delete cm; + return sat; + } + + //################################################## + //################################################## + + /******************************************************************* + * Helper Functions + *******************************************************************/ + + //This function prints the output of the STP solver + void ToSAT::PrintOutput(SOLVER_RETURN_TYPE ret) + { + bool true_iff_valid = (SOLVER_VALID == ret); + + if (bm->UserFlags.print_output_flag) + { + if (bm->UserFlags.smtlib_parser_flag) + { + if (true_iff_valid && + (input_status == TO_BE_SATISFIABLE)) + { + cerr << "Warning. Expected satisfiable,"\ + " FOUND unsatisfiable" << endl; + } + else if (!true_iff_valid && + (input_status == TO_BE_UNSATISFIABLE)) + { + cerr << "Warning. Expected unsatisfiable,"\ + " FOUND satisfiable" << endl; + } + } + } + + if (true_iff_valid) + { + bm->ValidFlag = true; + if (bm->UserFlags.print_output_flag) + { + if (bm->UserFlags.smtlib_parser_flag) + cout << "unsat\n"; + else + cout << "Valid.\n"; + } + } + else + { + bm->ValidFlag = false; + if (bm->UserFlags.print_output_flag) + { + if (bm->UserFlags.smtlib_parser_flag) + cout << "sat\n"; + else + cout << "Invalid.\n"; + } + } + } //end of PrintOutput() + #if 0 // Looks up truth value of ASTNode SYMBOL in MINISAT satisfying diff --git a/src/to-sat/ToSAT.h b/src/to-sat/ToSAT.h index 8359ae5..8446129 100644 --- a/src/to-sat/ToSAT.h +++ b/src/to-sat/ToSAT.h @@ -54,12 +54,14 @@ namespace BEEV // Ptr to Simplifier Simplifier * simp; +#if 0 // Memo table to check the functioning of bitblaster and CNF // converter ASTNodeMap CheckBBandCNFMemo; // Map from formulas to representative literals, for debugging. ASTNodeMap RepLitMap; +#endif ASTNode ASTTrue, ASTFalse, ASTUndefined; @@ -72,14 +74,30 @@ namespace BEEV MINISAT::Var LookupOrCreateSATVar(MINISAT::Solver& S, const ASTNode& n); +#if 0 // Evaluates bitblasted formula in satisfying assignment ASTNode CheckBBandCNF(MINISAT::Solver& newS, ASTNode form); ASTNode CheckBBandCNF_int(MINISAT::Solver& newS, ASTNode form); + // Looks up truth value of ASTNode SYMBOL in MINISAT satisfying // assignment. Returns ASTTrue if true, ASTFalse if false or // undefined. + ASTNode SymbolTruthValue(MINISAT::Solver &newS, ASTNode form); +#endif + + //Iteratively goes through the Clause Buckets, and calls + //toSATandSolve() + bool CallSAT_On_ClauseBuckets(MINISAT::Solver& SatSolver, + ClauseBuckets * cb); + + // Converts the clause to SAT and calls SAT solver + bool toSATandSolve(MINISAT::Solver& S, + ClauseList& cll, + bool add_xor_clauses=false, + bool enable_clausal_abstraction=false); + public: /**************************************************************** @@ -89,8 +107,10 @@ namespace BEEV // Constructor ToSAT(STPMgr * bm, Simplifier * s) : bm(bm), - simp(s), - CheckBBandCNFMemo() + simp(s) +#if 0 + ,CheckBBandCNFMemo() +#endif { ASTTrue = bm->CreateNode(TRUE); ASTFalse = bm->CreateNode(FALSE); @@ -102,17 +122,6 @@ namespace BEEV const ASTNode& modified_input, const ASTNode& original_input); - //Iteratively goes through the Clause Buckets, and calls - //toSATandSolve() - bool CallSAT_On_ClauseBuckets(MINISAT::Solver& SatSolver, - ClauseBuckets * cb); - - // Converts the clause to SAT and calls SAT solver - bool toSATandSolve(MINISAT::Solver& S, - ClauseList& cll, - bool add_xor_clauses=false, - bool enable_clausal_abstraction=false); - //print the STP solver output void PrintOutput(SOLVER_RETURN_TYPE ret); @@ -130,8 +139,10 @@ namespace BEEV ~ToSAT() { _ASTNode_to_SATVar_Map.clear(); +#if 0 RepLitMap.clear(); CheckBBandCNFMemo.clear(); +#endif _SATVar_to_AST_Vector.clear(); } }; //end of class ToSAT -- 2.47.3