Merged bit-vector and uf proof branch.

2 files changed, 22 insertions, 20 deletions

diff --git a/src/prop/minisat/simp/SimpSolver.cc b/src/prop/minisat/simp/SimpSolver.cc
index 235c97e8f..5bdaea950 100644
--- a/src/prop/minisat/simp/SimpSolver.cc
+++ b/src/prop/minisat/simp/SimpSolver.cc
@@ -160,7 +160,7 @@ lbool SimpSolver::solve_(bool do_simp, bool turn_off_simp)
 
 
 
-bool SimpSolver::addClause_(vec<Lit>& ps, bool removable, uint64_t proof_id)
+bool SimpSolver::addClause_(vec<Lit>& ps, bool removable, ClauseId& id)
 {
 #ifndef NDEBUG
     if (use_simplification) {
@@ -174,7 +174,7 @@ bool SimpSolver::addClause_(vec<Lit>& ps, bool removable, uint64_t proof_id)
     if (use_rcheck && implied(ps))
         return true;
 
-    if (!Solver::addClause_(ps, removable, proof_id))
+    if (!Solver::addClause_(ps, removable, id))
         return false;
 
     if (use_simplification && clauses_persistent.size() == nclauses + 1){
@@ -541,12 +541,14 @@ bool SimpSolver::eliminateVar(Var v)
     for (int i = 0; i < cls.size(); i++)
         removeClause(cls[i]); 
 
+    ClauseId id = ClauseIdUndef; 
     // 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++) {
             bool removable = ca[pos[i]].removable() && ca[pos[neg[j]]].removable();
-            if (merge(ca[pos[i]], ca[neg[j]], v, resolvent) && !addClause_(resolvent, removable, uint64_t(-1))) {
+            if (merge(ca[pos[i]], ca[neg[j]], v, resolvent) &&
+                !addClause_(resolvent, removable, id)) {
                 return false;
             }
         }
@@ -585,8 +587,8 @@ bool SimpSolver::substitute(Var v, Lit x)
         }
 
         removeClause(cls[i]);
-
-        if (!addClause_(subst_clause, c.removable(), uint64_t(-1))) {
+        ClauseId id = ClauseIdUndef;
+        if (!addClause_(subst_clause, c.removable(), id)) {
             return ok = false;
         }
     }
diff --git a/src/prop/minisat/simp/SimpSolver.h b/src/prop/minisat/simp/SimpSolver.h
index 0c5062726..a19bec1ef 100644
--- a/src/prop/minisat/simp/SimpSolver.h
+++ b/src/prop/minisat/simp/SimpSolver.h
@@ -48,12 +48,12 @@ class SimpSolver : public Solver {
     // Problem specification:
     //
     Var     newVar    (bool polarity = true, bool dvar = true, bool isTheoryAtom = false, bool preRegister = false, bool canErase = true);
-    bool    addClause (const vec<Lit>& ps, bool removable, uint64_t proof_id);
-    bool    addEmptyClause(bool removable, uint64_t proof_id); // Add the empty clause to the solver.
-    bool    addClause (Lit p, bool removable, uint64_t proof_id); // Add a unit clause to the solver.
-    bool    addClause (Lit p, Lit q, bool removable, uint64_t proof_id); // Add a binary clause to the solver.
-    bool    addClause (Lit p, Lit q, Lit r, bool removable, uint64_t proof_id); // Add a ternary clause to the solver.
-    bool    addClause_(vec<Lit>& ps, bool removable, uint64_t proof_id);
+    bool    addClause (const vec<Lit>& ps, bool removable, ClauseId& id);
+    bool    addEmptyClause(bool removable); // Add the empty clause to the solver.
+    bool    addClause (Lit p, bool removable, ClauseId& id); // Add a unit clause to the solver.
+    bool    addClause (Lit p, Lit q, bool removable, ClauseId& id); // Add a binary clause to the solver.
+    bool    addClause (Lit p, Lit q, Lit r, bool removable, ClauseId& id); // Add a ternary clause to the solver.
+    bool    addClause_(vec<Lit>& ps, bool removable, ClauseId& id);
     bool    substitute(Var v, Lit x);  // Replace all occurences of v with x (may cause a contradiction).
 
     // Variable mode:
@@ -183,15 +183,15 @@ inline void SimpSolver::updateElimHeap(Var v) {
         elim_heap.update(v); }
 
 
-inline bool SimpSolver::addClause    (const vec<Lit>& ps, bool removable, uint64_t proof_id)
-                                                                             { ps.copyTo(add_tmp); return addClause_(add_tmp, removable, proof_id); }
-inline bool SimpSolver::addEmptyClause(bool removable, uint64_t proof_id)    { add_tmp.clear(); return addClause_(add_tmp, removable, proof_id); }
-inline bool SimpSolver::addClause    (Lit p, bool removable, uint64_t proof_id)
-                                                                             { add_tmp.clear(); add_tmp.push(p); return addClause_(add_tmp, removable, proof_id); }
-inline bool SimpSolver::addClause    (Lit p, Lit q, bool removable, uint64_t proof_id)
-                                                                             { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); return addClause_(add_tmp, removable, proof_id); }
-inline bool SimpSolver::addClause    (Lit p, Lit q, Lit r, bool removable, uint64_t proof_id)
-                                                                             { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); add_tmp.push(r); return addClause_(add_tmp, removable, proof_id); }
+inline bool SimpSolver::addClause(const vec<Lit>& ps, bool removable, ClauseId& id)
+{ ps.copyTo(add_tmp); return addClause_(add_tmp, removable, id); }
+inline bool SimpSolver::addEmptyClause(bool removable)    { add_tmp.clear(); ClauseId id=-1; return addClause_(add_tmp, removable, id); }
+inline bool SimpSolver::addClause    (Lit p, bool removable, ClauseId& id)
+                                                                             { add_tmp.clear(); add_tmp.push(p); return addClause_(add_tmp, removable, id); }
+inline bool SimpSolver::addClause    (Lit p, Lit q, bool removable, ClauseId& id)
+                                                                             { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); return addClause_(add_tmp, removable, id); }
+inline bool SimpSolver::addClause    (Lit p, Lit q, Lit r, bool removable, ClauseId& id)
+                                                                             { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); add_tmp.push(r); return addClause_(add_tmp, removable, id); }
 inline void SimpSolver::setFrozen    (Var v, bool b) { frozen[v] = (char)b; if (use_simplification && !b) { updateElimHeap(v); } }
 
 // the solver can always return unknown due to resource limiting