From df5f7fe03fda041429548bcb39abb8916ca2e291 Mon Sep 17 00:00:00 2001
From: Dejan Jovanović <dejan.jovanovic@gmail.com>
Date: Tue, 9 Nov 2010 21:57:06 +0000
Subject: Lemmas on demand work, push-pop, some cleanup.

---
 src/smt/smt_engine.h | 17 +++++++++++------
 1 file changed, 11 insertions(+), 6 deletions(-)

(limited to 'src/smt/smt_engine.h')

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:
-- 
cgit v1.2.3