user push/pop support in minisat and simplification; also bindings work

3 files changed, 59 insertions, 13 deletions

diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc
index 7b5ba9286..c1795a12c 100644
--- a/src/prop/minisat/core/Solver.cc
+++ b/src/prop/minisat/core/Solver.cc
@@ -221,7 +221,6 @@ bool Solver::addClause_(vec<Lit>& ps, bool removable)
     // Fit to size
     ps.shrink(i - j);
 
-
     // If we are in solve or decision level > 0
     if (minisat_busy || decisionLevel() > 0) {
       lemmas.push();
@@ -232,8 +231,15 @@ bool Solver::addClause_(vec<Lit>& ps, bool removable)
       if (ps.size() == 0) {
           return ok = false;
       } else if (ps.size() == 1) {
-        uncheckedEnqueue(ps[0]);
-        return ok = (propagate(CHECK_WITHOUTH_PROPAGATION_QUICK) == CRef_Undef);
+        if(assigns[var(ps[0])] == l_Undef) {
+          uncheckedEnqueue(ps[0]);
+          if(assertionLevel > 0) {
+            // remember to unset it on user pop
+            Debug("minisat") << "got new unit " << ps[0] << " at assertion level " << assertionLevel << std::endl;
+            trail_user.push(ps[0]);
+          }
+          return ok = (propagate(CHECK_WITHOUTH_PROPAGATION_QUICK) == CRef_Undef);
+        } else return ok;
       } else {
         CRef cr = ca.alloc(assertionLevel, ps, false);
         clauses_persistent.push(cr);
@@ -307,10 +313,13 @@ void Solver::cancelUntil(int level) {
         }
         for (int c = trail.size()-1; c >= trail_lim[level]; c--){
             Var      x  = var(trail[c]);
-            assigns [x] = l_Undef;
-            if (phase_saving > 1 || (phase_saving == 1) && c > trail_lim.last())
+            if(intro_level(x) != -1) {// might be unregistered
+              assigns [x] = l_Undef;
+              vardata[x].trail_index = -1;
+              if (phase_saving > 1 || (phase_saving == 1) && c > trail_lim.last())
                 polarity[x] = sign(trail[c]);
-            insertVarOrder(x);
+              insertVarOrder(x);
+            }
         }
         qhead = trail_lim[level];
         trail.shrink(trail.size() - trail_lim[level]);
@@ -581,8 +590,16 @@ void Solver::uncheckedEnqueue(Lit p, CRef from)
     Debug("minisat") << "unchecked enqueue of " << p << " (" << trail_index(var(p)) << ") trail size is " << trail.size() << " cap is " << trail.capacity() << std::endl;
     assert(value(p) == l_Undef);
     assigns[var(p)] = lbool(!sign(p));
-    vardata[var(p)] = mkVarData(from, decisionLevel(), intro_level(var(p)), trail.size());
-    trail.push_(p);
+    if(trail_index(var(p)) != -1) {
+      // This var is already represented in the trail, presumably from
+      // an earlier incarnation as a unit clause (it has been
+      // unregistered and renewed since then)
+      vardata[var(p)] = mkVarData(from, decisionLevel(), intro_level(var(p)), trail_index(var(p)));
+      trail[trail_index(var(p))] = p;
+    } else {
+      vardata[var(p)] = mkVarData(from, decisionLevel(), intro_level(var(p)), trail.size());
+      trail.push_(p);
+    }
     if (theory[var(p)]) {
       // Enqueue to the theory
       proxy->enqueueTheoryLiteral(p);
@@ -1050,6 +1067,8 @@ lbool Solver::solve_()
 
     ScopedBool scoped_bool(minisat_busy, true);
 
+    popTrail();
+
     model.clear();
     conflict.clear();
     if (!ok){
@@ -1231,14 +1250,19 @@ void Solver::push()
 {
   assert(enable_incremental);
 
-  Debug("minisat") << "in user push, increasing assertion level to " << assertionLevel << std::endl;
+  popTrail();
   ++assertionLevel;
+  Debug("minisat") << "in user push, increasing assertion level to " << assertionLevel << std::endl;
+  trail_user.push(lit_Undef);
+  trail_ok.push(ok);
 }
 
 void Solver::pop()
 {
   assert(enable_incremental);
 
+  popTrail();
+
   --assertionLevel;
 
   Debug("minisat") << "in user pop, reducing assertion level to " << assertionLevel << " and removing clauses above this from db" << std::endl;
@@ -1247,8 +1271,26 @@ void Solver::pop()
   removeClausesAboveLevel(clauses_removable, assertionLevel);
   removeClausesAboveLevel(clauses_persistent, assertionLevel);
 
-  // Pop the user trail size
-  popTrail();
+  Debug("minisat") << "in user pop, at " << trail_lim.size() << " : " << assertionLevel << std::endl;
+
+  // Unset any units learned or added at this level
+  Debug("minisat") << "in user pop, unsetting level units for level " << assertionLevel << std::endl;
+  while(trail_user.last() != lit_Undef) {
+    Lit l = trail_user.last();
+    Debug("minisat") << "== unassigning " << l << std::endl;
+    Var      x  = var(l);
+    assigns [x] = l_Undef;
+    if (phase_saving >= 1)
+      polarity[x] = sign(l);
+    insertVarOrder(x);
+    trail_user.pop();
+  }
+  trail_user.pop();
+  ok = trail_ok.last();
+  trail_ok.pop();
+  Debug("minisat") << "in user pop, done unsetting level units" << std::endl;
+
+  Debug("minisat") << "about to removeClausesAboveLevel(" << assertionLevel << ") in CNF" << std::endl;
 
   // Notify the cnf
   proxy->removeClausesAboveLevel(assertionLevel);
@@ -1357,9 +1399,11 @@ CRef Solver::updateLemmas() {
 //          }
           Debug("minisat::lemmas") << "lemma size is " << lemma.size() << std::endl;
           uncheckedEnqueue(lemma[0], lemma_ref);
-          if(assertionLevel > 0) {
+          if(lemma.size() == 1 && assertionLevel > 0) {
+            assert(decisionLevel() == 0);
             // remember to unset it on user pop
             Debug("minisat") << "got new unit (survived downward during updateLemmas()) " << lemma[0] << " at assertion level " << assertionLevel << std::endl;
+            trail_user.push(lemma[0]);
           }
         }
       }
diff --git a/src/prop/minisat/core/Solver.h b/src/prop/minisat/core/Solver.h
index 345a00e52..c5220997b 100644
--- a/src/prop/minisat/core/Solver.h
+++ b/src/prop/minisat/core/Solver.h
@@ -278,6 +278,8 @@ protected:
     vec<char>           decision;           // Declares if a variable is eligible for selection in the decision heuristic.
     vec<Lit>            trail;              // Assignment stack; stores all assigments made in the order they were made.
     vec<int>            trail_lim;          // Separator indices for different decision levels in 'trail'.
+    vec<Lit>            trail_user;         // Stack of assignments to UNdo on user pop.
+    vec<bool>           trail_ok;           // Stack of "whether we're in conflict" flags.
     vec<VarData>        vardata;            // Stores reason and level for each variable.
     int                 qhead;              // Head of queue (as index into the trail -- no more explicit propagation queue in MiniSat).
     int                 simpDB_assigns;     // Number of top-level assignments since last execution of 'simplify()'.
diff --git a/src/prop/minisat/simp/SimpSolver.cc b/src/prop/minisat/simp/SimpSolver.cc
index f8292c072..8c31dd377 100644
--- a/src/prop/minisat/simp/SimpSolver.cc
+++ b/src/prop/minisat/simp/SimpSolver.cc
@@ -57,7 +57,7 @@ SimpSolver::SimpSolver(CVC4::prop::SatSolver* proxy, CVC4::context::Context* con
   , asymm_lits         (0)
   , eliminated_vars    (0)
   , elimorder          (1)
-  , use_simplification (true)
+  , use_simplification (!enableIncremental)
   , occurs             (ClauseDeleted(ca))
   , elim_heap          (ElimLt(n_occ))
   , bwdsub_assigns     (0)