Some base infrastructure for user push/pop; a few bugfixes to user push/pop and model gen also.

I also expect this commit to fix bug #273.

No performance change is expected on regressions with this commit, see
http://goedel.cims.nyu.edu/regress-results/compare_jobs.php?job_id=2871&reference_id=2863

3 files changed, 21 insertions, 12 deletions

diff --git a/test/unit/theory/theory_arith_white.h b/test/unit/theory/theory_arith_white.h
index ded7cee97..f0073cc0b 100644
--- a/test/unit/theory/theory_arith_white.h
+++ b/test/unit/theory/theory_arith_white.h
@@ -43,6 +43,7 @@ using namespace std;
 class TheoryArithWhite : public CxxTest::TestSuite {
 
   Context* d_ctxt;
+  UserContext* d_uctxt;
   NodeManager* d_nm;
   NodeManagerScope* d_scope;
 
@@ -92,11 +93,12 @@ public:
   }
 
   void setUp() {
-    d_ctxt = new Context;
+    d_ctxt = new Context();
+    d_uctxt = new UserContext();
     d_nm = new NodeManager(d_ctxt, NULL);
     d_scope = new NodeManagerScope(d_nm);
     d_outputChannel.clear();
-    d_arith = new TheoryArith(d_ctxt, d_outputChannel, Valuation(NULL));
+    d_arith = new TheoryArith(d_ctxt, d_uctxt, d_outputChannel, Valuation(NULL));
 
     preregistered = new std::set<Node>();
 
@@ -115,6 +117,7 @@ public:
     d_outputChannel.clear();
     delete d_scope;
     delete d_nm;
+    delete d_uctxt;
     delete d_ctxt;
   }
 
diff --git a/test/unit/theory/theory_black.h b/test/unit/theory/theory_black.h
index 2c3ff0bb1..63900c19c 100644
--- a/test/unit/theory/theory_black.h
+++ b/test/unit/theory/theory_black.h
@@ -95,8 +95,8 @@ public:
   set<Node> d_registered;
   vector<Node> d_getSequence;
 
-  DummyTheory(Context* ctxt, OutputChannel& out, Valuation valuation) :
-    Theory(theory::THEORY_BUILTIN, ctxt, out, valuation) {
+  DummyTheory(Context* ctxt, UserContext* uctxt, OutputChannel& out, Valuation valuation) :
+    Theory(theory::THEORY_BUILTIN, ctxt, uctxt, out, valuation) {
   }
 
   void registerTerm(TNode n) {
@@ -135,11 +135,12 @@ public:
   void explain(TNode n, Effort level) {}
   Node getValue(TNode n) { return Node::null(); }
   string identify() const { return "DummyTheory"; }
-};
+};/* class DummyTheory */
 
 class TheoryBlack : public CxxTest::TestSuite {
 
   Context* d_ctxt;
+  UserContext* d_uctxt;
   NodeManager* d_nm;
   NodeManagerScope* d_scope;
 
@@ -153,10 +154,11 @@ class TheoryBlack : public CxxTest::TestSuite {
 public:
 
   void setUp() {
-    d_ctxt = new Context;
+    d_ctxt = new Context();
+    d_uctxt = new UserContext();
     d_nm = new NodeManager(d_ctxt, NULL);
     d_scope = new NodeManagerScope(d_nm);
-    d_dummy = new DummyTheory(d_ctxt, d_outputChannel, Valuation(NULL));
+    d_dummy = new DummyTheory(d_ctxt, d_uctxt, d_outputChannel, Valuation(NULL));
     d_outputChannel.clear();
     atom0 = d_nm->mkConst(true);
     atom1 = d_nm->mkConst(false);
@@ -168,6 +170,7 @@ public:
     delete d_dummy;
     delete d_scope;
     delete d_nm;
+    delete d_uctxt;
     delete d_ctxt;
   }
 
diff --git a/test/unit/theory/theory_engine_white.h b/test/unit/theory/theory_engine_white.h
index e33efb597..7132d9b17 100644
--- a/test/unit/theory/theory_engine_white.h
+++ b/test/unit/theory/theory_engine_white.h
@@ -104,8 +104,8 @@ class FakeTheory : public Theory {
   // static std::deque<RewriteItem> s_expected;
 
 public:
-  FakeTheory(context::Context* ctxt, OutputChannel& out, Valuation valuation) :
-    Theory(theoryId, ctxt, out, valuation)
+  FakeTheory(context::Context* ctxt, context::UserContext* uctxt, OutputChannel& out, Valuation valuation) :
+    Theory(theoryId, ctxt, uctxt, out, valuation)
   { }
 
   /** Register an expected rewrite call */
@@ -222,6 +222,7 @@ public:
  */
 class TheoryEngineWhite : public CxxTest::TestSuite {
   Context* d_ctxt;
+  UserContext* d_uctxt;
 
   NodeManager* d_nm;
   NodeManagerScope* d_scope;
@@ -231,15 +232,16 @@ class TheoryEngineWhite : public CxxTest::TestSuite {
 public:
 
   void setUp() {
-    d_ctxt = new Context;
+    d_ctxt = new Context();
+    d_uctxt = new UserContext();
 
     d_nm = new NodeManager(d_ctxt, NULL);
     d_scope = new NodeManagerScope(d_nm);
 
-    d_nullChannel = new FakeOutputChannel;
+    d_nullChannel = new FakeOutputChannel();
 
     // create the TheoryEngine
-    d_theoryEngine = new TheoryEngine(d_ctxt);
+    d_theoryEngine = new TheoryEngine(d_ctxt, d_uctxt);
 
     d_theoryEngine->addTheory< FakeTheory<THEORY_BUILTIN> >(THEORY_BUILTIN);
     d_theoryEngine->addTheory< FakeTheory<THEORY_BOOL> >(THEORY_BOOL);
@@ -260,6 +262,7 @@ public:
     delete d_scope;
     delete d_nm;
 
+    delete d_uctxt;
     delete d_ctxt;
   }