From: vijay_ganesh Date: Mon, 7 Dec 2009 01:19:11 +0000 (+0000) Subject: cryptominisat2 is now the official SAT solver of STP X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=732bad7c827cbc97669320dfccc19b5923a01c00;p=francis%2Fstp.git cryptominisat2 is now the official SAT solver of STP git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@468 e59a4935-1847-0410-ae03-e826735625c1 --- diff --git a/src/AST/UsefulDefs.h b/src/AST/UsefulDefs.h index 060764a..27e1399 100644 --- a/src/AST/UsefulDefs.h +++ b/src/AST/UsefulDefs.h @@ -46,7 +46,7 @@ #define HASHMULTISET hash_multiset #define INITIAL_TABLE_SIZE 100 #define CLAUSAL_ABSTRACTION_CUTOFF 0.5 -#define MAX_BUCKET_LIMIT 3 +#define CLAUSAL_BUCKET_LIMIT 3 using namespace std; namespace BEEV { diff --git a/src/to-sat/BitBlast.cpp b/src/to-sat/BitBlast.cpp index f557225..d3c7cf5 100644 --- a/src/to-sat/BitBlast.cpp +++ b/src/to-sat/BitBlast.cpp @@ -729,15 +729,19 @@ namespace BEEV // worth doing explicitly (e.g., a = b, a = ~b, etc.) else { - // return _bm->CreateSimpForm(OR, - // _bm->CreateSimpForm(AND, a, b), - // _bm->CreateSimpForm(AND, b, c), - // _bm->CreateSimpForm(AND, a, c)); - return _bm->CreateSimpForm(AND, - _bm->CreateSimpForm(OR, a, b), - _bm->CreateSimpForm(OR, b, c), - _bm->CreateSimpForm(OR, a, c)); - +// return _bm->CreateSimpForm(OR, +// _bm->CreateSimpForm(AND, a, b), +// _bm->CreateSimpForm(AND, b, c), +// _bm->CreateSimpForm(AND, a, c)); + return + _bm->CreateSimpForm(AND, + _bm->CreateSimpForm(OR, a, b), + //_bm->CreateSimpForm(XOR,a,b)), + _bm->CreateSimpForm(OR, b, c), + //_bm->CreateSimpForm(XOR,b,c)), + _bm->CreateSimpForm(OR, a, c) + //_bm->CreateSimpForm(XOR,a,c) + ); } } @@ -745,31 +749,12 @@ namespace BEEV const ASTNode& yi, const ASTNode& cin) { - // For some unexplained reason, XORs are faster than converting - // them to cluases at this point ASTNode S0 = _bm->CreateSimpForm(XOR, - _bm->CreateSimpForm(XOR, xi, yi), + //_bm->CreateSimpForm(XOR, xi, yi), + xi, + yi, cin); return S0; - // ASTNode S1 = _bm->CreateSimpForm(OR,xi,yi,cin); - // ASTNode S2 = _bm->CreateSimpForm(OR, - // _bm->CreateSimpForm(NOT,xi), - // _bm->CreateSimpForm(NOT,yi), - // cin); - // ASTNode S3 = _bm->CreateSimpForm(OR, - // _bm->CreateSimpForm(NOT,xi), - // yi, - // _bm->CreateSimpForm(NOT,cin)); - // ASTNode S4 = _bm->CreateSimpForm(OR, - // xi, - // _bm->CreateSimpForm(NOT,yi), - // _bm->CreateSimpForm(NOT,cin)); - // ASTVec S; - // S.push_back(S1); - // S.push_back(S2); - // S.push_back(S3); - // S.push_back(S4); - // return _bm->CreateSimpForm(AND,S); } // Bitwise complement diff --git a/src/to-sat/CallSAT.cpp b/src/to-sat/CallSAT.cpp index 2df4a41..984b8f4 100644 --- a/src/to-sat/CallSAT.cpp +++ b/src/to-sat/CallSAT.cpp @@ -10,7 +10,7 @@ namespace BEEV { - //Bucketize clauses into buckets of size 1,2,...MAX_BUCKET_LIMIT + //Bucketize clauses into buckets of size 1,2,...CLAUSAL_BUCKET_LIMIT static ClauseBuckets * Sort_ClauseList_IntoBuckets(ClauseList * cl) { ClauseBuckets * cb = new ClauseBuckets(); @@ -21,9 +21,9 @@ namespace BEEV { ClausePtr cptr = *it; int cl_size = cptr->size(); - if(cl_size >= MAX_BUCKET_LIMIT) + if(cl_size >= CLAUSAL_BUCKET_LIMIT) { - cl_size = MAX_BUCKET_LIMIT; + cl_size = CLAUSAL_BUCKET_LIMIT; } //If no clauses of size cl_size have been seen, then create a @@ -51,10 +51,17 @@ namespace BEEV ClauseBuckets::iterator itend = cb->end(); bool sat = false; - for(;it!=itend;it++) + for(int count=1;it!=itend;it++, count++) { ClauseList *cl = (*it).second; - sat = toSATandSolve(SatSolver,*cl); +// if(CLAUSAL_BUCKET_LIMIT == count) +// { +// sat = toSATandSolve(SatSolver,*cl, false, true); +// } +// else + { + sat = toSATandSolve(SatSolver,*cl); + } if(!sat) { return sat; diff --git a/src/to-sat/SimpBool.cpp b/src/to-sat/SimpBool.cpp index 977de28..5b1ae40 100644 --- a/src/to-sat/SimpBool.cpp +++ b/src/to-sat/SimpBool.cpp @@ -38,7 +38,7 @@ namespace BEEV case AND: return CreateSimpAndOr(1, children); break; - case OR: + case OR: return CreateSimpAndOr(0, children); break; case NAND: @@ -148,10 +148,6 @@ namespace BEEV } } - // I don't think this is even called, since it called - // CreateSimpAndOr instead of CreateSimpXor until 1/9/07 with no ill - // effects. Calls seem to go to the version that takes a vector of - // children. ASTNode STPMgr::CreateSimpXor(const ASTNode& form1, const ASTNode& form2) { ASTVec children; diff --git a/src/to-sat/ToSAT.cpp b/src/to-sat/ToSAT.cpp index 8cd957f..2994a5f 100644 --- a/src/to-sat/ToSAT.cpp +++ b/src/to-sat/ToSAT.cpp @@ -66,7 +66,9 @@ namespace BEEV * unsat. else continue. */ bool ToSAT::toSATandSolve(MINISAT::Solver& newSolver, - ClauseList& cll, bool add_xor_clauses) + ClauseList& cll, + bool add_xor_clauses, + bool enable_clausal_abstraction) { CountersAndStats("SAT Solver", bm); bm->GetRunTimes()->start(RunTimes::SendingToSAT); @@ -88,7 +90,7 @@ namespace BEEV if(bm->UserFlags.print_cnf_flag) { - #define DEBUG_LIB + //newSolver.cnfDump = true; } #ifdef CRYPTOMINISAT newSolver.startClauseAdding(); @@ -134,8 +136,8 @@ namespace BEEV #else newSolver.addClause(satSolverClause); #endif - float percentage=CLAUSAL_ABSTRACTION_CUTOFF; - if(count++ >= input_clauselist_size*percentage) + if(enable_clausal_abstraction && + count++ >= input_clauselist_size*CLAUSAL_ABSTRACTION_CUTOFF) { //Arbitrary adding only 60% of the clauses in the hopes of //terminating early @@ -146,8 +148,8 @@ namespace BEEV #if defined CRYPTOMINISAT2 newSolver.set_gaussian_decision_until(100); - newSolver.performReplace = false; - newSolver.xorFinder = false; + //newSolver.performReplace = true; + //newSolver.xorFinder = true; #endif newSolver.solve(); bm->GetRunTimes()->stop(RunTimes::Solving); diff --git a/src/to-sat/ToSAT.h b/src/to-sat/ToSAT.h index b83377b..af53590 100644 --- a/src/to-sat/ToSAT.h +++ b/src/to-sat/ToSAT.h @@ -110,7 +110,9 @@ namespace BEEV // Converts the clause to SAT and calls SAT solver bool toSATandSolve(MINISAT::Solver& S, - ClauseList& cll, bool add_xor_clauses=false); + ClauseList& cll, + bool add_xor_clauses=false, + bool enable_clausal_abstraction=false); //print the STP solver output void PrintOutput(SOLVER_RETURN_TYPE ret);