Lemmas on demand work, push-pop, some cleanup.

2 files changed, 44 insertions, 19 deletions

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 151f7237b..bf74ab844 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -124,24 +124,24 @@ SmtEngine::SmtEngine(ExprManager* em, const Options& opts) throw() :
 
 void SmtEngine::init(const Options& opts) throw() {
   d_context = d_exprManager->getContext();
+  d_userContext = new Context();
+
   d_nodeManager = d_exprManager->getNodeManager();
 
   NodeManagerScope nms(d_nodeManager);
 
-  d_decisionEngine = new DecisionEngine;
   // We have mutual dependancy here, so we add the prop engine to the theory
   // engine later (it is non-essential there)
   d_theoryEngine = new TheoryEngine(d_context, opts);
-  d_propEngine = new PropEngine(d_decisionEngine, d_theoryEngine, 
-                                d_context, opts);
+  d_propEngine = new PropEngine(d_theoryEngine, d_context, opts);
   d_theoryEngine->setPropEngine(d_propEngine);
 
-  d_definedFunctions = new(true) DefinedFunctionMap(d_context);
+  d_definedFunctions = new(true) DefinedFunctionMap(d_userContext);
 
   d_assertionList = NULL;
   d_interactive = opts.interactive;
   if(d_interactive) {
-    d_assertionList = new(true) AssertionList(d_context);
+    d_assertionList = new(true) AssertionList(d_userContext);
   }
 
   d_assignments = NULL;
@@ -156,7 +156,6 @@ void SmtEngine::init(const Options& opts) throw() {
 void SmtEngine::shutdown() {
   d_propEngine->shutdown();
   d_theoryEngine->shutdown();
-  d_decisionEngine->shutdown();
 }
 
 SmtEngine::~SmtEngine() {
@@ -174,9 +173,10 @@ SmtEngine::~SmtEngine() {
 
   d_definedFunctions->deleteSelf();
 
+  delete d_userContext;
+
   delete d_theoryEngine;
   delete d_propEngine;
-  delete d_decisionEngine;
 }
 
 void SmtEngine::setLogic(const std::string& s) throw(ModalException) {
@@ -457,8 +457,10 @@ Result SmtEngine::checkSat(const BoolExpr& e) {
   NodeManagerScope nms(d_nodeManager);
   Debug("smt") << "SMT checkSat(" << e << ")" << endl;
   ensureBoolean(e);// ensure expr is type-checked at this point
+  internalPush();
   SmtEnginePrivate::addFormula(*this, e.getNode());
   Result r = check().asSatisfiabilityResult();
+  internalPop();
   d_status = r;
   d_haveAdditions = false;
   Debug("smt") << "SMT checkSat(" << e << ") ==> " << r << endl;
@@ -470,8 +472,10 @@ Result SmtEngine::query(const BoolExpr& e) {
   NodeManagerScope nms(d_nodeManager);
   Debug("smt") << "SMT query(" << e << ")" << endl;
   ensureBoolean(e);// ensure expr is type-checked at this point
+  internalPush();
   SmtEnginePrivate::addFormula(*this, e.getNode().notNode());
   Result r = check().asValidityResult();
+  internalPop();
   d_status = r;
   d_haveAdditions = false;
   Debug("smt") << "SMT query(" << e << ") ==> " << r << endl;
@@ -629,21 +633,37 @@ vector<Expr> SmtEngine::getAssertions()
 void SmtEngine::push() {
   NodeManagerScope nms(d_nodeManager);
   Debug("smt") << "SMT push()" << endl;
-  d_context->push();
-  d_propEngine->push();
+  d_userLevels.push_back(d_userContext->getLevel());
+  internalPush();
   Debug("userpushpop") << "SmtEngine: pushed to level "
-                       << d_context->getLevel() << endl;
+                       << d_userContext->getLevel() << endl;
 }
 
 void SmtEngine::pop() {
   NodeManagerScope nms(d_nodeManager);
   Debug("smt") << "SMT pop()" << endl;
-  d_propEngine->pop();
-  d_context->pop();
+  Assert(d_userLevels.size() > 0 && d_userLevels.back() < d_userContext->getLevel());
+  while (d_userLevels.back() < d_userContext->getLevel()) {
+    internalPop();
+  }
+  d_userLevels.pop_back();
+
   Debug("userpushpop") << "SmtEngine: popped to level "
-                       << d_context->getLevel() << endl;
+                       << d_userContext->getLevel() << endl;
   // FIXME: should we reset d_status here?
   // SMT-LIBv2 spec seems to imply no, but it would make sense to..
 }
 
+void SmtEngine::internalPop() {
+  Debug("smt") << "internalPop()" << endl;
+  d_propEngine->pop();
+  d_userContext->pop();
+}
+
+void SmtEngine::internalPush() {
+  Debug("smt") << "internalPush()" << endl;
+  d_userContext->push();
+  d_propEngine->push();
+}
+
 }/* CVC4 namespace */
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 854399bd7..d8d9f4b54 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -48,7 +48,6 @@ typedef NodeTemplate<false> TNode;
 class NodeHashFunction;
 
 class TheoryEngine;
-class DecisionEngine;
 
 namespace context {
   class Context;
@@ -91,16 +90,18 @@ class CVC4_PUBLIC SmtEngine {
   /** The type of our internal assignment set */
   typedef context::CDSet<Node, NodeHashFunction> AssignmentSet;
 
-  /** Our Context */
+  /** Expr manager context */
   context::Context* d_context;
+
+  /** The context levels of user pushes */
+  std::vector<int> d_userLevels;
+  /** User level context */
+  context::Context* d_userContext;
+
   /** Our expression manager */
   ExprManager* d_exprManager;
   /** Out internal expression/node manager */
   NodeManager* d_nodeManager;
-  /** User-level options */
-  //const Options d_options;
-  /** The decision engine */
-  DecisionEngine* d_decisionEngine;
   /** The decision engine */
   TheoryEngine* d_theoryEngine;
   /** The propositional engine */
@@ -190,6 +191,10 @@ class CVC4_PUBLIC SmtEngine {
    */
   void ensureBoolean(const BoolExpr& e);
 
+  void internalPush();
+
+  void internalPop();
+
   friend class ::CVC4::smt::SmtEnginePrivate;
 
 public: