diff options
Diffstat (limited to 'src/prop')
-rw-r--r-- | src/prop/minisat/core/Solver.cc | 18 | ||||
-rw-r--r-- | src/prop/sat.cpp | 5 | ||||
-rw-r--r-- | src/prop/sat.h | 2 |
3 files changed, 24 insertions, 1 deletions
diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc index e1a8ded8e..cdab47163 100644 --- a/src/prop/minisat/core/Solver.cc +++ b/src/prop/minisat/core/Solver.cc @@ -355,13 +355,27 @@ void Solver::popTrail() { Lit Solver::pickBranchLit() { + Lit nextLit; + #ifdef CVC4_REPLAY - Lit nextLit = proxy->getNextReplayDecision(); + nextLit = proxy->getNextReplayDecision(); if (nextLit != lit_Undef) { return nextLit; } #endif /* CVC4_REPLAY */ + // Theory requests + nextLit = proxy->getNextDecisionRequest(); + while (nextLit != lit_Undef) { + if(value(var(nextLit)) == l_Undef) { + Debug("propagateAsDecision") << "propagateAsDecision(): now deciding on " << nextLit << std::endl; + return nextLit; + } else { + Debug("propagateAsDecision") << "propagateAsDecision(): would decide on " << nextLit << " but it already has an assignment" << std::endl; + } + nextLit = proxy->getNextDecisionRequest(); + } + Var next = var_Undef; // Random decision: @@ -699,6 +713,7 @@ void Solver::propagateTheory() { std::vector<Lit> propagatedLiterals; proxy->theoryPropagate(propagatedLiterals); int oldTrailSize = trail.size(); + Debug("minisat") << "old trail size is " << oldTrailSize << ", propagating " << propagatedLiterals.size() << " lits..." << std::endl; for (unsigned i = 0, i_end = propagatedLiterals.size(); i < i_end; ++ i) { Debug("minisat") << "Theory propagated: " << propagatedLiterals[i] << std::endl; // multiple theories can propagate the same literal @@ -707,6 +722,7 @@ void Solver::propagateTheory() { uncheckedEnqueue(p, CRef_Lazy); } else { // but we check that this is the case and that they agree + Debug("minisat") << "trail_index(var(p)) == " << trail_index(var(p)) << std::endl; Assert(trail_index(var(p)) >= oldTrailSize); Assert(value(p) == lbool(!sign(p))); } diff --git a/src/prop/sat.cpp b/src/prop/sat.cpp index 7df7535dd..559467922 100644 --- a/src/prop/sat.cpp +++ b/src/prop/sat.cpp @@ -71,6 +71,11 @@ void SatSolver::enqueueTheoryLiteral(const SatLiteral& l) { d_theoryEngine->assertFact(literalNode); } +SatLiteral SatSolver::getNextDecisionRequest() { + TNode n = d_theoryEngine->getNextDecisionRequest(); + return n.isNull() ? Minisat::lit_Undef : d_cnfStream->getLiteral(n); +} + bool SatSolver::theoryNeedCheck() const { return d_theoryEngine->needCheck(); } diff --git a/src/prop/sat.h b/src/prop/sat.h index e86443827..3f3166c14 100644 --- a/src/prop/sat.h +++ b/src/prop/sat.h @@ -236,6 +236,8 @@ public: void enqueueTheoryLiteral(const SatLiteral& l); + SatLiteral getNextDecisionRequest(); + bool theoryNeedCheck() const; void setCnfStream(CnfStream* cnfStream); |