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

2 files changed, 14 insertions, 7 deletions

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;