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

17 files changed, 106 insertions, 78 deletions

diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index be8feb245..c69960d37 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -59,8 +59,8 @@ static const uint32_t RESET_START = 2;
 struct SlackAttrID;
 typedef expr::Attribute<SlackAttrID, bool> Slack;
 
-TheoryArith::TheoryArith(context::Context* c, OutputChannel& out, Valuation valuation) :
-  Theory(THEORY_ARITH, c, out, valuation),
+TheoryArith::TheoryArith(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation) :
+  Theory(THEORY_ARITH, c, u, out, valuation),
   learner(d_pbSubstitutions),
   d_nextIntegerCheckVar(0),
   d_partialModel(c),
@@ -68,6 +68,7 @@ TheoryArith::TheoryArith(context::Context* c, OutputChannel& out, Valuation valu
   d_diseq(c),
   d_tableau(),
   d_diosolver(c, d_tableau, d_partialModel),
+  d_pbSubstitutions(u),
   d_restartsCounter(0),
   d_rowHasBeenAdded(false),
   d_tableauResetDensity(1.6),
diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h
index 6bcf6a613..4731bea30 100644
--- a/src/theory/arith/theory_arith.h
+++ b/src/theory/arith/theory_arith.h
@@ -163,7 +163,7 @@ private:
   SimplexDecisionProcedure d_simplex;
 
 public:
-  TheoryArith(context::Context* c, OutputChannel& out, Valuation valuation);
+  TheoryArith(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation);
   virtual ~TheoryArith();
 
   /**
diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index 0aff30d74..f82b6c670 100644
--- a/src/theory/arrays/theory_arrays.cpp
+++ b/src/theory/arrays/theory_arrays.cpp
@@ -32,8 +32,8 @@ using namespace CVC4::theory;
 using namespace CVC4::theory::arrays;
 
 
-TheoryArrays::TheoryArrays(Context* c, OutputChannel& out, Valuation valuation) :
-  Theory(THEORY_ARRAY, c, out, valuation),
+TheoryArrays::TheoryArrays(Context* c, UserContext* u, OutputChannel& out, Valuation valuation) :
+  Theory(THEORY_ARRAY, c, u, out, valuation),
   d_ccChannel(this),
   d_cc(c, &d_ccChannel),
   d_unionFind(c),
diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h
index a984cb342..7fa215bfc 100644
--- a/src/theory/arrays/theory_arrays.h
+++ b/src/theory/arrays/theory_arrays.h
@@ -364,7 +364,7 @@ private:
   Node recursivePreprocessTerm(TNode term);
 
 public:
-  TheoryArrays(context::Context* c, OutputChannel& out, Valuation valuation);
+  TheoryArrays(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation);
   ~TheoryArrays();
 
   /**
diff --git a/src/theory/booleans/theory_bool.h b/src/theory/booleans/theory_bool.h
index d53337fa7..bd4c8d565 100644
--- a/src/theory/booleans/theory_bool.h
+++ b/src/theory/booleans/theory_bool.h
@@ -30,8 +30,8 @@ namespace booleans {
 
 class TheoryBool : public Theory {
 public:
-  TheoryBool(context::Context* c, OutputChannel& out, Valuation valuation) :
-    Theory(THEORY_BOOL, c, out, valuation) {
+  TheoryBool(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation) :
+    Theory(THEORY_BOOL, c, u, out, valuation) {
   }
 
   Node getValue(TNode n);
diff --git a/src/theory/builtin/theory_builtin.h b/src/theory/builtin/theory_builtin.h
index 5c3c70443..f5a46b799 100644
--- a/src/theory/builtin/theory_builtin.h
+++ b/src/theory/builtin/theory_builtin.h
@@ -29,8 +29,8 @@ namespace builtin {
 
 class TheoryBuiltin : public Theory {
 public:
-  TheoryBuiltin(context::Context* c, OutputChannel& out, Valuation valuation) :
-    Theory(THEORY_BUILTIN, c, out, valuation) {}
+  TheoryBuiltin(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation) :
+    Theory(THEORY_BUILTIN, c, u, out, valuation) {}
   Node getValue(TNode n);
   std::string identify() const { return std::string("TheoryBuiltin"); }
 };/* class TheoryBuiltin */
diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h
index 8ab806bd8..11ddceaae 100644
--- a/src/theory/bv/theory_bv.h
+++ b/src/theory/bv/theory_bv.h
@@ -122,8 +122,8 @@ private:
 
 public:
 
-  TheoryBV(context::Context* c, OutputChannel& out, Valuation valuation)
-  : Theory(THEORY_BV, c, out, valuation), 
+  TheoryBV(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation)
+  : Theory(THEORY_BV, c, u, out, valuation), 
     d_eqEngine(*this, c, "theory::bv::EqualityEngine"), 
     d_sliceManager(*this, c), 
     d_context(c),
diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index 4e185febc..08b142fe3 100644
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -53,8 +53,8 @@ Node TheoryDatatypes::getConstructorForSelector( Node sel )
 }
 
 
-TheoryDatatypes::TheoryDatatypes(Context* c, OutputChannel& out, Valuation valuation) :
-  Theory(THEORY_DATATYPES, c, out, valuation),
+TheoryDatatypes::TheoryDatatypes(Context* c, UserContext* u, OutputChannel& out, Valuation valuation) :
+  Theory(THEORY_DATATYPES, c, u, out, valuation),
   d_currAsserts(c),
   d_currEqualities(c),
   d_selectors(c),
diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h
index d91e9e7f4..433af38c3 100644
--- a/src/theory/datatypes/theory_datatypes.h
+++ b/src/theory/datatypes/theory_datatypes.h
@@ -140,7 +140,7 @@ private:
   CongruenceClosureExplainer<CongruenceChannel, CONGRUENCE_OPERATORS_2 (kind::APPLY_CONSTRUCTOR, kind::APPLY_SELECTOR)> d_cce;
 
 public:
-  TheoryDatatypes(context::Context* c, OutputChannel& out, Valuation valuation);
+  TheoryDatatypes(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation);
   ~TheoryDatatypes();
   void preRegisterTerm(TNode n);
   void presolve();
diff --git a/src/theory/example/theory_uf_tim.cpp b/src/theory/example/theory_uf_tim.cpp
index ae37dfe99..03787703a 100644
--- a/src/theory/example/theory_uf_tim.cpp
+++ b/src/theory/example/theory_uf_tim.cpp
@@ -27,8 +27,8 @@ using namespace CVC4::theory;
 using namespace CVC4::theory::uf;
 using namespace CVC4::theory::uf::tim;
 
-TheoryUFTim::TheoryUFTim(Context* c, OutputChannel& out, Valuation valuation) :
-  TheoryUF(c, out, valuation),
+TheoryUFTim::TheoryUFTim(Context* c, UserContext* u, OutputChannel& out, Valuation valuation) :
+  Theory(THEORY_UF, c, u, out, valuation),
   d_assertions(c),
   d_pending(c),
   d_currentPendingIdx(c,0),
diff --git a/src/theory/example/theory_uf_tim.h b/src/theory/example/theory_uf_tim.h
index 70c60728f..b47536f07 100644
--- a/src/theory/example/theory_uf_tim.h
+++ b/src/theory/example/theory_uf_tim.h
@@ -43,7 +43,7 @@ namespace theory {
 namespace uf {
 namespace tim {
 
-class TheoryUFTim : public TheoryUF {
+class TheoryUFTim : public Theory {
 
 private:
 
@@ -85,7 +85,7 @@ private:
 public:
 
   /** Constructs a new instance of TheoryUF w.r.t. the provided context.*/
-  TheoryUFTim(context::Context* c, OutputChannel& out, Valuation valuation);
+  TheoryUFTim(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation);
 
   /** Destructor for the TheoryUF object. */
   ~TheoryUFTim();
diff --git a/src/theory/substitutions.cpp b/src/theory/substitutions.cpp
index 88e5b3dba..cdcf33f6a 100644
--- a/src/theory/substitutions.cpp
+++ b/src/theory/substitutions.cpp
@@ -67,7 +67,7 @@ Node SubstitutionMap::internalSubstitute(TNode t, NodeMap& substitutionCache) {
       }
       for (unsigned i = 0; i < current.getNumChildren(); ++ i) {
         Assert(substitutionCache.find(current[i]) != substitutionCache.end());
-        builder << substitutionCache[current[i]];
+        builder << Node(substitutionCache[current[i]]);
       }
       // Mark the substitution and continue
       Node result = builder;
@@ -104,14 +104,14 @@ void SubstitutionMap::addSubstitution(TNode x, TNode t, bool invalidateCache) {
   Assert(d_substitutions.find(x) == d_substitutions.end());
 
   // Temporary substitution cache
-  NodeMap tempCache;
+  NodeMap tempCache(d_context);
   tempCache[x] = t;
 
   // Put in the new substitutions into the old ones
   NodeMap::iterator it = d_substitutions.begin();
   NodeMap::iterator it_end = d_substitutions.end();
   for(; it != it_end; ++ it) {
-    it->second = internalSubstitute(it->second, tempCache);
+    d_substitutions[(*it).first] = internalSubstitute((*it).second, tempCache);
   }
 
   // Put the new substitution in
@@ -123,11 +123,12 @@ void SubstitutionMap::addSubstitution(TNode x, TNode t, bool invalidateCache) {
   }
 }
 
-bool check(TNode node, const SubstitutionMap::NodeMap& substitutions) {
+static bool check(TNode node, const SubstitutionMap::NodeMap& substitutions) CVC4_UNUSED;
+static bool check(TNode node, const SubstitutionMap::NodeMap& substitutions) {
   SubstitutionMap::NodeMap::const_iterator it = substitutions.begin();
   SubstitutionMap::NodeMap::const_iterator it_end = substitutions.end();
   for (; it != it_end; ++ it) {
-    if (node.hasSubterm(it->first)) {
+    if (node.hasSubterm((*it).first)) {
       return false;
     }
   }
@@ -140,7 +141,12 @@ Node SubstitutionMap::apply(TNode t) {
 
   // Setup the cache
   if (d_cacheInvalidated) {
-    d_substitutionCache = d_substitutions;
+    SubstitutionMap::NodeMap::const_iterator it = d_substitutions.begin();
+    SubstitutionMap::NodeMap::const_iterator it_end = d_substitutions.end();
+    d_substitutionCache.clear();
+    for (; it != it_end; ++ it) {
+      d_substitutionCache[(*it).first] = (*it).second;
+    }
     d_cacheInvalidated = false;
   }
 
@@ -157,7 +163,7 @@ void SubstitutionMap::print(ostream& out) const {
   NodeMap::const_iterator it = d_substitutions.begin();
   NodeMap::const_iterator it_end = d_substitutions.end();
   for (; it != it_end; ++ it) {
-    out << it->first << " -> " << it->second << endl;
+    out << (*it).first << " -> " << (*it).second << endl;
   }
 }
 
diff --git a/src/theory/substitutions.h b/src/theory/substitutions.h
index 849c8f166..253507645 100644
--- a/src/theory/substitutions.h
+++ b/src/theory/substitutions.h
@@ -24,7 +24,11 @@
 #include <utility>
 #include <vector>
 #include <algorithm>
+
 #include "expr/node.h"
+#include "context/context.h"
+#include "context/cdo.h"
+#include "context/cdmap.h"
 
 namespace CVC4 {
 namespace theory {
@@ -32,17 +36,22 @@ namespace theory {
 /**
  * The type for the Substitutions mapping output by
  * Theory::simplify(), TheoryEngine::simplify(), and
- * Valuation::simplify().  This is in its own header to avoid circular
- * dependences between those three.
+ * Valuation::simplify().  This is in its own header to
+ * avoid circular dependences between those three.
+ *
+ * This map is context-dependent.
  */
 class SubstitutionMap {
 
 public:
 
-  typedef std::hash_map<Node, Node, NodeHashFunction> NodeMap;
+  typedef context::CDMap<Node, Node, NodeHashFunction> NodeMap;
 
 private:
 
+  /** The context within which this SubstitutionMap was constructed. */
+  context::Context* d_context;
+
   /** The variables, in order of addition */
   NodeMap d_substitutions;
 
@@ -50,14 +59,19 @@ private:
   NodeMap d_substitutionCache;
 
   /** Has the cache been invalidated */
-  bool d_cacheInvalidated;
+  context::CDO<bool> d_cacheInvalidated;
 
-  /** Internaal method that performs substitution */
+  /** Internal method that performs substitution */
   Node internalSubstitute(TNode t, NodeMap& substitutionCache);
 
 public:
 
-  SubstitutionMap(): d_cacheInvalidated(true) {}
+  SubstitutionMap(context::Context* context) :
+    d_context(context),
+    d_substitutions(context),
+    d_substitutionCache(context),
+    d_cacheInvalidated(context) {
+  }
 
   /**
    * Adds a substitution from x to t
@@ -77,24 +91,11 @@ public:
     return const_cast<SubstitutionMap*>(this)->apply(t);
   }
 
-  /**
-   * Clear out the accumulated substitutions, resetting this
-   * SubstitutionMap to the way it was when first constructed.
-   */
-  void clear() {
-    d_substitutions.clear();
-    d_substitutionCache.clear();
-    d_cacheInvalidated = true;
-  }
-
-  /**
-   * Swap the contents of this SubstitutionMap with those of another.
-   */
-  void swap(SubstitutionMap& map) {
-    d_substitutions.swap(map.d_substitutions);
-    d_substitutionCache.swap(map.d_substitutionCache);
-    std::swap(d_cacheInvalidated, map.d_cacheInvalidated);
-  }
+  // NOTE [MGD]: removed clear() and swap() from the interface
+  // when this data structure became context-dependent
+  // because they weren't used---and it's not clear how they
+  // should // best interact with cache invalidation on context
+  // pops.
 
   /**
    * Print to the output stream
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) {
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 5bb71532c..93df4fe38 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -37,22 +37,24 @@ using namespace std;
 using namespace CVC4;
 using namespace CVC4::theory;
 
-TheoryEngine::TheoryEngine(context::Context* ctxt)
+TheoryEngine::TheoryEngine(context::Context* context,
+                           context::UserContext* userContext)
 : d_propEngine(NULL),
-  d_context(ctxt),
+  d_context(context),
+  d_userContext(userContext),
   d_activeTheories(0),
-  d_sharedTerms(ctxt),
+  d_sharedTerms(context),
   d_atomPreprocessingCache(),
   d_possiblePropagations(),
-  d_hasPropagated(ctxt),
-  d_inConflict(ctxt, false),
+  d_hasPropagated(context),
+  d_inConflict(context, false),
   d_hasShutDown(false),
-  d_incomplete(ctxt, false),
-  d_sharedAssertions(ctxt),
+  d_incomplete(context, false),
+  d_sharedAssertions(context),
   d_logic(""),
-  d_propagatedLiterals(ctxt),
-  d_propagatedLiteralsIndex(ctxt, 0),
-  d_preRegistrationVisitor(this, ctxt),
+  d_propagatedLiterals(context),
+  d_propagatedLiteralsIndex(context, 0),
+  d_preRegistrationVisitor(this, context),
   d_sharedTermsVisitor(d_sharedTerms)
 {
   for(TheoryId theoryId = theory::THEORY_FIRST; theoryId != theory::THEORY_LAST; ++ theoryId) {
@@ -378,10 +380,10 @@ void TheoryEngine::shutdown() {
   theory::Rewriter::shutdown();
 }
 
-theory::Theory::SolveStatus TheoryEngine::solve(TNode literal, SubstitutionMap& substitionOut) {
+theory::Theory::SolveStatus TheoryEngine::solve(TNode literal, SubstitutionMap& substitutionOut) {
   TNode atom = literal.getKind() == kind::NOT ? literal[0] : literal;
   Trace("theory") << "TheoryEngine::solve(" << literal << "): solving with " << theoryOf(atom)->getId() << endl;
-  Theory::SolveStatus solveStatus = theoryOf(atom)->solve(literal, substitionOut);
+  Theory::SolveStatus solveStatus = theoryOf(atom)->solve(literal, substitutionOut);
   Trace("theory") << "TheoryEngine::solve(" << literal << ") => " << solveStatus << endl;
   return solveStatus;
 }
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index 04f15e89f..915373074 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -80,6 +80,9 @@ class TheoryEngine {
   /** Our context */
   context::Context* d_context;
 
+  /** Our user context */
+  context::UserContext* d_userContext;
+
   /**
    * A table of from theory IDs to theory pointers. Never use this table
    * directly, use theoryOf() instead.
@@ -343,7 +346,7 @@ class TheoryEngine {
 public:
 
   /** Constructs a theory engine */
-  TheoryEngine(context::Context* ctxt);
+  TheoryEngine(context::Context* context, context::UserContext* userContext);
 
   /** Destroys a theory engine */
   ~TheoryEngine();
@@ -356,7 +359,7 @@ public:
   inline void addTheory(theory::TheoryId theoryId) {
     Assert(d_theoryTable[theoryId] == NULL && d_theoryOut[theoryId] == NULL);
     d_theoryOut[theoryId] = new EngineOutputChannel(this, theoryId);
-    d_theoryTable[theoryId] = new TheoryClass(d_context, *d_theoryOut[theoryId], theory::Valuation(this));
+    d_theoryTable[theoryId] = new TheoryClass(d_context, d_userContext, *d_theoryOut[theoryId], theory::Valuation(this));
   }
 
   /**
@@ -407,7 +410,8 @@ public:
   /**
    * Solve the given literal with a theory that owns it.
    */
-  theory::Theory::SolveStatus solve(TNode literal, theory::SubstitutionMap& substitionOut);
+  theory::Theory::SolveStatus solve(TNode literal,
+                                    theory::SubstitutionMap& substitutionOut);
 
   /**
    * Preregister a Theory atom with the responsible theory (or
diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h
index 6cea8b85b..f8e17b1de 100644
--- a/src/theory/uf/theory_uf.h
+++ b/src/theory/uf/theory_uf.h
@@ -97,14 +97,14 @@ private:
 public:
 
   /** Constructs a new instance of TheoryUF w.r.t. the provided context.*/
-  TheoryUF(context::Context* ctxt, OutputChannel& out, Valuation valuation):
-    Theory(THEORY_UF, ctxt, out, valuation),
+  TheoryUF(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation):
+    Theory(THEORY_UF, c, u, out, valuation),
     d_notify(*this),
-    d_equalityEngine(d_notify, ctxt, "theory::uf::TheoryUF"),
-    d_knownFacts(ctxt),
-    d_conflict(ctxt, false),
-    d_literalsToPropagate(ctxt),
-    d_literalsToPropagateIndex(ctxt, 0)
+    d_equalityEngine(d_notify, c, "theory::uf::TheoryUF"),
+    d_knownFacts(c),
+    d_conflict(c, false),
+    d_literalsToPropagate(c),
+    d_literalsToPropagateIndex(c, 0)
   {
     // The kinds we are treating as function application in congruence
     d_equalityEngine.addFunctionKind(kind::APPLY_UF);