1 files changed, 42 insertions, 1 deletions
diff --git a/src/prop/sat.h b/src/prop/sat.h
index 550de5527..6e244d9d7 100644
--- a/src/prop/sat.h
+++ b/src/prop/sat.h
@@ -103,6 +103,12 @@ public:
   virtual void addClause(SatClause& clause, bool lemma) = 0;
   /** Create a new boolean variable in the solver. */
   virtual SatVariable newVar(bool theoryAtom = false) = 0;
+  /** Get the current decision level of the solver */
+  virtual int getLevel() const = 0;
+  /** Unregister the variable (of the literal) from solving */
+  virtual void unregisterVar(SatLiteral lit) = 0;
+  /** Register the variable (of the literal) for solving */
+  virtual void renewVar(SatLiteral lit, int level = -1) = 0;
 };
 
 /**
@@ -226,6 +232,21 @@ public:
   void setCnfStream(CnfStream* cnfStream);
 
   SatLiteralValue value(SatLiteral l);
+
+  int getLevel() const;
+
+  void push();
+
+  void pop();
+
+  void removeClausesAboveLevel(int level);
+
+  void unregisterVar(SatLiteral lit);
+
+  void renewVar(SatLiteral lit, int level = -1);
+
+  TNode getNode(SatLiteral lit);
+
 };/* class SatSolver */
 
 /* Functions that delegate to the concrete SAT solver. */
@@ -241,7 +262,7 @@ inline SatSolver::SatSolver(PropEngine* propEngine, TheoryEngine* theoryEngine,
   d_statistics()
 {
   // Create the solver
-  d_minisat = new Minisat::SimpSolver(this, d_context);
+  d_minisat = new Minisat::SimpSolver(this, d_context, options.incrementalSolving);
   // Setup the verbosity
   d_minisat->verbosity = (options.verbosity > 0) ? 1 : -1;
 
@@ -273,6 +294,26 @@ inline SatLiteralValue SatSolver::value(SatLiteral l) {
   return d_minisat->modelValue(l);
 }
 
+inline void SatSolver::push() {
+  d_minisat->push();
+}
+
+inline void SatSolver::pop() {
+  d_minisat->pop();
+}
+
+inline int SatSolver::getLevel() const {
+  return d_minisat->getAssertionLevel();
+}
+
+inline void SatSolver::unregisterVar(SatLiteral lit) {
+  d_minisat->unregisterVar(lit);
+}
+
+inline void SatSolver::renewVar(SatLiteral lit, int level) {
+  d_minisat->renewVar(lit, level);
+}
+
 #endif /* __CVC4_USE_MINISAT */
 
 inline size_t