diff options
Diffstat (limited to 'src/prop')
-rw-r--r-- | src/prop/cnf_stream.cpp | 1 | ||||
-rw-r--r-- | src/prop/minisat/core/Solver.cc | 29 | ||||
-rw-r--r-- | src/prop/minisat/minisat.cpp | 21 | ||||
-rw-r--r-- | src/prop/minisat/minisat.h | 6 | ||||
-rw-r--r-- | src/prop/prop_engine.cpp | 6 | ||||
-rw-r--r-- | src/prop/sat_solver_types.h | 11 | ||||
-rw-r--r-- | src/prop/theory_proxy.cpp | 8 | ||||
-rw-r--r-- | src/prop/theory_proxy.h | 4 |
8 files changed, 77 insertions, 9 deletions
diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp index 62d885c06..485ddbb55 100644 --- a/src/prop/cnf_stream.cpp +++ b/src/prop/cnf_stream.cpp @@ -120,6 +120,7 @@ bool CnfStream::hasLiteral(TNode n) const { } void TseitinCnfStream::ensureLiteral(TNode n) { + Debug("cnf") << "ensureLiteral(" << n << ")" << endl; if(hasLiteral(n)) { // Already a literal! // newLiteral() may be necessary to renew a previously-extant literal diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc index d220c4dbb..a260a8ca1 100644 --- a/src/prop/minisat/core/Solver.cc +++ b/src/prop/minisat/core/Solver.cc @@ -395,6 +395,7 @@ Lit Solver::pickBranchLit() while (nextLit != lit_Undef) { if(value(var(nextLit)) == l_Undef) { Debug("propagateAsDecision") << "propagateAsDecision(): now deciding on " << nextLit << std::endl; + decisions++; return nextLit; } else { Debug("propagateAsDecision") << "propagateAsDecision(): would decide on " << nextLit << " but it already has an assignment" << std::endl; @@ -414,14 +415,35 @@ Lit Solver::pickBranchLit() rnd_decisions++; } // Activity based decision: - while (next == var_Undef || value(next) != l_Undef || !decision[next]) + while (next == var_Undef || value(next) != l_Undef || !decision[next]) { if (order_heap.empty()){ next = var_Undef; break; - }else + }else { next = order_heap.removeMin(); + } + + if(!decision[next]) continue; + // Check with decision engine about relevancy + if(proxy->isDecisionRelevant(MinisatSatSolver::toSatVariable(next)) == false ) { + next = var_Undef; + } + } - return next == var_Undef ? lit_Undef : mkLit(next, rnd_pol ? drand(random_seed) < 0.5 : polarity[next]); + if(next == var_Undef) { + return lit_Undef; + } else { + decisions++; + // Check with decision engine if it can tell polarity + lbool dec_pol = MinisatSatSolver::toMinisatlbool + (proxy->getDecisionPolarity(MinisatSatSolver::toSatVariable(next))); + if(dec_pol != l_Undef) { + Assert(dec_pol == l_True || dec_pol == l_False); + return mkLit(next, (dec_pol == l_True) ); + } + // If it can't use internal heuristic to do that + return mkLit(next, rnd_pol ? drand(random_seed) < 0.5 : polarity[next]); + } } @@ -1127,7 +1149,6 @@ lbool Solver::search(int nof_conflicts) if (next == lit_Undef) { // New variable decision: - decisions++; next = pickBranchLit(); if (next == lit_Undef) { diff --git a/src/prop/minisat/minisat.cpp b/src/prop/minisat/minisat.cpp index 4f2a16670..6b02153c7 100644 --- a/src/prop/minisat/minisat.cpp +++ b/src/prop/minisat/minisat.cpp @@ -69,6 +69,20 @@ SatValue MinisatSatSolver::toSatLiteralValue(Minisat::lbool res) { return SAT_VALUE_FALSE; } +Minisat::lbool MinisatSatSolver::toMinisatlbool(SatValue val) +{ + if(val == SAT_VALUE_TRUE) return Minisat::lbool((uint8_t)0); + if(val == SAT_VALUE_UNKNOWN) return Minisat::lbool((uint8_t)2); + Assert(val == SAT_VALUE_FALSE); + return Minisat::lbool((uint8_t)1); +} + +/*bool MinisatSatSolver::tobool(SatValue val) +{ + if(val == SAT_VALUE_TRUE) return true; + Assert(val == SAT_VALUE_FALSE); + return false; + }*/ void MinisatSatSolver::toMinisatClause(SatClause& clause, Minisat::vec<Minisat::Lit>& minisat_clause) { @@ -92,10 +106,15 @@ void MinisatSatSolver::initialize(context::Context* context, TheoryProxy* theory d_context = context; + if( Options::current()->decisionMode != Options::DECISION_STRATEGY_INTERNAL ) { + Notice() << "minisat: Incremental solving is disabled" + << " unless using internal decision strategy." << std::endl; + } + // Create the solver d_minisat = new Minisat::SimpSolver(theoryProxy, d_context, Options::current()->incrementalSolving || - Options::current()->decisionMode == Options::DECISION_STRATEGY_JUSTIFICATION ); + Options::current()->decisionMode != Options::DECISION_STRATEGY_INTERNAL ); // Setup the verbosity d_minisat->verbosity = (Options::current()->verbosity > 0) ? 1 : -1; diff --git a/src/prop/minisat/minisat.h b/src/prop/minisat/minisat.h index 19ade8ffa..9171bf232 100644 --- a/src/prop/minisat/minisat.h +++ b/src/prop/minisat/minisat.h @@ -45,8 +45,10 @@ public: static SatVariable toSatVariable(Minisat::Var var); static Minisat::Lit toMinisatLit(SatLiteral lit); static SatLiteral toSatLiteral(Minisat::Lit lit); - static SatValue toSatLiteralValue(bool res); - static SatValue toSatLiteralValue(Minisat::lbool res); + static SatValue toSatLiteralValue(bool res); + static SatValue toSatLiteralValue(Minisat::lbool res); + static Minisat::lbool toMinisatlbool(SatValue val); + //(Commented because not in use) static bool tobool(SatValue val); static void toMinisatClause(SatClause& clause, Minisat::vec<Minisat::Lit>& minisat_clause); static void toSatClause (Minisat::vec<Minisat::Lit>& clause, SatClause& sat_clause); diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index 58270b4d0..702a530cf 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -77,7 +77,11 @@ PropEngine::PropEngine(TheoryEngine* te, DecisionEngine *de, Context* context) : d_satSolver = SatSolverFactory::createDPLLMinisat(); theory::TheoryRegistrar* registrar = new theory::TheoryRegistrar(d_theoryEngine); - d_cnfStream = new CVC4::prop::TseitinCnfStream(d_satSolver, registrar, Options::current()->threads > 1); + d_cnfStream = new CVC4::prop::TseitinCnfStream + (d_satSolver, registrar, + // fullLitToNode Map = + Options::current()->threads > 1 || + Options::current()->decisionMode == Options::DECISION_STRATEGY_RELEVANCY); d_satSolver->initialize(d_context, new TheoryProxy(this, d_theoryEngine, d_decisionEngine, d_context, d_cnfStream)); diff --git a/src/prop/sat_solver_types.h b/src/prop/sat_solver_types.h index 0da4d7a6a..9dcc1c4bf 100644 --- a/src/prop/sat_solver_types.h +++ b/src/prop/sat_solver_types.h @@ -3,7 +3,7 @@ ** \verbatim ** Original author: taking ** Major contributors: mdeters, dejan - ** Minor contributors (to current version): barrett, cconway + ** Minor contributors (to current version): barrett, cconway, kshitij ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences @@ -41,6 +41,15 @@ enum SatValue { SAT_VALUE_FALSE }; +/** Helper function for inverting a SatValue */ +inline SatValue invertValue(SatValue v) +{ + if(v == SAT_VALUE_UNKNOWN) return SAT_VALUE_UNKNOWN; + else if(v == SAT_VALUE_TRUE) return SAT_VALUE_FALSE; + else return SAT_VALUE_TRUE; +} + + /** * A variable of the SAT solver. */ diff --git a/src/prop/theory_proxy.cpp b/src/prop/theory_proxy.cpp index ccb26b6f0..93f8c0a5d 100644 --- a/src/prop/theory_proxy.cpp +++ b/src/prop/theory_proxy.cpp @@ -188,9 +188,17 @@ void TheoryProxy::checkTime() { d_propEngine->checkTime(); } +bool TheoryProxy::isDecisionRelevant(SatVariable var) { + return d_decisionEngine->isRelevant(var); +} + bool TheoryProxy::isDecisionEngineDone() { return d_decisionEngine->isDone(); } +SatValue TheoryProxy::getDecisionPolarity(SatVariable var) { + return d_decisionEngine->getPolarity(var); +} + }/* CVC4::prop namespace */ }/* CVC4 namespace */ diff --git a/src/prop/theory_proxy.h b/src/prop/theory_proxy.h index 2fac0ab7b..99aab8286 100644 --- a/src/prop/theory_proxy.h +++ b/src/prop/theory_proxy.h @@ -119,6 +119,10 @@ public: bool isDecisionEngineDone(); + bool isDecisionRelevant(SatVariable var); + + SatValue getDecisionPolarity(SatVariable var); + };/* class SatSolver */ /* Functions that delegate to the concrete SAT solver. */ |