From d11e5c8ca68a3691088360a927c6bc3442892100 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 19 Jan 2023 19:02:43 -0800 Subject: [PATCH] address compiler warnings, and user question #6544 --- src/qe/lite/qe_lite.cpp | 6 +++--- src/sat/sat_drat.cpp | 2 +- src/sat/sat_integrity_checker.cpp | 2 +- src/sat/sat_local_search.cpp | 2 -- src/sat/sat_model_converter.cpp | 1 + src/sat/sat_simplifier.cpp | 3 --- src/sat/sat_solver.cpp | 5 +---- src/sat/sat_solver/sat_smt_solver.cpp | 2 +- src/sat/smt/arith_diagnostics.cpp | 2 -- src/sat/smt/pb_solver.cpp | 7 ------- src/sat/smt/q_eval.cpp | 2 -- src/sat/smt/q_mam.cpp | 2 -- src/sat/smt/tseitin_theory_checker.cpp | 2 +- src/tactic/core/cofactor_elim_term_ite.cpp | 8 ++------ src/tactic/fd_solver/smtfd_solver.cpp | 20 -------------------- src/tactic/smtlogics/qfnia_tactic.cpp | 2 -- 16 files changed, 11 insertions(+), 57 deletions(-) diff --git a/src/qe/lite/qe_lite.cpp b/src/qe/lite/qe_lite.cpp index 75c90ee4d..90ea35769 100644 --- a/src/qe/lite/qe_lite.cpp +++ b/src/qe/lite/qe_lite.cpp @@ -2165,7 +2165,6 @@ namespace fm { subsume(); var_vector candidates; sort_candidates(candidates); - unsigned eliminated = 0; unsigned num = candidates.size(); for (unsigned i = 0; i < num; i++) { @@ -2173,8 +2172,9 @@ namespace fm { if (m_counter > m_fm_limit) break; m_counter++; - if (try_eliminate(candidates[i])) - eliminated++; + if (try_eliminate(candidates[i])) { + + } if (m_inconsistent) { m_new_fmls.reset(); m_new_fmls.push_back(m.mk_false()); diff --git a/src/sat/sat_drat.cpp b/src/sat/sat_drat.cpp index 46a608151..836a76c96 100644 --- a/src/sat/sat_drat.cpp +++ b/src/sat/sat_drat.cpp @@ -372,7 +372,7 @@ namespace sat { } } CTRACE("sat_drat", num_true == 0 && num_undef == 1, display(tout);); - SASSERT(num_true != 0 || num_undef != 1); + VERIFY(num_true != 0 || num_undef != 1); } } } diff --git a/src/sat/sat_integrity_checker.cpp b/src/sat/sat_integrity_checker.cpp index 223e58677..031ce9202 100644 --- a/src/sat/sat_integrity_checker.cpp +++ b/src/sat/sat_integrity_checker.cpp @@ -105,7 +105,7 @@ namespace sat { if (c.frozen()) num_frozen++; } - SASSERT(num_frozen == s.m_num_frozen); + VERIFY(num_frozen == s.m_num_frozen); return check_clauses(s.begin_learned(), s.end_learned()); } diff --git a/src/sat/sat_local_search.cpp b/src/sat/sat_local_search.cpp index 0b3c2f7c9..61ddd13d8 100644 --- a/src/sat/sat_local_search.cpp +++ b/src/sat/sat_local_search.cpp @@ -580,7 +580,6 @@ namespace sat { bool_var v = null_bool_var; unsigned num_unsat = m_unsat_stack.size(); constraint const& c = m_constraints[m_unsat_stack[m_rand() % num_unsat]]; - unsigned reflipped = 0; bool is_core = m_unsat_stack.size() <= 10; if (m_rand() % 10000 <= m_noise) { // take this branch with 98% probability. @@ -684,7 +683,6 @@ namespace sat { } if (false && is_core && c.m_k < constraint_value(c)) { - ++reflipped; goto reflip; } } diff --git a/src/sat/sat_model_converter.cpp b/src/sat/sat_model_converter.cpp index 656270f16..27cc6823a 100644 --- a/src/sat/sat_model_converter.cpp +++ b/src/sat/sat_model_converter.cpp @@ -167,6 +167,7 @@ namespace sat { // end of clause if (!sat) { TRACE("sat_model_bug", tout << "failed eliminated: " << mk_lits_pp(static_cast(it - itbegin), itbegin) << "\n";); + (void)itbegin; ok = false; } sat = false; diff --git a/src/sat/sat_simplifier.cpp b/src/sat/sat_simplifier.cpp index 9ba536091..56b81604d 100644 --- a/src/sat/sat_simplifier.cpp +++ b/src/sat/sat_simplifier.cpp @@ -288,16 +288,13 @@ namespace sat { clause_vector::iterator it = cs.begin(); clause_vector::iterator it2 = it; clause_vector::iterator end = cs.end(); - unsigned nm = 0; for (; it != end; ++it) { clause & c = *(*it); if (learned && !c.is_learned()) { s.m_clauses.push_back(&c); - ++nm; } else if (!learned && c.is_learned()) { s.m_learned.push_back(&c); - ++nm; } else { *it2 = *it; diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index 0e5d7aa73..7cfa102b7 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -4284,7 +4284,7 @@ namespace sat { lbool solver::get_bounded_consequences(literal_vector const& asms, bool_var_vector const& vars, vector& conseq) { bool_var_set unfixed_vars; - unsigned num_units = 0, num_iterations = 0; + unsigned num_units = 0; for (bool_var v : vars) { unfixed_vars.insert(v); } @@ -4316,7 +4316,6 @@ namespace sat { } while (true) { - ++num_iterations; SASSERT(!inconsistent()); lbool r = bounded_search(); @@ -4379,7 +4378,6 @@ namespace sat { checkpoint(); unsigned num_resolves = 0; unsigned num_fixed = 0; - unsigned num_assigned = 0; lbool is_sat = l_true; for (literal lit : unfixed_lits) { if (value(lit) != l_undef) { @@ -4390,7 +4388,6 @@ namespace sat { continue; } push(); - ++num_assigned; assign_scoped(~lit); propagate(false); while (inconsistent()) { diff --git a/src/sat/sat_solver/sat_smt_solver.cpp b/src/sat/sat_solver/sat_smt_solver.cpp index 8060afcd7..8d99153da 100644 --- a/src/sat/sat_solver/sat_smt_solver.cpp +++ b/src/sat/sat_solver/sat_smt_solver.cpp @@ -174,10 +174,10 @@ class sat_smt_solver : public solver { public: sat_smt_solver(ast_manager& m, params_ref const& p): solver(m), + m_solver(p, m.limit()), m_preprocess_state(*this), m_preprocess(m, p, m_preprocess_state), m_trail(m_preprocess_state.m_trail), - m_solver(p, m.limit()), m_dep(m, m_trail), m_assumptions(m), m_core(m), m_ors(m), m_aux_fmls(m), m_internalized_fmls(m), m_map(m), diff --git a/src/sat/smt/arith_diagnostics.cpp b/src/sat/smt/arith_diagnostics.cpp index 5fd5de07d..8ead3d980 100644 --- a/src/sat/smt/arith_diagnostics.cpp +++ b/src/sat/smt/arith_diagnostics.cpp @@ -83,9 +83,7 @@ namespace arith { } void solver::explain_assumptions(lp::explanation const& e) { - unsigned i = 0; for (auto const & ev : e) { - ++i; auto idx = ev.ci(); if (UINT_MAX == idx) continue; diff --git a/src/sat/smt/pb_solver.cpp b/src/sat/smt/pb_solver.cpp index ade48c42b..fed6aaf7c 100644 --- a/src/sat/smt/pb_solver.cpp +++ b/src/sat/smt/pb_solver.cpp @@ -2791,7 +2791,6 @@ namespace pb { bool solver::subsumes(card& c1, card& c2, literal_vector & comp) { if (c2.lit() != sat::null_literal) return false; - unsigned c2_exclusive = 0; unsigned common = 0; comp.reset(); for (literal l : c2) { @@ -2801,9 +2800,6 @@ namespace pb { else if (is_visited(~l)) { comp.push_back(l); } - else { - ++c2_exclusive; - } } unsigned c1_exclusive = c1.size() - common - comp.size(); @@ -3405,16 +3401,13 @@ namespace pb { unsigned slack = 0; unsigned max_level = 0; - unsigned num_max_level = 0; for (wliteral wl : m_wlits) { if (value(wl.second) != l_false) ++slack; unsigned level = lvl(wl.second); if (level > max_level) { max_level = level; - num_max_level = 1; } else if (max_level == level) { - ++num_max_level; } } if (m_overflow) diff --git a/src/sat/smt/q_eval.cpp b/src/sat/smt/q_eval.cpp index ae79dbeee..35bdc4285 100644 --- a/src/sat/smt/q_eval.cpp +++ b/src/sat/smt/q_eval.cpp @@ -124,11 +124,9 @@ namespace q { std::swap(t, s); } unsigned sz = evidence.size(); - unsigned count = 0; for (euf::enode* t1 : euf::enode_class(tn)) { if (!t1->is_cgr()) continue; - ++count; expr* t2 = t1->get_expr(); if ((c = compare_rec(n, binding, s, t2, evidence), c != l_undef)) { evidence.push_back(euf::enode_pair(t1, tn)); diff --git a/src/sat/smt/q_mam.cpp b/src/sat/smt/q_mam.cpp index 91f19806a..1c356f9f2 100644 --- a/src/sat/smt/q_mam.cpp +++ b/src/sat/smt/q_mam.cpp @@ -3797,7 +3797,6 @@ namespace q { } void rematch(bool use_irrelevant) override { - unsigned lbl = 0; for (auto * t : m_trees) { if (t) { m_interpreter.init(t); @@ -3807,7 +3806,6 @@ namespace q { m_interpreter.execute_core(t, curr); } } - ++lbl; } } diff --git a/src/sat/smt/tseitin_theory_checker.cpp b/src/sat/smt/tseitin_theory_checker.cpp index a15d0277b..74f4e55b0 100644 --- a/src/sat/smt/tseitin_theory_checker.cpp +++ b/src/sat/smt/tseitin_theory_checker.cpp @@ -190,7 +190,7 @@ namespace tseitin { complement_mark(arg); if (is_marked(x) && is_complement(y)) return true; - if (is_marked(y) & is_complement(x)) + if (is_marked(y) && is_complement(x)) return true; } diff --git a/src/tactic/core/cofactor_elim_term_ite.cpp b/src/tactic/core/cofactor_elim_term_ite.cpp index 63455864d..2da133409 100644 --- a/src/tactic/core/cofactor_elim_term_ite.cpp +++ b/src/tactic/core/cofactor_elim_term_ite.cpp @@ -438,7 +438,6 @@ struct cofactor_elim_term_ite::imp { if (m_cache.find(s, t)) return true; - unsigned step = 0; TRACE("cofactor_ite", tout << "cofactor target:\n" << mk_ismt2_pp(s, m) << "\n";); expr_ref curr(m); curr = s; @@ -451,7 +450,6 @@ struct cofactor_elim_term_ite::imp { t = curr.get(); return true; } - step++; expr_ref pos_cofactor(m); expr_ref neg_cofactor(m); m_cofactor.set_cofactor_atom(c); @@ -461,7 +459,7 @@ struct cofactor_elim_term_ite::imp { m_cofactor.set_cofactor_atom(neg_c); m_cofactor(curr, neg_cofactor); curr = m.mk_ite(c, pos_cofactor, neg_cofactor); - TRACE("cofactor", tout << "cofactor_ite step: " << step << "\n" << mk_ismt2_pp(curr, m) << "\n";); + TRACE("cofactor", tout << "cofactor_ite step\n" << mk_ismt2_pp(curr, m) << "\n";); } } return false; @@ -515,7 +513,6 @@ struct cofactor_elim_term_ite::imp { } void cofactor(expr * t, expr_ref & r) { - unsigned step = 0; TRACE("cofactor", tout << "cofactor target:\n" << mk_ismt2_pp(t, m) << "\n";); expr_ref curr(m); curr = t; @@ -526,7 +523,6 @@ struct cofactor_elim_term_ite::imp { r = curr.get(); return; } - step++; expr_ref pos_cofactor(m); expr_ref neg_cofactor(m); m_cofactor.set_cofactor_atom(c); @@ -548,7 +544,7 @@ struct cofactor_elim_term_ite::imp { curr = m.mk_ite(c, pos_cofactor, neg_cofactor); } TRACE("cofactor", - tout << "cofactor_ite step: " << step << "\n"; + tout << "cofactor_ite step\n"; tout << "cofactor: " << mk_ismt2_pp(c, m) << "\n"; tout << mk_ismt2_pp(curr, m) << "\n";); } diff --git a/src/tactic/fd_solver/smtfd_solver.cpp b/src/tactic/fd_solver/smtfd_solver.cpp index 5676c6ee8..01370812f 100644 --- a/src/tactic/fd_solver/smtfd_solver.cpp +++ b/src/tactic/fd_solver/smtfd_solver.cpp @@ -1040,11 +1040,6 @@ namespace smtfd { // A[j] = w: i = j or T[j] = A[j] // void reconcile_stores(app* t, expr* vT, table& tT, expr* vA, table& tA) { - unsigned r = 0; - //if (get_lambda(vA) <= 1) { - // return; - //} - //std::cout << get_lambda(vA) << " " << get_lambda(vT) << "\n"; inc_lambda(vT); for (auto& fA : tA) { f_app fT; @@ -1056,23 +1051,8 @@ namespace smtfd { } if (!tT.find(fA, fT) || (value_of(fA) != value_of(fT) && !eq(m_vargs, fA))) { add_select_store_axiom(t, fA); - ++r; } } -#if 0 - // only up-propagation really needed. - for (auto& fT : tT) { - f_app fA; - if (m_context.at_max()) { - break; - } - if (!tA.find(fT, fA) && t->get_sort() == m.get_sort(fT.m_t->get_arg(0))) { - TRACE("smtfd", tout << "not found\n";); - add_select_store_axiom(t, fT); - ++r; - } - } -#endif } void add_select_store_axiom(app* t, f_app& f) { diff --git a/src/tactic/smtlogics/qfnia_tactic.cpp b/src/tactic/smtlogics/qfnia_tactic.cpp index cf56cced2..3dd66606d 100644 --- a/src/tactic/smtlogics/qfnia_tactic.cpp +++ b/src/tactic/smtlogics/qfnia_tactic.cpp @@ -95,8 +95,6 @@ static tactic * mk_qfnia_sat_solver(ast_manager & m, params_ref const & p) { } static tactic * mk_qfnia_nlsat_solver(ast_manager & m, params_ref const & p) { - params_ref nia2sat_p = p; - nia2sat_p.set_uint("nla2bv_max_bv_size", 64); params_ref simp_p = p; simp_p.set_bool("som", true); // expand into sums of monomials simp_p.set_bool("factor", false);