1 files changed, 26 insertions, 4 deletions
diff --git a/src/prop/bvminisat/bvminisat.h b/src/prop/bvminisat/bvminisat.h
index 19b605067..cd2a2c6b9 100644
--- a/src/prop/bvminisat/bvminisat.h
+++ b/src/prop/bvminisat/bvminisat.h
@@ -26,14 +26,36 @@
 namespace CVC4 {
 namespace prop {
 
-class BVMinisatSatSolver: public BVSatSolverInterface, public context::ContextNotifyObj {
+class BVMinisatSatSolver : public BVSatSolverInterface, public context::ContextNotifyObj {
+
+private:
+
+  class MinisatNotify : public BVMinisat::Notify {
+    BVSatSolverInterface::Notify* d_notify;
+  public:
+    MinisatNotify(BVSatSolverInterface::Notify* notify)
+    : d_notify(notify)
+    {}
+    bool notify(BVMinisat::Lit lit) {
+      return d_notify->notify(toSatLiteral(lit));
+    }
+    void notify(BVMinisat::vec<BVMinisat::Lit>& clause) {
+      SatClause satClause;
+      toSatClause(clause, satClause);
+      d_notify->notify(satClause);
+    }
+  };
+
   BVMinisat::SimpSolver* d_minisat;
+  MinisatNotify* d_minisatNotify;
+
   unsigned d_solveCount;
   unsigned d_assertionsCount;
   context::CDO<unsigned> d_assertionsRealCount;
   context::CDO<unsigned> d_lastPropagation;
 
 public:
+
   BVMinisatSatSolver() :
     ContextNotifyObj(NULL, false),
     d_assertionsRealCount(NULL, (unsigned)0),
@@ -42,6 +64,8 @@ public:
   BVMinisatSatSolver(context::Context* mainSatContext);
   ~BVMinisatSatSolver() throw(AssertionException);
 
+  void setNotify(Notify* notify);
+
   void addClause(SatClause& clause, bool removable);
 
   SatVariable newVar(bool theoryAtom = false);
@@ -76,9 +100,7 @@ public:
   static void  toSatClause    (BVMinisat::vec<BVMinisat::Lit>& clause, SatClause& sat_clause);
   void addMarkerLiteral(SatLiteral lit);
 
-  bool getPropagations(std::vector<SatLiteral>& propagations);
-
-  void explainPropagation(SatLiteral lit, std::vector<SatLiteral>& explanation);
+  void explain(SatLiteral lit, std::vector<SatLiteral>& explanation);
 
   SatValue assertAssumption(SatLiteral lit, bool propagate);