diff options
Diffstat (limited to 'src/prop/theory_proxy.cpp')
| -rw-r--r-- | src/prop/theory_proxy.cpp | 13 |
1 files changed, 11 insertions, 2 deletions
diff --git a/src/prop/theory_proxy.cpp b/src/prop/theory_proxy.cpp index f024dccf3..53afce35e 100644 --- a/src/prop/theory_proxy.cpp +++ b/src/prop/theory_proxy.cpp @@ -73,7 +73,7 @@ void TheoryProxy::enqueueTheoryLiteral(const SatLiteral& l) { d_theoryEngine->assertFact(literalNode); } -SatLiteral TheoryProxy::getNextDecisionRequest() { +SatLiteral TheoryProxy::getNextDecisionRequest(bool &stopSearch) { TNode n = d_theoryEngine->getNextDecisionRequest(); if(not n.isNull()) return d_cnfStream->getLiteral(n); @@ -82,7 +82,12 @@ SatLiteral TheoryProxy::getNextDecisionRequest() { // may return in undefSatLiteral in which case the sat solver figure // it out something Assert(d_decisionEngine != NULL); - return d_decisionEngine->getNext(); + Assert(stopSearch != true); + SatLiteral ret = d_decisionEngine->getNext(stopSearch); + if(stopSearch) { + Trace("decision") << " *** Decision Engine stopped search *** " << std::endl; + } + return ret; } bool TheoryProxy::theoryNeedCheck() const { @@ -178,5 +183,9 @@ void TheoryProxy::checkTime() { d_propEngine->checkTime(); } +bool TheoryProxy::isDecisionEngineDone() { + return d_decisionEngine->isDone(); +} + }/* CVC4::prop namespace */ }/* CVC4 namespace */ |