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

This should also fix bug 325. 

9 files changed, 202 insertions, 108 deletions

diff --git a/src/prop/bvminisat/bvminisat.cpp b/src/prop/bvminisat/bvminisat.cpp
index 232502696..124fc35f1 100644
--- a/src/prop/bvminisat/bvminisat.cpp
+++ b/src/prop/bvminisat/bvminisat.cpp
@@ -25,6 +25,7 @@ using namespace prop;
 BVMinisatSatSolver::BVMinisatSatSolver(context::Context* mainSatContext)
 : context::ContextNotifyObj(mainSatContext, false),
   d_minisat(new BVMinisat::SimpSolver(mainSatContext)),
+  d_minisatNotify(0),
   d_solveCount(0),
   d_assertionsCount(0),
   d_assertionsRealCount(mainSatContext, 0),
@@ -36,6 +37,12 @@ BVMinisatSatSolver::BVMinisatSatSolver(context::Context* mainSatContext)
 
 BVMinisatSatSolver::~BVMinisatSatSolver() throw(AssertionException) {
   delete d_minisat;
+  delete d_minisatNotify;
+}
+
+void BVMinisatSatSolver::setNotify(Notify* notify) {
+  d_minisatNotify = new MinisatNotify(notify);
+  d_minisat->setNotify(d_minisatNotify);
 }
 
 void BVMinisatSatSolver::addClause(SatClause& clause, bool removable) {
@@ -52,16 +59,9 @@ void BVMinisatSatSolver::addMarkerLiteral(SatLiteral lit) {
   d_minisat->addMarkerLiteral(BVMinisat::var(toMinisatLit(lit)));
 }
 
-bool BVMinisatSatSolver::getPropagations(std::vector<SatLiteral>& propagations) {
-  for (; d_lastPropagation < d_minisat->atom_propagations.size(); d_lastPropagation = d_lastPropagation + 1) {
-    propagations.push_back(toSatLiteral(d_minisat->atom_propagations[d_lastPropagation]));
-  }
-  return propagations.size() > 0; 
-}
-
-void BVMinisatSatSolver::explainPropagation(SatLiteral lit, std::vector<SatLiteral>& explanation) {
+void BVMinisatSatSolver::explain(SatLiteral lit, std::vector<SatLiteral>& explanation) {
   std::vector<BVMinisat::Lit> minisat_explanation;
-  d_minisat->explainPropagation(toMinisatLit(lit), minisat_explanation);
+  d_minisat->explain(toMinisatLit(lit), minisat_explanation);
   for (unsigned i = 0; i < minisat_explanation.size(); ++i) {
     explanation.push_back(toSatLiteral(minisat_explanation[i])); 
   }
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);
   
diff --git a/src/prop/bvminisat/core/Solver.cc b/src/prop/bvminisat/core/Solver.cc
index 9bded3db5..e24fcac1a 100644
--- a/src/prop/bvminisat/core/Solver.cc
+++ b/src/prop/bvminisat/core/Solver.cc
@@ -24,8 +24,10 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #include "core/Solver.h"
 #include <vector>
 #include <iostream>
+
 #include "util/output.h"
 #include "util/utility.h"
+#include "util/options.h"
 
 using namespace BVMinisat;
 
@@ -51,14 +53,14 @@ static const char* _cat = "CORE";
 
 static DoubleOption  opt_var_decay         (_cat, "var-decay",   "The variable activity decay factor",            0.95,     DoubleRange(0, false, 1, false));
 static DoubleOption  opt_clause_decay      (_cat, "cla-decay",   "The clause activity decay factor",              0.999,    DoubleRange(0, false, 1, false));
-static DoubleOption  opt_random_var_freq   (_cat, "rnd-freq",    "The frequency with which the decision heuristic tries to choose a random variable", 0, DoubleRange(0, true, 1, true));
+static DoubleOption  opt_random_var_freq   (_cat, "rnd-freq",    "The frequency with which the decision heuristic tries to choose a random variable", 0.0, DoubleRange(0, true, 1, true));
 static DoubleOption  opt_random_seed       (_cat, "rnd-seed",    "Used by the random variable selection",         91648253, DoubleRange(0, false, HUGE_VAL, false));
-static IntOption     opt_ccmin_mode        (_cat, "ccmin-mode",  "Controls conflict clause minimization (0=none, 1=basic, 2=deep)", 0, IntRange(0, 0));
+static IntOption     opt_ccmin_mode        (_cat, "ccmin-mode",  "Controls conflict clause minimization (0=none, 1=basic, 2=deep)", 0, IntRange(0, 2));
 static IntOption     opt_phase_saving      (_cat, "phase-saving", "Controls the level of phase saving (0=none, 1=limited, 2=full)", 2, IntRange(0, 2));
 static BoolOption    opt_rnd_init_act      (_cat, "rnd-init",    "Randomize the initial activity", false);
 static BoolOption    opt_luby_restart      (_cat, "luby",        "Use the Luby restart sequence", true);
 static IntOption     opt_restart_first     (_cat, "rfirst",      "The base restart interval", 100, IntRange(1, INT32_MAX));
-static DoubleOption  opt_restart_inc       (_cat, "rinc",        "Restart interval increase factor", 2, DoubleRange(1, false, HUGE_VAL, false));
+static DoubleOption  opt_restart_inc       (_cat, "rinc",        "Restart interval increase factor", 1.5, DoubleRange(1, false, HUGE_VAL, false));
 static DoubleOption  opt_garbage_frac      (_cat, "gc-frac",     "The fraction of wasted memory allowed before a garbage collection is triggered",  0.20, DoubleRange(0, false, HUGE_VAL, false));
 
 
@@ -70,7 +72,8 @@ Solver::Solver(CVC4::context::Context* c) :
 
     // Parameters (user settable):
     //
-    verbosity        (0)
+    c(c)
+  , verbosity        (0)
   , var_decay        (opt_var_decay)
   , clause_decay     (opt_clause_decay)
   , random_var_freq  (opt_random_var_freq)
@@ -86,7 +89,7 @@ Solver::Solver(CVC4::context::Context* c) :
 
     // Parameters (the rest):
     //
-  , learntsize_factor((double)1/(double)3), learntsize_inc(1.1)
+  , learntsize_factor((double)1/(double)3), learntsize_inc(1.5)
 
     // Parameters (experimental):
     //
@@ -115,7 +118,7 @@ Solver::Solver(CVC4::context::Context* c) :
   , conflict_budget    (-1)
   , propagation_budget (-1)
   , asynch_interrupt   (false)
-  , d_explanations(c)
+  , clause_added(false)
 {}
 
 
@@ -153,9 +156,9 @@ Var Solver::newVar(bool sign, bool dvar)
 
 bool Solver::addClause_(vec<Lit>& ps)
 {
-  if (decisionLevel() > 0) {
-    cancelUntil(0);
-  }
+    if (decisionLevel() > 0) {
+      cancelUntil(0);
+    }
     
     if (!ok) return false;
 
@@ -169,6 +172,8 @@ bool Solver::addClause_(vec<Lit>& ps)
             ps[j++] = p = ps[i];
     ps.shrink(i - j);
 
+    clause_added = true;
+
     if (ps.size() == 0)
         return ok = false;
     else if (ps.size() == 1){
@@ -183,7 +188,6 @@ bool Solver::addClause_(vec<Lit>& ps)
     return true;
 }
 
-
 void Solver::attachClause(CRef cr) {
     const Clause& c = ca[cr];
     assert(c.size() > 1);
@@ -242,11 +246,6 @@ void Solver::cancelUntil(int level) {
         trail.shrink(trail.size() - trail_lim[level]);
         trail_lim.shrink(trail_lim.size() - level);
     }
-
-    if (level < atom_propagations_lim.size()) {
-      atom_propagations.shrink(atom_propagations.size() - atom_propagations_lim[level]);
-      atom_propagations_lim.shrink(atom_propagations_lim.size() - level);
-    }
 }
 
 
@@ -379,12 +378,24 @@ void Solver::analyze(CRef confl, vec<Lit>& out_learnt, int& out_btlevel, UIP uip
     out_learnt.shrink(i - j);
     tot_literals += out_learnt.size();
 
+    bool clause_all_marker = true;
+    for (int i = 0; i < out_learnt.size(); ++ i) {
+      if (marker[var(out_learnt[i])] == 0) {
+        clause_all_marker = false;
+        break;
+      }
+    }
+
     // Find correct backtrack level:
     //
-    if (out_learnt.size() == 1)
-        out_btlevel = 0;
+    if (out_learnt.size() == 1) {
+      out_btlevel = 0;
+    }
     else{
         int max_i = 1;
+        if (marker[var(out_learnt[0])] == 0) {
+          clause_all_marker = false;
+        }
         // Find the first literal assigned at the next-highest level:
         for (int i = 2; i < out_learnt.size(); i++)
             if (level(var(out_learnt[i])) > level(var(out_learnt[max_i])))
@@ -396,6 +407,10 @@ void Solver::analyze(CRef confl, vec<Lit>& out_learnt, int& out_btlevel, UIP uip
         out_btlevel       = level(var(p));
     }
 
+    if (out_learnt.size() > 0 && clause_all_marker && CVC4::Options::current()->bitvector_share_lemmas) {
+      notify->notify(out_learnt);
+    }
+
     for (int j = 0; j < analyze_toclear.size(); j++) seen[var(analyze_toclear[j])] = 0;    // ('seen[]' is now cleared)
 }
 
@@ -452,17 +467,16 @@ void Solver::analyzeFinal(Lit p, vec<Lit>& out_conflict)
 
     for (int i = trail.size()-1; i >= trail_lim[0]; i--){
         Var x = var(trail[i]);
-        if (seen[x]){
-            if (reason(x) == CRef_Undef){
-              if (marker[x] == 2) {
-                assert(level(x) > 0);
-                out_conflict.push(~trail[i]);
-              }
-            }else{
-                Clause& c = ca[reason(x)];
-                for (int j = 1; j < c.size(); j++)
-                    if (level(var(c[j])) > 0)
-                        seen[var(c[j])] = 1;
+        if (seen[x]) {
+            if (reason(x) == CRef_Undef) {
+              assert(marker[x] == 2);
+              assert(level(x) > 0);
+              out_conflict.push(~trail[i]);
+            } else {
+              Clause& c = ca[reason(x)];
+              for (int j = 1; j < c.size(); j++)
+                if (level(var(c[j])) > 0)
+                  seen[var(c[j])] = 1;
             }
             seen[x] = 0;
         }
@@ -478,31 +492,44 @@ void Solver::uncheckedEnqueue(Lit p, CRef from)
     assigns[var(p)] = lbool(!sign(p));
     vardata[var(p)] = mkVarData(from, decisionLevel());
     trail.push_(p);
-    if (only_bcp && marker[var(p)] == 1 && from != CRef_Undef) {
-      atom_propagations.push(p);
+    if (decisionLevel() <= assumptions.size() && marker[var(p)] == 1) {
+      if (notify) {
+        notify->notify(p);
+      }
     }
 }
 
 void Solver::popAssumption() {
-  marker[var(assumptions.last())] = 1;
-  assumptions.pop();
-  conflict.clear();
-  cancelUntil(assumptions.size());
+    assumptions.pop();
+    conflict.clear();
+    cancelUntil(assumptions.size());
 }
 
 lbool Solver::assertAssumption(Lit p, bool propagate) {
 
   assert(marker[var(p)] == 1);
 
-  // add to the assumptions
-  assumptions.push(p);
+  if (decisionLevel() > assumptions.size()) {
+    cancelUntil(assumptions.size());
+  }
+
   conflict.clear();
 
+  // add to the assumptions
+  if (c->getLevel() > 0) {
+    assumptions.push(p);
+  } else {
+    if (!addClause(p)) {
+      conflict.push(~p);
+      return l_False;
+    }
+  }
+
   // run the propagation
   if (propagate) {
     only_bcp = true;
     ccmin_mode = 0; 
-    lbool result = search(-1, UIP_FIRST);
+    lbool result = search(-1);
     return result; 
   } else {
     return l_True;
@@ -702,11 +729,12 @@ lbool Solver::search(int nof_conflicts, UIP uip)
 
             learnt_clause.clear();
             analyze(confl, learnt_clause, backtrack_level, uip);
-            cancelUntil(backtrack_level);
 
             Lit p = learnt_clause[0];
             bool assumption = marker[var(p)] == 2;
 
+            cancelUntil(backtrack_level);
+
             if (learnt_clause.size() == 1){
                 uncheckedEnqueue(p);
             }else{
@@ -741,10 +769,10 @@ lbool Solver::search(int nof_conflicts, UIP uip)
 
         }else{
             // NO CONFLICT
-            if (nof_conflicts >= 0 && conflictC >= nof_conflicts || !withinBudget()){
+            if (decisionLevel() > assumptions.size() && nof_conflicts >= 0 && conflictC >= nof_conflicts || !withinBudget()){
                 // Reached bound on number of conflicts:
                 progress_estimate = progressEstimate();
-                cancelUntil(0);
+                cancelUntil(assumptions.size());
                 return l_Undef; }
 
             // Simplify the set of problem clauses:
@@ -890,31 +918,27 @@ lbool Solver::solve_()
 // Bitvector propagations
 // 
 
-void Solver::storeExplanation(Lit p) {
-}
+void Solver::explain(Lit p, std::vector<Lit>& explanation) {
 
-void Solver::explainPropagation(Lit p, std::vector<Lit>& explanation) {
   vec<Lit> queue;
   queue.push(p);
 
   __gnu_cxx::hash_set<Var> visited;
   visited.insert(var(p));
+  
   while(queue.size() > 0) {
     Lit l = queue.last();
     assert(value(l) == l_True);
     queue.pop();
     if (reason(var(l)) == CRef_Undef) {
-      if (marker[var(l)] == 2) {
-        explanation.push_back(l);
-        visited.insert(var(l));
-      }
+      if (level(var(l)) == 0) continue;
+      Assert(marker[var(l)] == 2);
+      explanation.push_back(l);
+      visited.insert(var(l));
     } else {
       Clause& c = ca[reason(var(l))];
       for (int i = 1; i < c.size(); ++i) {
-        if (var(c[i]) >= vardata.size()) {
-          std::cerr << "BOOM" << std::endl;
-        }
-        if (visited.count(var(c[i])) == 0) {
+        if (level(var(c[i])) > 0 && visited.count(var(c[i])) == 0) {
           queue.push(~c[i]);
           visited.insert(var(c[i]));
         }
diff --git a/src/prop/bvminisat/core/Solver.h b/src/prop/bvminisat/core/Solver.h
index c7346d7f7..c323bfe2b 100644
--- a/src/prop/bvminisat/core/Solver.h
+++ b/src/prop/bvminisat/core/Solver.h
@@ -34,10 +34,36 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 
 namespace BVMinisat {
 
+/** Interface for minisat callbacks */
+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(Lit lit) = 0;
+
+  /**
+   * Notify about a new learnt clause with marked literals only.
+   */
+  virtual void notify(vec<Lit>& learnt) = 0;
+
+};
+
 //=================================================================================================
 // Solver -- the main class:
-
 class Solver {
+
+    /** To notify */
+    Notify* notify;
+
+    /** Cvc4 context */
+    CVC4::context::Context* c;
+
 public:
 
     // Constructor/Destructor:
@@ -45,6 +71,8 @@ public:
     Solver(CVC4::context::Context* c);
     virtual ~Solver();
 
+    void setNotify(Notify* toNotify) { notify = toNotify; }
+
     // Problem specification:
     //
     Var     newVar    (bool polarity = true, bool dvar = true); // Add a new variable with parameters specifying variable mode.
@@ -153,15 +181,15 @@ public:
       marker[var] = 1;
     }
 
-    __gnu_cxx::hash_set<Var> assumptions_vars; // all the variables that appear in the current assumptions
-    vec<Lit> atom_propagations;         // the atom literals implied by the last call to solve with assumptions
-    vec<int> atom_propagations_lim;     // for backtracking
-
     bool only_bcp;                      // solving mode in which only boolean constraint propagation is done
     void setOnlyBCP (bool val) { only_bcp = val;}
-    void explainPropagation(Lit l, std::vector<Lit>& explanation);
+    void explain(Lit l, std::vector<Lit>& explanation);
+
 protected:
 
+    // has a clause been added
+    bool                clause_added;
+
     // Helper structures:
     //
     struct VarData { CRef reason; int level; };
@@ -248,9 +276,6 @@ protected:
       UIP_LAST
     };
 
-    CVC4::context::CDHashMap<Lit, std::vector<Lit>, LitHashFunction> d_explanations;
-
-    void     storeExplanation (Lit p);                                                 // make sure that the explanation of p is cached
     void     analyze          (CRef confl, vec<Lit>& out_learnt, int& out_btlevel, UIP uip = UIP_FIRST);    // (bt = backtrack)
     void     analyzeFinal     (Lit p, vec<Lit>& out_conflict);                         // COULD THIS BE IMPLEMENTED BY THE ORDINARIY "analyze" BY SOME REASONABLE GENERALIZATION?
     bool     litRedundant     (Lit p, uint32_t abstract_levels);                       // (helper method for 'analyze()')
@@ -346,7 +371,7 @@ inline bool     Solver::addClause       (Lit p)                 { add_tmp.clear(
 inline bool     Solver::addClause       (Lit p, Lit q)          { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); return addClause_(add_tmp); }
 inline bool     Solver::addClause       (Lit p, Lit q, Lit r)   { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); add_tmp.push(r); return addClause_(add_tmp); }
 inline bool     Solver::locked          (const Clause& c) const { return value(c[0]) == l_True && reason(var(c[0])) != CRef_Undef && ca.lea(reason(var(c[0]))) == &c; }
-inline void     Solver::newDecisionLevel()                      { trail_lim.push(trail.size()); atom_propagations_lim.push(atom_propagations.size()); }
+inline void     Solver::newDecisionLevel()                      { trail_lim.push(trail.size()); }
 
 inline int      Solver::decisionLevel ()      const   { return trail_lim.size(); }
 inline uint32_t Solver::abstractLevel (Var x) const   { return 1 << (level(x) & 31); }
@@ -381,10 +406,10 @@ inline bool     Solver::withinBudget() const {
 // FIXME: after the introduction of asynchronous interrruptions the solve-versions that return a
 // pure bool do not give a safe interface. Either interrupts must be possible to turn off here, or
 // all calls to solve must return an 'lbool'. I'm not yet sure which I prefer.
-inline bool     Solver::solve         ()                    { budgetOff(); assumptions.clear(); return solve_() == l_True; }
-inline bool     Solver::solve         (Lit p)               { budgetOff(); assumptions.clear(); assumptions.push(p); return solve_() == l_True; }
-inline bool     Solver::solve         (Lit p, Lit q)        { budgetOff(); assumptions.clear(); assumptions.push(p); assumptions.push(q); return solve_() == l_True; }
-inline bool     Solver::solve         (Lit p, Lit q, Lit r) { budgetOff(); assumptions.clear(); assumptions.push(p); assumptions.push(q); assumptions.push(r); return solve_() == l_True; }
+inline bool     Solver::solve         ()                    { budgetOff(); return solve_() == l_True; }
+inline bool     Solver::solve         (Lit p)               { budgetOff(); assumptions.push(p); return solve_() == l_True; }
+inline bool     Solver::solve         (Lit p, Lit q)        { budgetOff(); assumptions.push(p); assumptions.push(q); return solve_() == l_True; }
+inline bool     Solver::solve         (Lit p, Lit q, Lit r) { budgetOff(); assumptions.push(p); assumptions.push(q); assumptions.push(r); return solve_() == l_True; }
 inline bool     Solver::solve         (const vec<Lit>& assumps){ budgetOff(); assumps.copyTo(assumptions); return solve_() == l_True; }
 inline lbool    Solver::solveLimited  (const vec<Lit>& assumps){ assumps.copyTo(assumptions); return solve_(); }
 inline bool     Solver::okay          ()      const   { return ok; }
diff --git a/src/prop/bvminisat/simp/SimpSolver.cc b/src/prop/bvminisat/simp/SimpSolver.cc
index 903ffa270..c8ce13410 100644
--- a/src/prop/bvminisat/simp/SimpSolver.cc
+++ b/src/prop/bvminisat/simp/SimpSolver.cc
@@ -32,7 +32,7 @@ static const char* _cat = "SIMP";
 
 static BoolOption   opt_use_asymm        (_cat, "asymm",        "Shrink clauses by asymmetric branching.", false);
 static BoolOption   opt_use_rcheck       (_cat, "rcheck",       "Check if a clause is already implied. (costly)", false);
-static BoolOption   opt_use_elim         (_cat, "elim",         "Perform variable elimination.", true);
+static BoolOption   opt_use_elim         (_cat, "elim",         "Perform variable elimination.", false);
 static IntOption    opt_grow             (_cat, "grow",         "Allow a variable elimination step to grow by a number of clauses.", 0);
 static IntOption    opt_clause_lim       (_cat, "cl-lim",       "Variables are not eliminated if it produces a resolvent with a length above this limit. -1 means no limit", 20,   IntRange(-1, INT32_MAX));
 static IntOption    opt_subsumption_lim  (_cat, "sub-lim",      "Do not check if subsumption against a clause larger than this. -1 means no limit.", 1000, IntRange(-1, INT32_MAX));
@@ -100,20 +100,14 @@ Var SimpSolver::newVar(bool sign, bool dvar, bool freeze) {
 
 lbool SimpSolver::solve_(bool do_simp, bool turn_off_simp)
 {
-    vec<Lit> atom_propagations_backup;
-    atom_propagations.moveTo(atom_propagations_backup);
-    vec<int> atom_propagations_lim_backup;
-    atom_propagations_lim.moveTo(atom_propagations_lim_backup);
-
     only_bcp = false;
-    cancelUntil(0);
   
     vec<Var> extra_frozen;
     lbool    result = l_True;
 
     do_simp &= use_simplification;
 
-    if (do_simp){
+    if (do_simp) {
         // Assumptions must be temporarily frozen to run variable elimination:
         for (int i = 0; i < assumptions.size(); i++){
             Var v = var(assumptions[i]);
@@ -127,7 +121,11 @@ lbool SimpSolver::solve_(bool do_simp, bool turn_off_simp)
                 extra_frozen.push(v);
             } }
 
-        result = lbool(eliminate(turn_off_simp));
+        if (do_simp && clause_added) {
+          cancelUntil(0);
+          result = lbool(eliminate(turn_off_simp));
+          clause_added = false;
+        }
     }
 
     if (result == l_True)
@@ -135,9 +133,6 @@ lbool SimpSolver::solve_(bool do_simp, bool turn_off_simp)
     else if (verbosity >= 1)
         printf("===============================================================================\n");
 
-    atom_propagations_backup.moveTo(atom_propagations);
-    atom_propagations_lim_backup.moveTo(atom_propagations_lim);
-
     if (do_simp)
         // Unfreeze the assumptions that were frozen:
         for (int i = 0; i < extra_frozen.size(); i++)
diff --git a/src/prop/bvminisat/simp/SimpSolver.h b/src/prop/bvminisat/simp/SimpSolver.h
index e3ef76212..378812e03 100644
--- a/src/prop/bvminisat/simp/SimpSolver.h
+++ b/src/prop/bvminisat/simp/SimpSolver.h
@@ -184,9 +184,9 @@ inline bool SimpSolver::addClause    (Lit p, Lit q, Lit r)   { add_tmp.clear();
 inline void SimpSolver::setFrozen    (Var v, bool b) { frozen[v] = (char)b; if (use_simplification && !b) { updateElimHeap(v); } }
 
 inline bool SimpSolver::solve        (                     bool do_simp, bool turn_off_simp)  { budgetOff(); return solve_(do_simp, turn_off_simp) == l_True; }
-inline bool SimpSolver::solve        (Lit p       ,        bool do_simp, bool turn_off_simp)  { budgetOff(); assumptions.clear(); assumptions.push(p); return solve_(do_simp, turn_off_simp) == l_True; }
-inline bool SimpSolver::solve        (Lit p, Lit q,        bool do_simp, bool turn_off_simp)  { budgetOff(); assumptions.clear(); assumptions.push(p); assumptions.push(q); return solve_(do_simp, turn_off_simp) == l_True; }
-inline bool SimpSolver::solve        (Lit p, Lit q, Lit r, bool do_simp, bool turn_off_simp)  { budgetOff(); assumptions.clear(); assumptions.push(p); assumptions.push(q); assumptions.push(r); return solve_(do_simp, turn_off_simp) == l_True; }
+inline bool SimpSolver::solve        (Lit p       ,        bool do_simp, bool turn_off_simp)  { budgetOff(); assumptions.push(p); return solve_(do_simp, turn_off_simp) == l_True; }
+inline bool SimpSolver::solve        (Lit p, Lit q,        bool do_simp, bool turn_off_simp)  { budgetOff(); assumptions.push(p); assumptions.push(q); return solve_(do_simp, turn_off_simp) == l_True; }
+inline bool SimpSolver::solve        (Lit p, Lit q, Lit r, bool do_simp, bool turn_off_simp)  { budgetOff(); assumptions.push(p); assumptions.push(q); assumptions.push(r); return solve_(do_simp, turn_off_simp) == l_True; }
 inline bool SimpSolver::solve        (const vec<Lit>& assumps, bool do_simp, bool turn_off_simp){
   budgetOff(); assumps.copyTo(assumptions);
   return solve_(do_simp, turn_off_simp) == l_True;
diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc
index 79893a087..ea6cafdcd 100644
--- a/src/prop/minisat/core/Solver.cc
+++ b/src/prop/minisat/core/Solver.cc
@@ -657,6 +657,7 @@ CRef Solver::propagate(TheoryCheckType type)
 {
     CRef confl = CRef_Undef;
     recheck = false;
+    theoryConflict = false;
 
     ScopedBool scoped_bool(minisat_busy, true);
 
@@ -694,7 +695,11 @@ CRef Solver::propagate(TheoryCheckType type)
         // If no conflict, do the theory check
         if (confl == CRef_Undef && type != CHECK_WITHOUTH_THEORY) {
             // Do the theory check
-            theoryCheck(CVC4::theory::Theory::EFFORT_STANDARD);
+            if (type == CHECK_FINAL_FAKE) {
+              theoryCheck(CVC4::theory::Theory::EFFORT_FULL);
+            } else {
+              theoryCheck(CVC4::theory::Theory::EFFORT_STANDARD);
+            }
             // Pick up the theory propagated literals
             propagateTheory();
             // If there are lemmas (or conflicts) update them
@@ -1018,8 +1023,12 @@ lbool Solver::search(int nof_conflicts)
                            (int)max_learnts, nLearnts(), (double)learnts_literals/nLearnts(), progressEstimate()*100);
             }
 
-             // We have a conflict so, we are going back to standard checks
-            check_type = CHECK_WITH_THEORY;
+            if (theoryConflict && Options::current()->sat_refine_conflicts) {
+              check_type = CHECK_FINAL_FAKE;
+            } else {
+              check_type = CHECK_WITH_THEORY;
+            }
+
         } else {
 
 	    // If this was a final check, we are satisfiable
@@ -1043,6 +1052,8 @@ lbool Solver::search(int nof_conflicts)
 		}
                 return l_True;
               }
+            } else if (check_type == CHECK_FINAL_FAKE) {
+              check_type = CHECK_WITH_THEORY;
             }
 
             if (nof_conflicts >= 0 && conflictC >= nof_conflicts || !withinBudget()) {
@@ -1503,14 +1514,6 @@ CRef Solver::updateLemmas() {
             conflict = CRef_Lazy;
           }
         } else {
-//          if (Debug.isOn("minisat::lemmas")) {
-//          	Debug("minisat::lemmas") << "Solver::updateLemmas(): " << lemma[0] << " from ";
-//          	Clause& c = ca[lemma_ref];
-//          	for (int i = 0; i < c.size(); ++ i) {
-//          	   Debug("minisat::lemmas") << c[i] << "(" << value(c[i]) << "," << level(var(c[i])) << "," << trail_index(var(c[i])) << ") "; 
-//          	} 
-//			Debug("minisat::lemmas") << std::endl; 
-//          }
           Debug("minisat::lemmas") << "lemma size is " << lemma.size() << std::endl;
           uncheckedEnqueue(lemma[0], lemma_ref);
           if(lemma.size() == 1 && assertionLevel > 0) {
@@ -1528,5 +1531,9 @@ CRef Solver::updateLemmas() {
   lemmas.clear();
   lemmas_removable.clear();
 
+  if (conflict != CRef_Undef) {
+    theoryConflict = true;
+  }
+
   return conflict;
 }
diff --git a/src/prop/minisat/core/Solver.h b/src/prop/minisat/core/Solver.h
index ca5b2c30f..cfeb06211 100644
--- a/src/prop/minisat/core/Solver.h
+++ b/src/prop/minisat/core/Solver.h
@@ -308,7 +308,9 @@ protected:
       // Check and perform theory reasoning
       CHECK_WITH_THEORY,
       // The SAT abstraction of the problem is satisfiable, perform a full theory check
-      CHECK_FINAL
+      CHECK_FINAL,
+      // Perform a full theory check even if not done with everything
+      CHECK_FINAL_FAKE
     };
 
     // Temporaries (to reduce allocation overhead). Each variable is prefixed by the method in which it is
@@ -336,6 +338,7 @@ protected:
     void     newDecisionLevel ();                                                      // Begins a new decision level.
     void     uncheckedEnqueue (Lit p, CRef from = CRef_Undef);                         // Enqueue a literal. Assumes value of literal is undefined.
     bool     enqueue          (Lit p, CRef from = CRef_Undef);                         // Test if fact 'p' contradicts current state, enqueue otherwise.
+    bool     theoryConflict;                                                           // Was the last conflict a theory conflict
     CRef     propagate        (TheoryCheckType type);                                  // Perform Boolean and Theory. Returns possibly conflicting clause.
     CRef     propagateBool    ();                                                      // Perform Boolean propagation. Returns possibly conflicting clause.
     void     propagateTheory  ();                                                      // Perform Theory propagation.
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;