1 files changed, 5 insertions, 1 deletions
diff --git a/src/prop/sat_module.h b/src/prop/sat_module.h
index 320dfe09b..9c49c7d67 100644
--- a/src/prop/sat_module.h
+++ b/src/prop/sat_module.h
@@ -152,6 +152,8 @@ public:
 
   virtual void pop() = 0;
 
+  virtual bool properExplanation(SatLiteral lit, SatLiteral expl) const = 0;
+
 }; 
 
 // toodo add ifdef
@@ -179,11 +181,11 @@ public:
   SatLiteralValue value(SatLiteral l);
   SatLiteralValue modelValue(SatLiteral l);
 
-
   void unregisterVar(SatLiteral lit);
   void renewVar(SatLiteral lit, int level = -1);
   int getAssertionLevel() const;
 
+
   // helper methods for converting from the internal Minisat representation
 
   static SatVariable     toSatVariable(BVMinisat::Var var); 
@@ -254,6 +256,8 @@ public:
 
   SatLiteralValue modelValue(SatLiteral l);
 
+  bool properExplanation(SatLiteral lit, SatLiteral expl) const;
+
   /** Incremental interface */ 
   
   int getAssertionLevel() const;