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/minisat | |
parent | da3b2212ed6befc0d29646ef65570919377913fe (diff) |
Fix compiler warnings. (#2555)
Diffstat (limited to 'src/prop/minisat')
-rw-r--r-- | src/prop/minisat/core/Solver.cc | 19 | ||||
-rw-r--r-- | src/prop/minisat/simp/SimpSolver.cc | 52 |
2 files changed, 42 insertions, 29 deletions
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<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++) @@ -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; |