diff options
Diffstat (limited to 'src/prop/minisat/simp/SimpSolver.h')
| -rw-r--r-- | src/prop/minisat/simp/SimpSolver.h | 30 |
1 files changed, 15 insertions, 15 deletions
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 |