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

1 files changed, 20 insertions, 6 deletions

diff --git a/src/theory/theory.h b/src/theory/theory.h
index 931b1155e..17c9ef14a 100644
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -103,6 +103,11 @@ private:
   context::Context* d_context;
 
   /**
+   * The user context for the Theory.
+   */
+  context::UserContext* d_userContext;
+
+  /**
    * The assertFact() queue.
    *
    * These can not be TNodes as some atoms (such as equalities) are sent
@@ -133,13 +138,15 @@ protected:
   /**
    * Construct a Theory.
    */
-  Theory(TheoryId id, context::Context* ctxt, OutputChannel& out, Valuation valuation) throw() :
+  Theory(TheoryId id, context::Context* context, context::UserContext* userContext,
+         OutputChannel& out, Valuation valuation) throw() :
     d_id(id),
-    d_context(ctxt),
-    d_facts(ctxt),
-    d_factsHead(ctxt, 0),
-    d_sharedTermsIndex(ctxt, 0),
-    d_sharedTerms(ctxt),
+    d_context(context),
+    d_userContext(userContext),
+    d_facts(context),
+    d_factsHead(context, 0),
+    d_sharedTermsIndex(context, 0),
+    d_sharedTerms(context),
     d_out(&out),
     d_valuation(valuation)
   {
@@ -328,6 +335,13 @@ public:
   }
 
   /**
+   * Get the context associated to this Theory.
+   */
+  context::UserContext* getUserContext() const {
+    return d_userContext;
+  }
+
+  /**
    * Set the output channel associated to this theory.
    */
   void setOutputChannel(OutputChannel& out) {