From d41c0aa8c7ec8d14ce07f5817da38895598e55da Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Mon, 1 Oct 2018 11:36:45 -0700 Subject: [PATCH] Fix compiler warnings. (#2555) --- src/prop/bvminisat/core/Solver.cc | 28 +++++++++------ src/prop/bvminisat/simp/SimpSolver.cc | 52 ++++++++++++++++----------- src/prop/minisat/core/Solver.cc | 19 +++++----- src/prop/minisat/simp/SimpSolver.cc | 52 ++++++++++++++++----------- src/theory/arith/constraint.cpp | 5 ++- 5 files changed, 93 insertions(+), 63 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& 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; diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc index dbe417dbc..c8a2e16c2 100644 --- a/src/prop/minisat/core/Solver.cc +++ b/src/prop/minisat/core/Solver.cc @@ -1349,15 +1349,16 @@ lbool Solver::search(int nof_conflicts) check_type = CHECK_WITH_THEORY; } - if (nof_conflicts >= 0 && conflictC >= nof_conflicts || - !withinBudget(options::satConflictStep())) { - // Reached bound on number of conflicts: - progress_estimate = progressEstimate(); - cancelUntil(0); - // [mdeters] notify theory engine of restarts for deferred - // theory processing - proxy->notifyRestart(); - return l_Undef; + if ((nof_conflicts >= 0 && conflictC >= nof_conflicts) + || !withinBudget(options::satConflictStep())) + { + // Reached bound on number of conflicts: + progress_estimate = progressEstimate(); + cancelUntil(0); + // [mdeters] notify theory engine of restarts for deferred + // theory processing + proxy->notifyRestart(); + return l_Undef; } // Simplify the set of problem clauses: diff --git a/src/prop/minisat/simp/SimpSolver.cc b/src/prop/minisat/simp/SimpSolver.cc index 96fea2147..a101a0c2d 100644 --- a/src/prop/minisat/simp/SimpSolver.cc +++ b/src/prop/minisat/simp/SimpSolver.cc @@ -256,17 +256,23 @@ bool SimpSolver::merge(const Clause& _ps, const Clause& _qs, Var v, vec& 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++) @@ -290,17 +296,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; diff --git a/src/theory/arith/constraint.cpp b/src/theory/arith/constraint.cpp index f5c3eac08..ff71f6432 100644 --- a/src/theory/arith/constraint.cpp +++ b/src/theory/arith/constraint.cpp @@ -711,9 +711,8 @@ bool Constraint::wellFormedFarkasProof() const { } Debug("constraints::wffp") << "final sum: " << lhs << " <= " << rhs << endl; // 0 = lhs <= rhs < 0 - return - (lhs.isNull() || Constant::isMember(lhs) && Constant(lhs).isZero() ) && - rhs.sgn() < 0; + return (lhs.isNull() || (Constant::isMember(lhs) && Constant(lhs).isZero())) + && rhs.sgn() < 0; #else /* IS_PROOFS_BUILD */ return true; -- 2.30.2