From: trevor_hansen Date: Thu, 23 Jun 2011 02:17:24 +0000 (+0000) Subject: Improvement. Simplifying minisat now uses the advanced CNF generator by default. X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=a0ae305ae92955dbb693abf0a61dae10c717e329;p=francis%2Fstp.git Improvement. Simplifying minisat now uses the advanced CNF generator by default. git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1353 e59a4935-1847-0410-ae03-e826735625c1 --- diff --git a/src/STPManager/STP.cpp b/src/STPManager/STP.cpp index 2fe332a..69b01d6 100644 --- a/src/STPManager/STP.cpp +++ b/src/STPManager/STP.cpp @@ -446,9 +446,6 @@ 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) && !bm->UserFlags.isSet("traditional-cnf", "0"); - const bool maybeRefinement = arrayops && bm->UserFlags.arrayread_refinement_flag; simplifier::constantBitP::ConstantBitPropagation* cb = NULL; @@ -469,8 +466,9 @@ namespace BEEV { } ToSATAIG toSATAIG(bm, cb); + toSATAIG.setArrayTransformer(arrayTransformer); - ToSATBase* satBase = useAIGToCNF ? ((ToSAT*) &toSATAIG) : tosat; + ToSATBase* satBase = bm->UserFlags.isSet("traditional-cnf", "0") ? tosat : ((ToSAT*) &toSATAIG) ; // If it doesn't contain array operations, use ABC's CNF generation. res = Ctr_Example->CallSAT_ResultCheck(NewSolver, simplified_solved_InputToSAT, orig_input, satBase, diff --git a/src/absrefine_counterexample/AbstractionRefinement.cpp b/src/absrefine_counterexample/AbstractionRefinement.cpp index 658a1d7..5617807 100644 --- a/src/absrefine_counterexample/AbstractionRefinement.cpp +++ b/src/absrefine_counterexample/AbstractionRefinement.cpp @@ -36,7 +36,12 @@ namespace BEEV assert(a.GetKind() == SYMBOL); // It was ommitted from the initial problem, so assign it freshly. for (int i = 0; i < a.GetValueWidth(); i++) - v_a.push_back(SatSolver.newVar()); + { + SATSolver::Var v = SatSolver.newVar(); + // We probably don't want the variable eliminated. + SatSolver.setFrozen(v); + v_a.push_back(v); + } satVar.insert(make_pair(a, v_a)); } } diff --git a/src/sat/MinisatCore.cpp b/src/sat/MinisatCore.cpp index e90b10b..b85fd1b 100644 --- a/src/sat/MinisatCore.cpp +++ b/src/sat/MinisatCore.cpp @@ -86,5 +86,5 @@ namespace BEEV // I was going to make SimpSolver and Solver instances of this template. // But I'm not so sure now because I don't understand what eliminate() does in the simp solver. template class MinisatCore; - template class MinisatCore; + //template class MinisatCore; }; diff --git a/src/sat/SATSolver.h b/src/sat/SATSolver.h index 7cad410..ea3aba5 100644 --- a/src/sat/SATSolver.h +++ b/src/sat/SATSolver.h @@ -55,6 +55,10 @@ namespace BEEV virtual lbool false_literal() =0; virtual lbool undef_literal() =0; + // The simplifying solvers shouldn't eliminate index / value variables. + virtual void setFrozen(Var x) + {} + }; }; #endif diff --git a/src/sat/SimplifyingMinisat.cpp b/src/sat/SimplifyingMinisat.cpp index e1e1115..7bd5295 100644 --- a/src/sat/SimplifyingMinisat.cpp +++ b/src/sat/SimplifyingMinisat.cpp @@ -32,8 +32,6 @@ namespace BEEV if (!s->simplify()) return false; - // Without the eliminate(true) call. Calling solve() multiple times returns the wrong answer. - s->eliminate(true); return s->solve(); } @@ -76,4 +74,8 @@ namespace BEEV printf("CPU time : %g s\n", cpu_time); } + void SimplifyingMinisat::setFrozen(Var x) + { + s->setFrozen(x,true); + } }; diff --git a/src/sat/SimplifyingMinisat.h b/src/sat/SimplifyingMinisat.h index c71b027..314b188 100644 --- a/src/sat/SimplifyingMinisat.h +++ b/src/sat/SimplifyingMinisat.h @@ -48,6 +48,7 @@ namespace BEEV virtual lbool false_literal() {return ((uint8_t)1);} virtual lbool undef_literal() {return ((uint8_t)2);} + virtual void setFrozen(Var x); }; } ; diff --git a/src/to-sat/AIG/ToSATAIG.cpp b/src/to-sat/AIG/ToSATAIG.cpp index b9bf1bc..d48cb82 100644 --- a/src/to-sat/AIG/ToSATAIG.cpp +++ b/src/to-sat/AIG/ToSATAIG.cpp @@ -111,6 +111,36 @@ namespace BEEV Cnf_DataFree(cnfData); cnfData = NULL; + // Minisat doesn't, but simplifying minisat and cryptominsat eliminate variables during their + // simplification phases. The problem is that we may later add clauses in that refer to those + // simplified-away variables. Here we mark them as frozen which prevents them from being removed. + for (ArrayTransformer::ArrType::iterator it = arrayTransformer->arrayToIndexToRead.begin(); it + != arrayTransformer->arrayToIndexToRead.end(); it++) + { + ArrayTransformer::arrTypeMap& atm = it->second; + + for (ArrayTransformer::arrTypeMap::const_iterator it2 = atm.begin(); it2 != atm.end(); it2++) + { + const ArrayTransformer::ArrayRead& ar = it2->second; + ASTNodeToSATVar::iterator it = nodeToSATVar.find(ar.index_symbol); + if (it != nodeToSATVar.end()) + { + vector& v = it->second; + for (int i=0; i < v.size(); i++) + satSolver.setFrozen(v[i]); + } + + it = nodeToSATVar.find(ar.symbol); + if (it != nodeToSATVar.end()) + { + vector& v = it->second; + for (int i=0; i < v.size(); i++) + satSolver.setFrozen(v[i]); + } + } + } + + bm->GetRunTimes()->start(RunTimes::Solving); satSolver.solve(); bm->GetRunTimes()->stop(RunTimes::Solving); diff --git a/src/to-sat/AIG/ToSATAIG.h b/src/to-sat/AIG/ToSATAIG.h index 3a33b17..f5b4e4b 100644 --- a/src/to-sat/AIG/ToSATAIG.h +++ b/src/to-sat/AIG/ToSATAIG.h @@ -17,6 +17,7 @@ #include "../BitBlaster.h" #include "BBNodeManagerAIG.h" #include "ToCNFAIG.h" +#include "../../AST/ArrayTransformer.h" namespace BEEV { @@ -28,6 +29,8 @@ namespace BEEV ASTNodeToSATVar nodeToSATVar; simplifier::constantBitP::ConstantBitPropagation* cb; + ArrayTransformer *arrayTransformer; + // don't assign or copy construct. ToSATAIG& operator = (const ToSATAIG& other); ToSATAIG(const ToSATAIG& other); @@ -43,10 +46,16 @@ namespace BEEV count = 0; first = true; CNFFileNameCounter =0; + arrayTransformer = NULL; } public: + void setArrayTransformer(ArrayTransformer *at) + { + arrayTransformer = at; + } + bool cbIsDestructed() { return cb == NULL;