diff options
Diffstat (limited to 'src/prop')
-rw-r--r-- | src/prop/minisat/core/Solver.cc | 18 | ||||
-rw-r--r-- | src/prop/theory_proxy.cpp | 11 | ||||
-rw-r--r-- | src/prop/theory_proxy.h | 4 |
3 files changed, 20 insertions, 13 deletions
diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc index c7f1780b6..6196ca357 100644 --- a/src/prop/minisat/core/Solver.cc +++ b/src/prop/minisat/core/Solver.cc @@ -458,9 +458,8 @@ Lit Solver::pickBranchLit() } #endif /* CVC4_REPLAY */ - // Theory/DE requests - bool stopSearch = false; - nextLit = MinisatSatSolver::toMinisatLit(proxy->getNextDecisionRequest(stopSearch)); + // Theory requests + nextLit = MinisatSatSolver::toMinisatLit(proxy->getNextTheoryDecisionRequest()); while (nextLit != lit_Undef) { if(value(var(nextLit)) == l_Undef) { Debug("propagateAsDecision") << "propagateAsDecision(): now deciding on " << nextLit << std::endl; @@ -469,12 +468,21 @@ Lit Solver::pickBranchLit() } else { Debug("propagateAsDecision") << "propagateAsDecision(): would decide on " << nextLit << " but it already has an assignment" << std::endl; } - nextLit = MinisatSatSolver::toMinisatLit(proxy->getNextDecisionRequest(stopSearch)); + nextLit = MinisatSatSolver::toMinisatLit(proxy->getNextTheoryDecisionRequest()); } + Debug("propagateAsDecision") << "propagateAsDecision(): decide on another literal" << std::endl; + + // DE requests + bool stopSearch = false; + nextLit = MinisatSatSolver::toMinisatLit(proxy->getNextDecisionEngineRequest(stopSearch)); if(stopSearch) { return lit_Undef; } - Debug("propagateAsDecision") << "propagateAsDecision(): decide on another literal" << std::endl; + if(nextLit != lit_Undef) { + Assert(value(var(nextLit)) == l_Undef, "literal to decide already has value"); + decisions++; + return nextLit; + } Var next = var_Undef; diff --git a/src/prop/theory_proxy.cpp b/src/prop/theory_proxy.cpp index a6908ff52..c9f19b42e 100644 --- a/src/prop/theory_proxy.cpp +++ b/src/prop/theory_proxy.cpp @@ -79,15 +79,12 @@ void TheoryProxy::enqueueTheoryLiteral(const SatLiteral& l) { d_queue.push(literalNode); } -SatLiteral TheoryProxy::getNextDecisionRequest(bool &stopSearch) { +SatLiteral TheoryProxy::getNextTheoryDecisionRequest() { TNode n = d_theoryEngine->getNextDecisionRequest(); - if(not n.isNull()) { - return d_cnfStream->getLiteral(n); - } + return n.isNull() ? undefSatLiteral : d_cnfStream->getLiteral(n); +} - // If theory doesn't give us a deicsion ask the decision engine. It - // may return in undefSatLiteral in which case the sat solver uses - // whatever default heuristic it has. +SatLiteral TheoryProxy::getNextDecisionEngineRequest(bool &stopSearch) { Assert(d_decisionEngine != NULL); Assert(stopSearch != true); SatLiteral ret = d_decisionEngine->getNext(stopSearch); diff --git a/src/prop/theory_proxy.h b/src/prop/theory_proxy.h index 5f1ea0e23..7b0aa2058 100644 --- a/src/prop/theory_proxy.h +++ b/src/prop/theory_proxy.h @@ -93,7 +93,9 @@ public: void enqueueTheoryLiteral(const SatLiteral& l); - SatLiteral getNextDecisionRequest(bool& stopSearch); + SatLiteral getNextTheoryDecisionRequest(); + + SatLiteral getNextDecisionEngineRequest(bool& stopSearch); bool theoryNeedCheck() const; |