Unsat core infrastruture and API (SMT-LIB compliance to come).

1 files changed, 15 insertions, 11 deletions

diff --git a/src/prop/minisat/simp/SimpSolver.h b/src/prop/minisat/simp/SimpSolver.h
index 878d799a5..041309546 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 isTheoryAtom = false, bool preRegister = false, bool canErase = true);
-    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    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    substitute(Var v, Lit x);  // Replace all occurences of v with x (may cause a contradiction).
 
     // Variable mode:
@@ -182,11 +182,15 @@ inline void SimpSolver::updateElimHeap(Var v) {
         elim_heap.update(v); }
 
 
-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 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 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; }