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

25 files changed, 181 insertions, 88 deletions

diff --git a/src/context/cdmap.h b/src/context/cdmap.h
index 3ac99f729..2a5365082 100644
--- a/src/context/cdmap.h
+++ b/src/context/cdmap.h
@@ -364,6 +364,10 @@ public:
     return d_map.size();
   }
 
+  bool empty() const {
+    return d_map.empty();
+  }
+
   size_t count(const Key& k) const {
     return d_map.count(k);
   }
diff --git a/src/context/context.h b/src/context/context.h
index 1e69964a0..78c06e7d5 100644
--- a/src/context/context.h
+++ b/src/context/context.h
@@ -95,6 +95,10 @@ class Context {
   friend std::ostream&
   operator<<(std::ostream&, const Context&) throw(AssertionException);
 
+  // disable copy, assignment
+  Context(const Context&) CVC4_UNUSED;
+  Context& operator=(const Context&) CVC4_UNUSED;
+
 public:
   /**
    * Constructor: create ContextMemoryManager and initial Scope
@@ -153,6 +157,22 @@ public:
 
 };/* class Context */
 
+
+/**
+ * A UserContext is different from a Context only because it's used for
+ * different purposes---so separating the two types gives type errors where
+ * appropriate.
+ */
+class UserContext : public Context {
+private:
+  // disable copy, assignment
+  UserContext(const UserContext&) CVC4_UNUSED;
+  UserContext& operator=(const UserContext&) CVC4_UNUSED;
+public:
+  UserContext() {}
+};/* class UserContext */
+
+
 /**
  * Conceptually, a Scope encapsulates that portion of the context that
  * changes after a call to push() and must be undone on a subsequent call to
diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp
index f013c1644..28f990c98 100644
--- a/src/expr/expr_manager_template.cpp
+++ b/src/expr/expr_manager_template.cpp
@@ -71,7 +71,7 @@ using namespace CVC4::kind;
 namespace CVC4 {
 
 ExprManager::ExprManager() :
-  d_ctxt(new Context),
+  d_ctxt(new Context()),
   d_nodeManager(new NodeManager(d_ctxt, this)) {
 #ifdef CVC4_STATISTICS_ON
   for (unsigned i = 0; i < kind::LAST_KIND; ++ i) {
@@ -84,7 +84,7 @@ ExprManager::ExprManager() :
 }
 
 ExprManager::ExprManager(const Options& options) :
-  d_ctxt(new Context),
+  d_ctxt(new Context()),
   d_nodeManager(new NodeManager(d_ctxt, this, options)) {
 #ifdef CVC4_STATISTICS_ON
   for (unsigned i = 0; i <= LAST_TYPE; ++ i) {
diff --git a/src/main/interactive_shell.cpp b/src/main/interactive_shell.cpp
index 8f1d54a3a..1d1f447be 100644
--- a/src/main/interactive_shell.cpp
+++ b/src/main/interactive_shell.cpp
@@ -18,6 +18,7 @@
  **/
 
 #include <iostream>
+#include <cstdlib>
 #include <vector>
 #include <string>
 #include <set>
@@ -92,23 +93,38 @@ InteractiveShell::InteractiveShell(ExprManager& exprManager,
   if(d_in == cin) {
     ::rl_readline_name = "CVC4";
     ::rl_completion_entry_function = commandGenerator;
+    ::using_history();
 
     switch(OutputLanguage lang = toOutputLanguage(d_language)) {
     case output::LANG_CVC4:
+      d_historyFilename = string(getenv("HOME")) + "/.cvc4_history";
       commandsBegin = cvc_commands;
       commandsEnd = cvc_commands + sizeof(cvc_commands) / sizeof(*cvc_commands);
       break;
     case output::LANG_SMTLIB:
+      d_historyFilename = string(getenv("HOME")) + "/.cvc4_history_smtlib";
       commandsBegin = smt_commands;
       commandsEnd = smt_commands + sizeof(smt_commands) / sizeof(*smt_commands);
       break;
     case output::LANG_SMTLIB_V2:
+      d_historyFilename = string(getenv("HOME")) + "/.cvc4_history_smtlib2";
       commandsBegin = smt2_commands;
       commandsEnd = smt2_commands + sizeof(smt2_commands) / sizeof(*smt2_commands);
       break;
     default: Unhandled(lang);
     }
     d_usingReadline = true;
+    int err = ::read_history(d_historyFilename.c_str());
+    ::stifle_history(s_historyLimit);
+    if(Notice.isOn()) {
+      if(err == 0) {
+        Notice() << "Read " << ::history_length << " lines of history from "
+                 << d_historyFilename << std::endl;
+      } else {
+        Notice() << "Could not read history from " << d_historyFilename
+                 << ": " << strerror(err) << std::endl;
+      }
+    }
   } else {
     d_usingReadline = false;
   }
@@ -117,6 +133,16 @@ InteractiveShell::InteractiveShell(ExprManager& exprManager,
 #endif /* HAVE_LIBREADLINE */
 }/* InteractiveShell::InteractiveShell() */
 
+InteractiveShell::~InteractiveShell() {
+  int err = ::write_history(d_historyFilename.c_str());
+  if(err == 0) {
+    Notice() << "Wrote " << ::history_length << " lines of history to "
+             << d_historyFilename << std::endl;
+  } else {
+    Notice() << "Could not write history to " << d_historyFilename
+             << ": " << strerror(err) << std::endl;
+  }
+}
 
 Command* InteractiveShell::readCommand() {
   /* Don't do anything if the input is closed or if we've seen a
diff --git a/src/main/interactive_shell.h b/src/main/interactive_shell.h
index f6852b95b..65fea8494 100644
--- a/src/main/interactive_shell.h
+++ b/src/main/interactive_shell.h
@@ -40,12 +40,20 @@ class CVC4_PUBLIC InteractiveShell {
   bool d_quit;
   bool d_usingReadline;
 
+  std::string d_historyFilename;
+
   static const std::string INPUT_FILENAME;
+  static const unsigned s_historyLimit = 500;
 
 public:
   InteractiveShell(ExprManager& exprManager, const Options& options);
 
   /**
+   * Close out the interactive session.
+   */
+  ~InteractiveShell();
+
+  /**
    * Read a command from the interactive shell. This will read as
    * many lines as necessary to parse a well-formed command.
    */
diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc
index 770433489..f3a85ed5e 100644
--- a/src/prop/minisat/core/Solver.cc
+++ b/src/prop/minisat/core/Solver.cc
@@ -1100,7 +1100,7 @@ lbool Solver::solve_()
         ok = false;
 
     // Cancel the trail downto previous push
-    popTrail();
+    //popTrail();
 
     return status;
 }
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 24ebf9bfd..86d06520a 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -101,7 +101,7 @@ public:
 class SmtEnginePrivate {
   SmtEngine& d_smt;
 
-  /** The assertions yet to be preprecessed */
+  /** The assertions yet to be preprocessed */
   vector<Node> d_assertionsToPreprocess;
 
   /** Learned literals */
@@ -138,7 +138,10 @@ class SmtEnginePrivate {
 
 public:
 
-  SmtEnginePrivate(SmtEngine& smt) : d_smt(smt) { }
+  SmtEnginePrivate(SmtEngine& smt) :
+    d_smt(smt),
+    d_topLevelSubstitutions(smt.d_userContext) {
+  }
 
   Node applySubstitutions(TNode node) const {
     return Rewriter::rewrite(d_topLevelSubstitutions.apply(node));
@@ -172,7 +175,7 @@ using namespace CVC4::smt;
 
 SmtEngine::SmtEngine(ExprManager* em) throw(AssertionException) :
   d_context(em->getContext()),
-  d_userContext(new Context()),
+  d_userContext(new UserContext()),
   d_exprManager(em),
   d_nodeManager(d_exprManager->getNodeManager()),
   d_private(new smt::SmtEnginePrivate(*this)),
@@ -186,9 +189,9 @@ SmtEngine::SmtEngine(ExprManager* em) throw(AssertionException) :
   StatisticsRegistry::registerStat(&d_nonclausalSimplificationTime);
   StatisticsRegistry::registerStat(&d_staticLearningTime);
 
-  // We have mutual dependancy here, so we add the prop engine to the theory
+  // We have mutual dependency here, so we add the prop engine to the theory
   // engine later (it is non-essential there)
-  d_theoryEngine = new TheoryEngine(d_context);
+  d_theoryEngine = new TheoryEngine(d_context, d_userContext);
 
   // Add the theories
   d_theoryEngine->addTheory<theory::builtin::TheoryBuiltin>(theory::THEORY_BUILTIN);
@@ -927,8 +930,11 @@ Expr SmtEngine::getValue(const Expr& e)
     throw ModalException(msg);
   }
 
+  // Apply what was learned from preprocessing
+  Node n = d_private->applySubstitutions(e.getNode());
+
   // Normalize for the theories
-  Node n = theory::Rewriter::rewrite(e.getNode());
+  n = theory::Rewriter::rewrite(n);
 
   Trace("smt") << "--- getting value of " << n << endl;
   Node resultNode = d_theoryEngine->getValue(n);
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index d2abf2fce..7a5f39056 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -54,6 +54,7 @@ class StatisticsRegistry;
 
 namespace context {
   class Context;
+  class UserContext;
 }/* CVC4::context namespace */
 
 namespace prop {
@@ -99,7 +100,7 @@ class CVC4_PUBLIC SmtEngine {
   /** The context levels of user pushes */
   std::vector<int> d_userLevels;
   /** User level context */
-  context::Context* d_userContext;
+  context::UserContext* d_userContext;
 
   /** Our expression manager */
   ExprManager* d_exprManager;
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);