new implementation of lemmas on demand

comparison <http://goedel.cims.nyu.edu/regress-results/compare_jobs.php?job_id=2673&&p=5&reference_id=2637>

2 files changed, 27 insertions, 23 deletions

diff --git a/src/prop/minisat/simp/SimpSolver.cc b/src/prop/minisat/simp/SimpSolver.cc
index 8bcd9fe76..271aabb52 100644
--- a/src/prop/minisat/simp/SimpSolver.cc
+++ b/src/prop/minisat/simp/SimpSolver.cc
@@ -134,23 +134,23 @@ lbool SimpSolver::solve_(bool do_simp, bool turn_off_simp)
 
 
 
-bool SimpSolver::addClause_(vec<Lit>& ps, ClauseType type)
+bool SimpSolver::addClause_(vec<Lit>& ps, bool removable)
 {
 #ifndef NDEBUG
     for (int i = 0; i < ps.size(); i++)
         assert(!isEliminated(var(ps[i])));
 #endif
 
-    int nclauses = clauses.size();
+    int nclauses = clauses_persistent.size();
 
     if (use_rcheck && implied(ps))
         return true;
 
-    if (!Solver::addClause_(ps, type))
+    if (!Solver::addClause_(ps, removable))
         return false;
 
-    if (use_simplification && clauses.size() == nclauses + 1){
-        CRef          cr = clauses.last();
+    if (use_simplification && clauses_persistent.size() == nclauses + 1){
+        CRef          cr = clauses_persistent.last();
         const Clause& c  = ca[cr];
 
         // NOTE: the clause is added to the queue immediately and then
@@ -516,9 +516,12 @@ bool SimpSolver::eliminateVar(Var v)
     // Produce clauses in cross product:
     vec<Lit>& resolvent = add_tmp;
     for (int i = 0; i < pos.size(); i++)
-        for (int j = 0; j < neg.size(); j++)
-            if (merge(ca[pos[i]], ca[neg[j]], v, resolvent) && !addClause_(resolvent, CLAUSE_CONFLICT))
+        for (int j = 0; j < neg.size(); j++) {
+            bool removable = ca[pos[i]].removable() && ca[pos[neg[j]]].removable();
+            if (merge(ca[pos[i]], ca[neg[j]], v, resolvent) && !addClause_(resolvent, removable)) {
                 return false;
+            }
+        }
 
     // Free occurs list for this variable:
     occurs[v].clear(true);
@@ -555,8 +558,9 @@ bool SimpSolver::substitute(Var v, Lit x)
 
         removeClause(cls[i]);
 
-        if (!addClause_(subst_clause, CLAUSE_PROBLEM))
+        if (!addClause_(subst_clause, c.removable())) {
             return ok = false;
+        }
     }
 
     return true;
@@ -669,10 +673,10 @@ void SimpSolver::cleanUpClauses()
 {
     occurs.cleanAll();
     int i,j;
-    for (i = j = 0; i < clauses.size(); i++)
-        if (ca[clauses[i]].mark() == 0)
-            clauses[j++] = clauses[i];
-    clauses.shrink(i - j);
+    for (i = j = 0; i < clauses_persistent.size(); i++)
+        if (ca[clauses_persistent[i]].mark() == 0)
+            clauses_persistent[j++] = clauses_persistent[i];
+    clauses_persistent.shrink(i - j);
 }
 
 
diff --git a/src/prop/minisat/simp/SimpSolver.h b/src/prop/minisat/simp/SimpSolver.h
index a7359e28e..9b5e5d45c 100644
--- a/src/prop/minisat/simp/SimpSolver.h
+++ b/src/prop/minisat/simp/SimpSolver.h
@@ -47,12 +47,12 @@ class SimpSolver : public Solver {
     // Problem specification:
     //
     Var     newVar    (bool polarity = true, bool dvar = true, bool theoryAtom = false);
-    bool    addClause (const vec<Lit>& ps, ClauseType type);
-    bool    addEmptyClause(ClauseType type);                  // Add the empty clause to the solver.
-    bool    addClause (Lit p, ClauseType type);               // Add a unit clause to the solver.
-    bool    addClause (Lit p, Lit q, ClauseType type);        // Add a binary clause to the solver.
-    bool    addClause (Lit p, Lit q, Lit r, ClauseType type); // Add a ternary clause to the solver.
-    bool    addClause_(vec<Lit>& ps, ClauseType type);
+    bool    addClause (const vec<Lit>& ps, bool removable);
+    bool    addEmptyClause(bool removable);                  // Add the empty clause to the solver.
+    bool    addClause (Lit p, bool removable);               // Add a unit clause to the solver.
+    bool    addClause (Lit p, Lit q, bool removable);        // Add a binary clause to the solver.
+    bool    addClause (Lit p, Lit q, Lit r, bool removable); // Add a ternary clause to the solver.
+    bool    addClause_(vec<Lit>& ps, bool removable);
     bool    substitute(Var v, Lit x);  // Replace all occurences of v with x (may cause a contradiction).
 
     // Variable mode:
@@ -181,11 +181,11 @@ inline void SimpSolver::updateElimHeap(Var v) {
         elim_heap.update(v); }
 
 
-inline bool SimpSolver::addClause    (const vec<Lit>& ps, ClauseType type)    { ps.copyTo(add_tmp); return addClause_(add_tmp, type); }
-inline bool SimpSolver::addEmptyClause(ClauseType type)                       { add_tmp.clear(); return addClause_(add_tmp, type); }
-inline bool SimpSolver::addClause    (Lit p, ClauseType type)                 { add_tmp.clear(); add_tmp.push(p); return addClause_(add_tmp, type); }
-inline bool SimpSolver::addClause    (Lit p, Lit q, ClauseType type)          { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); return addClause_(add_tmp, type); }
-inline bool SimpSolver::addClause    (Lit p, Lit q, Lit r, ClauseType type)   { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); add_tmp.push(r); return addClause_(add_tmp, type); }
+inline bool SimpSolver::addClause    (const vec<Lit>& ps, bool removable)    { ps.copyTo(add_tmp); return addClause_(add_tmp, removable); }
+inline bool SimpSolver::addEmptyClause(bool removable)                       { add_tmp.clear(); return addClause_(add_tmp, removable); }
+inline bool SimpSolver::addClause    (Lit p, bool removable)                 { add_tmp.clear(); add_tmp.push(p); return addClause_(add_tmp, removable); }
+inline bool SimpSolver::addClause    (Lit p, Lit q, bool removable)          { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); return addClause_(add_tmp, removable); }
+inline bool SimpSolver::addClause    (Lit p, Lit q, Lit r, bool removable)   { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); add_tmp.push(r); return addClause_(add_tmp, removable); }
 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(); assumptions.clear(); return solve_(do_simp, turn_off_simp) == l_True; }