From 576b0af0a5410558b29394b525ad56cb0d3254c4 Mon Sep 17 00:00:00 2001 From: vijay_ganesh Date: Thu, 5 Nov 2009 19:41:17 +0000 Subject: [PATCH] added xor clause adding to cryptominisat. still being debugged git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@382 e59a4935-1847-0410-ae03-e826735625c1 --- src/to-sat/CallSAT.cpp | 20 +++++++++- src/to-sat/ToCNF.cpp | 90 +++++++++++++++++++++++++++++++++++++++--- src/to-sat/ToCNF.h | 7 ++++ src/to-sat/ToSAT.cpp | 14 +++++-- src/to-sat/ToSAT.h | 5 ++- 5 files changed, 125 insertions(+), 11 deletions(-) diff --git a/src/to-sat/CallSAT.cpp b/src/to-sat/CallSAT.cpp index ef1a4f1..01e4abe 100644 --- a/src/to-sat/CallSAT.cpp +++ b/src/to-sat/CallSAT.cpp @@ -8,7 +8,7 @@ ********************************************************************/ #include "ToSAT.h" -#define MAX_BUCKET_LIMIT 3 +#define MAX_BUCKET_LIMIT 2 namespace BEEV { @@ -79,9 +79,27 @@ namespace BEEV CNFMgr* cm = new CNFMgr(bm); ClauseList* cl = cm->convertToCNF(BBFormula); + +#ifdef CRYPTOMINISAT + ClauseList* xorcl = cm->ReturnXorClauses(); +#endif + ClauseBuckets * cb = Sort_ClauseList_IntoBuckets(cl); //bool sat = toSATandSolve(SatSolver, *cl); bool sat = CallSAT_On_ClauseBuckets(SatSolver, cb); + if(!sat) + { + return sat; + } + +#ifdef CRYPTOMINISAT + if(!xorcl->empty()) + { + sat = toSATandSolve(SatSolver, *xorcl, true); + } + cm->DELETE(xorcl); +#endif + cm->DELETE(cl); delete cm; return sat; diff --git a/src/to-sat/ToCNF.cpp b/src/to-sat/ToCNF.cpp index f46bb62..9a3e156 100644 --- a/src/to-sat/ToCNF.cpp +++ b/src/to-sat/ToCNF.cpp @@ -1,6 +1,6 @@ // -*- c++ -*- /******************************************************************** - * AUTHORS: Vijay Ganesh, Mike Katelman + * AUTHORS: Mike Katelman * * BEGIN DATE: November, 2005 * @@ -401,6 +401,13 @@ namespace BEEV return psi; } //End of SINGLETON() + static ASTNode GetNodeFrom_SINGLETON(ClauseList *cl) + { + ClausePtr c = (*cl)[0]; + const ASTNode * a = (*c)[0]; + return *a; + } + ClauseList* CNFMgr::UNION(const ClauseList& varphi1, const ClauseList& varphi2) { @@ -775,6 +782,40 @@ namespace BEEV setWasRenamedPos(*x); }//End of doRenamingPos + + void CNFMgr::doRenamingPosXor(const ASTNode& varphi) + { + CNFInfo* x = info[varphi]; + + //######################################## + // step 1, calc new variable + //######################################## + + ostringstream oss; + oss << "cnf" << "{" << varphi.GetNodeNum() << "}"; + ASTNode psi = bm->CreateSymbol(oss.str().c_str()); + + //######################################## + // step 2, add defs + //######################################## + + // ClauseList* cl1; + // cl1 = SINGLETON(bm->CreateNode(NOT, psi)); + // ClauseList* cl2 = PRODUCT(*(info[varphi]->clausespos), *cl1); + // defs->insert(defs->end(), cl2->begin(), cl2->end()); + // DELETE(info[varphi]->clausespos); + // DELETE(cl1); + // delete cl2; + + //######################################## + // step 3, update info[varphi] + //######################################## + + x->clausespos = SINGLETON(psi); + setWasRenamedPos(*x); + }//End of doRenamingPos + + void CNFMgr::doRenamingNeg(const ASTNode& varphi, ClauseList* defs) { CNFInfo* x = info[varphi]; @@ -1219,6 +1260,34 @@ namespace BEEV void CNFMgr::convertFormulaToCNFPosXOR(const ASTNode& varphi, ClauseList* defs) { +#ifdef CRYPTOMINISAT + ASTVec::const_iterator it = varphi.GetChildren().begin(); + ClausePtr xor_clause = new vector(); + + for (; it != varphi.GetChildren().end(); it++) + { + convertFormulaToCNF(*it, defs); // make pos and neg clause set + + //Creating a new variable name for each of the children of the + //XOR node + doRenamingPos(*it, defs); + xor_clause->insert(xor_clause->end(), + ((*(info[*it]->clausespos))[0])->begin(), + ((*(info[*it]->clausespos))[0])->end()); + } + doRenamingPosXor(varphi); + //doRenamingPos(varphi, defs); + ASTNode varXorNode = GetNodeFrom_SINGLETON(info[varphi]->clausespos); + ASTNode NotVarXorNode = bm->CreateNode(NOT, varXorNode); + xor_clause->push_back(ASTNodeToASTNodePtr(NotVarXorNode)); + clausesxor->push_back(xor_clause); + + ASTVec::const_iterator it2 = varphi.GetChildren().begin(); + for (; it2 != varphi.GetChildren().end(); it2++){ + reduceMemoryFootprintPos(*it2); + reduceMemoryFootprintNeg(*it2); + } +#else ASTVec::const_iterator it = varphi.GetChildren().begin(); for (; it != varphi.GetChildren().end(); it++) { @@ -1231,13 +1300,13 @@ namespace BEEV reduceMemoryFootprintPos(*it2); reduceMemoryFootprintNeg(*it2); } +#endif } //End of convertFormulaToCNFPosXOR() ClauseList* CNFMgr::convertFormulaToCNFPosXORAux(const ASTNode& varphi, unsigned int idx, ClauseList* defs) { - bool renamesibs; ClauseList* psi; ClauseList* psi1; @@ -1246,8 +1315,8 @@ namespace BEEV if (idx == varphi.GetChildren().size() - 2) { //**************************************** - // (pos) XOR ~> UNION - // (PRODUCT [idx] ; [idx+1]) + // (pos) XOR ~> UNION (AND) + // (PRODUCT (OR) [idx] ; [idx+1]) // ; (PRODUCT NOT [idx] ; NOT [idx+1]) //**************************************** renamesibs = @@ -1738,6 +1807,7 @@ namespace BEEV CNFMgr::CNFMgr(STPMgr *bmgr) { bm = bmgr; + clausesxor = new ClauseList(); } //######################################## @@ -1749,8 +1819,10 @@ namespace BEEV for (; it1 != store.end(); it1++) { delete it1->second; - } - store.clear(); + } + store.clear(); + + //FIXME: Delete clausesxor } //######################################## @@ -1778,6 +1850,12 @@ namespace BEEV return defs; }//End of convertToCNF() + //All XOR clauses are stored here. Return it after CNF translation + ClauseList* CNFMgr::ReturnXorClauses(void) + { + return clausesxor; + } + void CNFMgr::DELETE(ClauseList* varphi) { ClauseList::const_iterator it = varphi->begin(); diff --git a/src/to-sat/ToCNF.h b/src/to-sat/ToCNF.h index f50e90e..b4c7bff 100644 --- a/src/to-sat/ToCNF.h +++ b/src/to-sat/ToCNF.h @@ -37,6 +37,9 @@ namespace BEEV }; } CNFInfo; + //Collect all XOR Clauses here + ClauseList* clausesxor; + typedef HASHMAP< ASTNode, CNFInfo*, @@ -163,6 +166,8 @@ namespace BEEV void doRenamingPos(const ASTNode& varphi, ClauseList* defs); + void doRenamingPosXor(const ASTNode& varphi); + void doRenamingNeg(const ASTNode& varphi, ClauseList* defs); //######################################## @@ -246,6 +251,8 @@ namespace BEEV ClauseList* convertToCNF(const ASTNode& varphi); + ClauseList* ReturnXorClauses(void); + void DELETE(ClauseList* varphi); void PrintClauseList(ostream& os, ClauseList& cll); diff --git a/src/to-sat/ToSAT.cpp b/src/to-sat/ToSAT.cpp index 0ab7c1e..a95f36a 100644 --- a/src/to-sat/ToSAT.cpp +++ b/src/to-sat/ToSAT.cpp @@ -43,7 +43,8 @@ namespace BEEV * and calls solve(). If solve returns unsat, then stop and return * unsat. else continue. */ - bool ToSAT::toSATandSolve(MINISAT::Solver& newS, ClauseList& cll) + bool ToSAT::toSATandSolve(MINISAT::Solver& newS, + ClauseList& cll, bool add_xor_clauses) { CountersAndStats("SAT Solver", bm); bm->GetRunTimes()->start(RunTimes::SendingToSAT); @@ -87,11 +88,18 @@ namespace BEEV // continue; // } #ifdef CRYPTOMINISAT - newS.addClause(satSolverClause,0,"z"); + if(add_xor_clauses) + { + newS.addXorClause(satSolverClause, false, 0, "z"); + } + else + { + newS.addClause(satSolverClause,0,"z"); + } #else newS.addClause(satSolverClause); #endif - float percentage=0.6; + float percentage=CLAUSAL_ABSTRACTION_CUTOFF; if(count++ >= input_clauselist_size*percentage) { //Arbitrary adding only 60% of the clauses in the hopes of diff --git a/src/to-sat/ToSAT.h b/src/to-sat/ToSAT.h index b74d8de..4e10b6a 100644 --- a/src/to-sat/ToSAT.h +++ b/src/to-sat/ToSAT.h @@ -23,6 +23,8 @@ namespace BEEV { + #define CLAUSAL_ABSTRACTION_CUTOFF 0.6 + class ToSAT { private: /**************************************************************** @@ -109,7 +111,8 @@ namespace BEEV ClauseBuckets * cb); // Converts the clause to SAT and calls SAT solver - bool toSATandSolve(MINISAT::Solver& S, ClauseList& cll); + bool toSATandSolve(MINISAT::Solver& S, + ClauseList& cll, bool add_xor_clauses=false); // Calls SAT simplifier, array transformer (abstraction // refinement), bitvector solver, and SAT solver. Returns the -- 2.47.3