From: Dejan Jovanović Date: Thu, 17 May 2012 04:34:03 +0000 (+0000) Subject: Queueing up asserted literals in the proxy instead of sending them off to the theory... X-Git-Tag: cvc5-1.0.0~8160 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=a998a2a58571f6791b019fe77e698e05ce3fadd2;p=cvc5.git Queueing up asserted literals in the proxy instead of sending them off to the theory engine immediately. The queue is discharged just before a check(). --- diff --git a/src/prop/theory_proxy.cpp b/src/prop/theory_proxy.cpp index 53afce35e..7366afcaf 100644 --- a/src/prop/theory_proxy.cpp +++ b/src/prop/theory_proxy.cpp @@ -35,6 +35,11 @@ void TheoryProxy::variableNotify(SatVariable var) { } void TheoryProxy::theoryCheck(theory::Theory::Effort effort) { + while (!d_queue.empty()) { + TNode assertion = d_queue.front(); + d_queue.pop(); + d_theoryEngine->assertFact(assertion); + } d_theoryEngine->check(effort); } @@ -70,7 +75,7 @@ void TheoryProxy::enqueueTheoryLiteral(const SatLiteral& l) { Node literalNode = d_cnfStream->getNode(l); Debug("prop") << "enqueueing theory literal " << l << " " << literalNode << std::endl; Assert(!literalNode.isNull()); - d_theoryEngine->assertFact(literalNode); + d_queue.push(literalNode); } SatLiteral TheoryProxy::getNextDecisionRequest(bool &stopSearch) { diff --git a/src/prop/theory_proxy.h b/src/prop/theory_proxy.h index f3fe634e2..2fac0ab7b 100644 --- a/src/prop/theory_proxy.h +++ b/src/prop/theory_proxy.h @@ -29,6 +29,8 @@ #include "util/options.h" #include "util/stats.h" +#include "context/cdqueue.h" + #include "prop/sat_solver.h" namespace CVC4 { @@ -61,6 +63,9 @@ class TheoryProxy { /** Context we will be using to synchronzie the sat solver */ context::Context* d_context; + /** Queue of asserted facts */ + context::CDQueue d_queue; + /** * Set of all lemmas that have been "shared" in the portfolio---i.e., * all imported and exported lemmas. @@ -127,7 +132,8 @@ inline TheoryProxy::TheoryProxy(PropEngine* propEngine, d_cnfStream(cnfStream), d_decisionEngine(decisionEngine), d_theoryEngine(theoryEngine), - d_context(context) + d_context(context), + d_queue(context) {} }/* CVC4::prop namespace */