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().

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 */