diff options
author | Aina Niemetz <aina.niemetz@gmail.com> | 2018-10-01 11:36:45 -0700 |
---|---|---|
committer | Andres Noetzli <andres.noetzli@gmail.com> | 2018-10-01 11:36:45 -0700 |
commit | d41c0aa8c7ec8d14ce07f5817da38895598e55da (patch) | |
tree | 81d1767b4e2384df9d9a4fa90ed868d9419f9693 /src/prop/bvminisat | |
parent | da3b2212ed6befc0d29646ef65570919377913fe (diff) |
Fix compiler warnings. (#2555)
Diffstat (limited to 'src/prop/bvminisat')
-rw-r--r-- | src/prop/bvminisat/core/Solver.cc | 28 | ||||
-rw-r--r-- | src/prop/bvminisat/simp/SimpSolver.cc | 52 |
2 files changed, 49 insertions, 31 deletions
diff --git a/src/prop/bvminisat/core/Solver.cc b/src/prop/bvminisat/core/Solver.cc index 372f8eb04..a4b0248e0 100644 --- a/src/prop/bvminisat/core/Solver.cc +++ b/src/prop/bvminisat/core/Solver.cc @@ -357,8 +357,11 @@ void Solver::cancelUntil(int level) { Var x = var(trail[c]); assigns [x] = l_Undef; if (marker[x] == 2) marker[x] = 1; - if (phase_saving > 1 || (phase_saving == 1) && c > trail_lim.last()) - polarity[x] = sign(trail[c]); + if (phase_saving > 1 + || ((phase_saving == 1) && c > trail_lim.last())) + { + polarity[x] = sign(trail[c]); + } insertVarOrder(x); } qhead = trail_lim[level]; trail.shrink(trail.size() - trail_lim[level]); @@ -1080,16 +1083,19 @@ lbool Solver::search(int nof_conflicts, UIP uip) cancelUntil(assumptions.size()); throw e; } - - if (decisionLevel() > assumptions.size() && nof_conflicts >= 0 && conflictC >= nof_conflicts || - !isWithinBudget) { - // Reached bound on number of conflicts: - Debug("bvminisat::search") << OUTPUT_TAG << " restarting " << std::endl; - progress_estimate = progressEstimate(); - cancelUntil(assumptions.size()); - return l_Undef; + + if ((decisionLevel() > assumptions.size() && nof_conflicts >= 0 + && conflictC >= nof_conflicts) + || !isWithinBudget) + { + // Reached bound on number of conflicts: + Debug("bvminisat::search") + << OUTPUT_TAG << " restarting " << std::endl; + progress_estimate = progressEstimate(); + cancelUntil(assumptions.size()); + return l_Undef; } - + // Simplify the set of problem clauses: if (decisionLevel() == 0 && !simplify()) { Debug("bvminisat::search") << OUTPUT_TAG << " base level conflict, we're unsat" << std::endl; diff --git a/src/prop/bvminisat/simp/SimpSolver.cc b/src/prop/bvminisat/simp/SimpSolver.cc index 2fa8d472d..698d2a776 100644 --- a/src/prop/bvminisat/simp/SimpSolver.cc +++ b/src/prop/bvminisat/simp/SimpSolver.cc @@ -255,17 +255,23 @@ bool SimpSolver::merge(const Clause& _ps, const Clause& _qs, Var v, vec<Lit>& ou const Clause& ps = ps_smallest ? _qs : _ps; const Clause& qs = ps_smallest ? _ps : _qs; - for (int i = 0; i < qs.size(); i++){ - if (var(qs[i]) != v){ - for (int j = 0; j < ps.size(); j++) - if (var(ps[j]) == var(qs[i])) - if (ps[j] == ~qs[i]) - return false; - else - goto next; - out_clause.push(qs[i]); + for (int i = 0; i < qs.size(); i++) + { + if (var(qs[i]) != v) + { + for (int j = 0; j < ps.size(); j++) + { + if (var(ps[j]) == var(qs[i])) + { + if (ps[j] == ~qs[i]) + return false; + else + goto next; + } } - next:; + out_clause.push(qs[i]); + } + next:; } for (int i = 0; i < ps.size(); i++) @@ -289,17 +295,23 @@ bool SimpSolver::merge(const Clause& _ps, const Clause& _qs, Var v, int& size) size = ps.size()-1; - for (int i = 0; i < qs.size(); i++){ - if (var(__qs[i]) != v){ - for (int j = 0; j < ps.size(); j++) - if (var(__ps[j]) == var(__qs[i])) - if (__ps[j] == ~__qs[i]) - return false; - else - goto next; - size++; + for (int i = 0; i < qs.size(); i++) + { + if (var(__qs[i]) != v) + { + for (int j = 0; j < ps.size(); j++) + { + if (var(__ps[j]) == var(__qs[i])) + { + if (__ps[j] == ~__qs[i]) + return false; + else + goto next; + } } - next:; + size++; + } + next:; } return true; |