Merging in bvprop branch, with proper bit-vector propagation.

This should also fix bug 325. 

1 files changed, 21 insertions, 3 deletions

diff --git a/src/prop/sat_solver.h b/src/prop/sat_solver.h
index 4fe24fc60..898709c43 100644
--- a/src/prop/sat_solver.h
+++ b/src/prop/sat_solver.h
@@ -73,15 +73,33 @@ public:
 class BVSatSolverInterface: public SatSolver {
 public:
 
+  /** Interface for notifications */
+  class Notify {
+  public:
+
+    virtual ~Notify() {};
+
+    /**
+     * If the notify returns false, the solver will break out of whatever it's currently doing
+     * with an "unknown" answer.
+     */
+    virtual bool notify(SatLiteral lit) = 0;
+
+    /**
+     * Notify about a learnt clause.
+     */
+    virtual void notify(SatClause& clause) = 0;
+};
+
+  virtual void setNotify(Notify* notify) = 0; 
+  
   virtual void markUnremovable(SatLiteral lit) = 0;
 
   virtual void getUnsatCore(SatClause& unsatCore) = 0; 
 
   virtual void addMarkerLiteral(SatLiteral lit) = 0; 
 
-  virtual bool getPropagations(std::vector<SatLiteral>& propagations) = 0;
-
-  virtual void explainPropagation(SatLiteral lit, std::vector<SatLiteral>& explanation) = 0;
+  virtual void explain(SatLiteral lit, std::vector<SatLiteral>& explanation) = 0;
 
   virtual SatValue assertAssumption(SatLiteral lit, bool propagate = false) = 0;