diff options
Diffstat (limited to 'src/prop/bvminisat/core/Solver.h')
-rw-r--r-- | src/prop/bvminisat/core/Solver.h | 16 |
1 files changed, 8 insertions, 8 deletions
diff --git a/src/prop/bvminisat/core/Solver.h b/src/prop/bvminisat/core/Solver.h index 2197d030f..7324666a1 100644 --- a/src/prop/bvminisat/core/Solver.h +++ b/src/prop/bvminisat/core/Solver.h @@ -365,11 +365,11 @@ public: // Less than for literals in an added clause when proofs are on. struct assign_lt { - Solver& solver; - assign_lt(Solver& solver) : solver(solver) {} + Solver& d_solver; + assign_lt(Solver& solver) : d_solver(solver) {} bool operator () (Lit x, Lit y) { - lbool x_value = solver.value(x); - lbool y_value = solver.value(y); + lbool x_value = d_solver.value(x); + lbool y_value = d_solver.value(y); // Two unassigned literals are sorted arbitrarily if (x_value == l_Undef && y_value == l_Undef) { return x < y; @@ -379,7 +379,7 @@ public: if (y_value == l_Undef) return false; // Literals of the same value are sorted by decreasing levels if (x_value == y_value) { - return solver.level(var(x)) > solver.level(var(y)); + return d_solver.level(var(x)) > d_solver.level(var(y)); } else { // True literals go up front if (x_value == l_True) { @@ -417,8 +417,8 @@ inline void Solver::varBumpActivity(Var v, double inc) { order_heap.decrease(v); } inline void Solver::claDecayActivity() { cla_inc *= (1 / clause_decay); } -inline void Solver::claBumpActivity (Clause& c) { - if ( (c.activity() += cla_inc) > 1e20 ) { +inline void Solver::claBumpActivity (Clause& clause) { + if ( (clause.activity() += cla_inc) > 1e20 ) { // Rescale: for (int i = 0; i < learnts.size(); i++) ca[learnts[i]].activity() *= 1e-20; @@ -436,7 +436,7 @@ inline bool Solver::addEmptyClause () { add_tmp.clear( inline bool Solver::addClause (Lit p, ClauseId& id) { add_tmp.clear(); add_tmp.push(p); return addClause_(add_tmp, id); } inline bool Solver::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 Solver::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 bool Solver::locked (const Clause& c) const { return value(c[0]) == l_True && reason(var(c[0])) != CRef_Undef && ca.lea(reason(var(c[0]))) == &c; } +inline bool Solver::locked (const Clause& clause) const { return value(clause[0]) == l_True && reason(var(clause[0])) != CRef_Undef && ca.lea(reason(var(clause[0]))) == &clause; } inline void Solver::newDecisionLevel() { trail_lim.push(trail.size()); } inline int Solver::decisionLevel () const { return trail_lim.size(); } |