1 files changed, 10 insertions, 1 deletions
diff --git a/src/prop/sat.h b/src/prop/sat.h
index 2521f3ee7..39977a96b 100644
--- a/src/prop/sat.h
+++ b/src/prop/sat.h
@@ -70,6 +70,10 @@ inline SatVariable literalToVariable(SatLiteral lit) {
   return Minisat::var(lit);
 }
 
+inline SatLiteral variableToLiteral(SatVariable var) {
+  return Minisat::mkLit(var);
+}
+
 inline bool literalSign(SatLiteral lit) {
   return Minisat::sign(lit);
 }
@@ -208,7 +212,7 @@ public:
             TheoryEngine* theoryEngine,
             context::Context* context);
 
-  ~SatSolver();
+  virtual ~SatSolver();
 
   bool solve();
 
@@ -242,6 +246,11 @@ public:
 
   void removeClausesAboveLevel(int level);
 
+  /**
+   * Notifies of a new variable at a decision level.
+   */
+  void variableNotify(SatVariable var);
+
   void unregisterVar(SatLiteral lit);
 
   void renewVar(SatLiteral lit, int level = -1);