diff options
author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2012-05-17 04:34:03 +0000 |
---|---|---|
committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2012-05-17 04:34:03 +0000 |
commit | a998a2a58571f6791b019fe77e698e05ce3fadd2 (patch) | |
tree | 8fd6d62a0cd8abfb1686f7528c99ab77d8032f18 /src | |
parent | a090197414c31b4cae3cdced9e448474858b7553 (diff) |
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().
Diffstat (limited to 'src')
-rw-r--r-- | src/prop/theory_proxy.cpp | 7 | ||||
-rw-r--r-- | src/prop/theory_proxy.h | 8 |
2 files changed, 13 insertions, 2 deletions
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<TNode> 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 */ |