diff options
Diffstat (limited to 'src/prop/bvminisat/simp')
-rw-r--r-- | src/prop/bvminisat/simp/SimpSolver.cc | 20 | ||||
-rw-r--r-- | src/prop/bvminisat/simp/SimpSolver.h | 20 |
2 files changed, 22 insertions, 18 deletions
diff --git a/src/prop/bvminisat/simp/SimpSolver.cc b/src/prop/bvminisat/simp/SimpSolver.cc index c5b185c95..311ed1dd1 100644 --- a/src/prop/bvminisat/simp/SimpSolver.cc +++ b/src/prop/bvminisat/simp/SimpSolver.cc @@ -24,6 +24,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include "options/bv_options.h" #include "options/smt_options.h" #include "utils/System.h" +#include "proof/proof.h" namespace CVC4 { namespace BVMinisat { @@ -62,7 +63,7 @@ SimpSolver::SimpSolver(CVC4::context::Context* c) : , asymm_lits (0) , eliminated_vars (0) , elimorder (1) - , use_simplification (true) + , use_simplification (!PROOF_ON()) , occurs (ClauseDeleted(ca)) , elim_heap (ElimLt(n_occ)) , bwdsub_assigns (0) @@ -162,7 +163,7 @@ lbool SimpSolver::solve_(bool do_simp, bool turn_off_simp) -bool SimpSolver::addClause_(vec<Lit>& ps) +bool SimpSolver::addClause_(vec<Lit>& ps, ClauseId& id) { #ifndef NDEBUG for (int i = 0; i < ps.size(); i++) @@ -174,7 +175,7 @@ bool SimpSolver::addClause_(vec<Lit>& ps) if (use_rcheck && implied(ps)) return true; - if (!Solver::addClause_(ps)) + if (!Solver::addClause_(ps, id)) return false; if (use_simplification && clauses.size() == nclauses + 1){ @@ -544,9 +545,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)) - return false; + for (int j = 0; j < neg.size(); j++) { + ClauseId id = -1; + if (merge(ca[pos[i]], ca[neg[j]], v, resolvent) && + !addClause_(resolvent, id)) + return false; + } // Free occurs list for this variable: occurs[v].clear(true); @@ -582,8 +586,8 @@ bool SimpSolver::substitute(Var v, Lit x) } removeClause(cls[i]); - - if (!addClause_(subst_clause)) + ClauseId id; + if (!addClause_(subst_clause, id)) return ok = false; } diff --git a/src/prop/bvminisat/simp/SimpSolver.h b/src/prop/bvminisat/simp/SimpSolver.h index 85556e935..5f6f46b91 100644 --- a/src/prop/bvminisat/simp/SimpSolver.h +++ b/src/prop/bvminisat/simp/SimpSolver.h @@ -42,12 +42,12 @@ class SimpSolver : public Solver { // Problem specification: // Var newVar (bool polarity = true, bool dvar = true, bool freeze = false); - bool addClause (const vec<Lit>& ps); + bool addClause (const vec<Lit>& ps, ClauseId& id); bool addEmptyClause(); // Add the empty clause to the solver. - bool addClause (Lit p); // Add a unit clause to the solver. - bool addClause (Lit p, Lit q); // Add a binary clause to the solver. - bool addClause (Lit p, Lit q, Lit r); // Add a ternary clause to the solver. - bool addClause_( vec<Lit>& ps); + bool addClause (Lit p, ClauseId& id); // Add a unit clause to the solver. + bool addClause (Lit p, Lit q, ClauseId& id); // Add a binary clause to the solver. + bool addClause (Lit p, Lit q, Lit r, ClauseId& id); // Add a ternary clause to the solver. + bool addClause_( vec<Lit>& ps, ClauseId& id); bool substitute(Var v, Lit x); // Replace all occurences of v with x (may cause a contradiction). // Variable mode: @@ -178,11 +178,11 @@ inline void SimpSolver::updateElimHeap(Var v) { elim_heap.update(v); } -inline bool SimpSolver::addClause (const vec<Lit>& ps) { ps.copyTo(add_tmp); return addClause_(add_tmp); } -inline bool SimpSolver::addEmptyClause() { add_tmp.clear(); return addClause_(add_tmp); } -inline bool SimpSolver::addClause (Lit p) { add_tmp.clear(); add_tmp.push(p); return addClause_(add_tmp); } -inline bool SimpSolver::addClause (Lit p, Lit q) { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); return addClause_(add_tmp); } -inline bool SimpSolver::addClause (Lit p, Lit q, Lit r) { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); add_tmp.push(r); return addClause_(add_tmp); } +inline bool SimpSolver::addClause (const vec<Lit>& ps, ClauseId& id) { ps.copyTo(add_tmp); return addClause_(add_tmp, id); } +inline bool SimpSolver::addEmptyClause() { add_tmp.clear(); ClauseId id; return addClause_(add_tmp, id); } +inline bool SimpSolver::addClause (Lit p, ClauseId& id) { add_tmp.clear(); add_tmp.push(p); return addClause_(add_tmp, id); } +inline bool SimpSolver::addClause (Lit p, Lit q, ClauseId& id) { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); return addClause_(add_tmp, id); } +inline bool SimpSolver::addClause (Lit p, Lit q, Lit r, ClauseId& id) { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); add_tmp.push(r); return addClause_(add_tmp, id); } inline void SimpSolver::setFrozen (Var v, bool b) { frozen[v] = (char)b; if (use_simplification && !b) { updateElimHeap(v); } } inline lbool SimpSolver::solve ( bool do_simp, bool turn_off_simp) { |