From 826835fd7c74ba1c9debb590b23a8e95fe00accb Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 30 Sep 2024 08:23:31 -0700 Subject: [PATCH] fixes to build warnings --- src/ast/euf/euf_ac_plugin.cpp | 5 +++-- src/ast/euf/euf_egraph.cpp | 4 ++-- src/math/lp/nla_divisions.cpp | 2 -- src/muz/ddnf/ddnf.cpp | 9 ++------- src/muz/fp/datalog_parser.cpp | 4 +--- src/muz/rel/dl_product_relation.cpp | 1 + src/muz/spacer/spacer_unsat_core_plugin.cpp | 4 +--- src/opt/opt_cores.cpp | 3 +-- src/opt/opt_lns.cpp | 2 -- src/parsers/smt2/smt2parser.cpp | 1 - src/sat/sat_clause_use_list.cpp | 6 +++--- src/sat/sat_lookahead.cpp | 1 - src/shell/dimacs_frontend.cpp | 1 - src/smt/diff_logic.h | 1 + src/smt/dyn_ack.cpp | 6 ------ src/smt/theory_arith_core.h | 17 +---------------- src/smt/theory_bv.cpp | 1 + src/smt/theory_lra.cpp | 2 -- src/smt/theory_pb.cpp | 6 +++--- src/tactic/smtlogics/qfnra_tactic.cpp | 8 -------- src/util/params.cpp | 1 - 21 files changed, 20 insertions(+), 65 deletions(-) diff --git a/src/ast/euf/euf_ac_plugin.cpp b/src/ast/euf/euf_ac_plugin.cpp index 69d0e6572..9a7202362 100644 --- a/src/ast/euf/euf_ac_plugin.cpp +++ b/src/ast/euf/euf_ac_plugin.cpp @@ -440,8 +440,9 @@ namespace euf { TRACE("plugin", tout << "propagate " << eq_id << ": " << eq_pp(*this, m_eqs[eq_id]) << "\n"); // simplify eq using processed - for (auto other_eq : backward_iterator(eq_id)) - TRACE("plugin", tout << "backward iterator " << eq_id << " vs " << other_eq << " " << is_processed(other_eq) << "\n"); + TRACE("plugin", + for (auto other_eq : backward_iterator(eq_id)) + tout << "backward iterator " << eq_id << " vs " << other_eq << " " << is_processed(other_eq) << "\n");); for (auto other_eq : backward_iterator(eq_id)) if (is_processed(other_eq) && backward_simplify(eq_id, other_eq)) goto loop_start; diff --git a/src/ast/euf/euf_egraph.cpp b/src/ast/euf/euf_egraph.cpp index 21bc14ba4..eaa290bbf 100644 --- a/src/ast/euf/euf_egraph.cpp +++ b/src/ast/euf/euf_egraph.cpp @@ -107,8 +107,8 @@ namespace euf { void egraph::update_children(enode* n) { for (enode* child : enode_args(n)) child->get_root()->add_parent(n); - for (enode* child : enode_args(n)) - SASSERT(child->get_root()->m_parents.back() == n); + DEBUG_CODE(for (enode* child : enode_args(n)) + SASSERT(child->get_root()->m_parents.back() == n);); m_updates.push_back(update_record(n, update_record::update_children())); } diff --git a/src/math/lp/nla_divisions.cpp b/src/math/lp/nla_divisions.cpp index 6c3bb178c..72b6d73f0 100644 --- a/src/math/lp/nla_divisions.cpp +++ b/src/math/lp/nla_divisions.cpp @@ -19,7 +19,6 @@ Description: namespace nla { void divisions::add_idivision(lpvar q, lpvar x, lpvar y) { - const auto& lra = m_core.lra; if (x == null_lpvar || y == null_lpvar || q == null_lpvar) return; m_idivisions.push_back({q, x, y}); @@ -27,7 +26,6 @@ namespace nla { } void divisions::add_rdivision(lpvar q, lpvar x, lpvar y) { - auto& lra = m_core.lra; if (x == null_lpvar || y == null_lpvar || q == null_lpvar) return; m_rdivisions.push_back({ q, x, y }); diff --git a/src/muz/ddnf/ddnf.cpp b/src/muz/ddnf/ddnf.cpp index f4f946d09..eaf352475 100644 --- a/src/muz/ddnf/ddnf.cpp +++ b/src/muz/ddnf/ddnf.cpp @@ -678,14 +678,9 @@ namespace datalog { } bool compile_rules1(rule_set const& rules, rule_set& new_rules) { - datalog::rule_set::iterator it = rules.begin(); - datalog::rule_set::iterator end = rules.end(); - unsigned idx = 0; - for (; it != end; ++idx, ++it) { - if (!compile_rule1(**it, rules, new_rules)) { + for (auto const & r : rules) + if (!compile_rule1(*r, rules, new_rules)) return false; - } - } return true; } diff --git a/src/muz/fp/datalog_parser.cpp b/src/muz/fp/datalog_parser.cpp index d748dca63..4d8f60121 100644 --- a/src/muz/fp/datalog_parser.cpp +++ b/src/muz/fp/datalog_parser.cpp @@ -902,7 +902,6 @@ protected: unsigned arg_idx = 0; tok = m_lexer->next_token(); while (tok != TK_EOS && tok != TK_ERROR) { - symbol alias; sort* s = nullptr; if(!f) { @@ -939,7 +938,6 @@ protected: } s = f->get_domain(arg_idx); - symbol var_symbol; tok = parse_arg(tok, s, args); } @@ -1067,7 +1065,7 @@ protected: bool read_line(std::istream& strm, std::string& line) { line.clear(); - char ch = strm.get(); + int ch = strm.get(); while (ch == ' ' || ch == '\t' || ch == '\n' || ch == '\r') { ch = strm.get(); } diff --git a/src/muz/rel/dl_product_relation.cpp b/src/muz/rel/dl_product_relation.cpp index 52c168f12..701bad3cc 100644 --- a/src/muz/rel/dl_product_relation.cpp +++ b/src/muz/rel/dl_product_relation.cpp @@ -1030,6 +1030,7 @@ namespace datalog { } new_rels.push_back(irel); } + (void)old_remain; SASSERT(old_remain==0); //the new specification must be a superset of the old one m_relations = new_rels; diff --git a/src/muz/spacer/spacer_unsat_core_plugin.cpp b/src/muz/spacer/spacer_unsat_core_plugin.cpp index c0a9d7e6f..f0cfcbcd2 100644 --- a/src/muz/spacer/spacer_unsat_core_plugin.cpp +++ b/src/muz/spacer/spacer_unsat_core_plugin.cpp @@ -97,7 +97,6 @@ namespace spacer { // XXX this assertion should be true so there is no need to check for it SASSERT (!m_ctx.is_closed (step)); func_decl* d = step->get_decl(); - symbol sym; TRACE("spacer.farkas", tout << "looking at: " << mk_pp(step, m) << "\n";); if (!m_ctx.is_closed(step) && is_farkas_lemma(m, step)) { @@ -239,9 +238,8 @@ namespace spacer { SASSERT(m_ctx.is_b(step)); func_decl* d = step->get_decl(); - symbol sym; if (!m_ctx.is_closed(step) && // if step is not already interpolated - is_farkas_lemma(m, step)) { + is_farkas_lemma(m, step)) { SASSERT(d->get_num_parameters() == m.get_num_parents(step) + 2); SASSERT(m.has_fact(step)); diff --git a/src/opt/opt_cores.cpp b/src/opt/opt_cores.cpp index 124df63d7..44376e2f5 100644 --- a/src/opt/opt_cores.cpp +++ b/src/opt/opt_cores.cpp @@ -256,12 +256,11 @@ namespace opt { void cores::rotate_cores() { expr_ref_vector soft(m); soft.append(ctx.soft()); - unsigned num_sat = 0, num_unsat = 0, num_undef = 0; + unsigned num_sat = 0, num_undef = 0; lbool is_sat = l_false; while (m.inc() && m_cores.size() < m_max_num_cores) { switch (is_sat) { case l_false: { - ++num_unsat; auto core = unsat_core(); add_core(core); if (core.empty()) diff --git a/src/opt/opt_lns.cpp b/src/opt/opt_lns.cpp index 878c4a3ea..ae9bff215 100644 --- a/src/opt/opt_lns.cpp +++ b/src/opt/opt_lns.cpp @@ -174,7 +174,6 @@ namespace opt { void lns::relax_cores() { if (!m_cores.empty() && m_cores_are_valid) { std::sort(m_cores.begin(), m_cores.end(), [&](expr_ref_vector const& a, expr_ref_vector const& b) { return a.size() < b.size(); }); - unsigned num_disjoint = 0; vector new_cores; for (auto const& c : m_cores) { bool in_core = false; @@ -185,7 +184,6 @@ namespace opt { for (auto* e : c) m_in_core.mark(e); new_cores.push_back(c); - ++num_disjoint; } IF_VERBOSE(2, verbose_stream() << "num cores: " << m_cores.size() << " new cores: " << new_cores.size() << "\n"); ctx.relax_cores(new_cores); diff --git a/src/parsers/smt2/smt2parser.cpp b/src/parsers/smt2/smt2parser.cpp index 98323816a..48c48d0a9 100644 --- a/src/parsers/smt2/smt2parser.cpp +++ b/src/parsers/smt2/smt2parser.cpp @@ -942,7 +942,6 @@ namespace smt2 { } for (unsigned i = 0; i < sz; i++) { pdatatype_decl * d = new_dt_decls[i]; - symbol duplicated; check_duplicate(d, line, pos); if (!is_smt2_6) { // datatypes are inserted up front in SMT2.6 mode, so no need to re-insert them. diff --git a/src/sat/sat_clause_use_list.cpp b/src/sat/sat_clause_use_list.cpp index 7ca0aa2c6..347e49db9 100644 --- a/src/sat/sat_clause_use_list.cpp +++ b/src/sat/sat_clause_use_list.cpp @@ -25,13 +25,13 @@ namespace sat { unsigned sz = 0; for (clause* c : m_clauses) if (!c->was_removed()) - sz++; - SASSERT(sz == m_size); + sz++; + VERIFY(sz == m_size); unsigned redundant = 0; for (clause* c : m_clauses) if (c->is_learned()) redundant++; - SASSERT(redundant == m_num_redundant); + VERIFY(redundant == m_num_redundant); return true; } diff --git a/src/sat/sat_lookahead.cpp b/src/sat/sat_lookahead.cpp index 2f3fc91b2..3fef08559 100644 --- a/src/sat/sat_lookahead.cpp +++ b/src/sat/sat_lookahead.cpp @@ -1392,7 +1392,6 @@ namespace sat { void lookahead::propagate_clauses_searching(literal l) { // clauses where l is negative unsigned sz = m_nary_count[(~l).index()]; - literal lit; SASSERT(m_search_mode == lookahead_mode::searching); for (nary* n : m_nary[(~l).index()]) { if (sz-- == 0) break; diff --git a/src/shell/dimacs_frontend.cpp b/src/shell/dimacs_frontend.cpp index 12dedb64f..afeb604a8 100644 --- a/src/shell/dimacs_frontend.cpp +++ b/src/shell/dimacs_frontend.cpp @@ -110,7 +110,6 @@ static void track_clauses(sat::solver const& src, dst.mk_var(false, true); } sat::literal_vector lits; - sat::literal lit; sat::clause * const * it = src.begin_clauses(); sat::clause * const * end = src.end_clauses(); svector bin_clauses; diff --git a/src/smt/diff_logic.h b/src/smt/diff_logic.h index ee1dbd63a..cd4c8bf75 100644 --- a/src/smt/diff_logic.h +++ b/src/smt/diff_logic.h @@ -569,6 +569,7 @@ public: void traverse_neg_cycle2(bool try_relax, Functor & f) { static unsigned num_conflicts = 0; ++num_conflicts; + (void)num_conflicts; SASSERT(!is_feasible(m_edges[m_last_enabled_edge])); vector potentials; svector edges; diff --git a/src/smt/dyn_ack.cpp b/src/smt/dyn_ack.cpp index 978f1fbe3..66a2c2d5d 100644 --- a/src/smt/dyn_ack.cpp +++ b/src/smt/dyn_ack.cpp @@ -294,7 +294,6 @@ namespace smt { void dyn_ack_manager::gc() { TRACE("dyn_ack", tout << "dyn_ack GC\n";); - unsigned num_deleted = 0; m_to_instantiate.reset(); m_qhead = 0; svector::iterator it = m_app_pairs.begin(); @@ -318,7 +317,6 @@ namespace smt { // SASSERT(num_occs > 0); num_occs = static_cast(num_occs * m_params.m_dack_gc_inv_decay); if (num_occs <= 1) { - num_deleted++; TRACE("dyn_ack", tout << "2) erasing:\n" << mk_pp(p.first, m) << "\n" << mk_pp(p.second, m) << "\n";); m_app_pair2num_occs.erase(p.first, p.second); m.dec_ref(p.first); @@ -337,7 +335,6 @@ namespace smt { // app_pair_lt is not a total order on pairs of expressions. // So, we should use stable_sort to avoid different behavior in different platforms. std::stable_sort(m_to_instantiate.begin(), m_to_instantiate.end(), f); - // IF_VERBOSE(10, if (num_deleted > 0) verbose_stream() << "dynamic ackermann GC: " << num_deleted << "\n";); } class dyn_ack_clause_del_eh : public clause_del_eh { @@ -519,7 +516,6 @@ namespace smt { void dyn_ack_manager::gc_triples() { TRACE("dyn_ack", tout << "dyn_ack GC\n";); - unsigned num_deleted = 0; m_triple.m_to_instantiate.reset(); m_triple.m_qhead = 0; svector::iterator it = m_triple.m_apps.begin(); @@ -544,7 +540,6 @@ namespace smt { // SASSERT(num_occs > 0); num_occs = static_cast(num_occs * m_params.m_dack_gc_inv_decay); if (num_occs <= 1) { - num_deleted++; TRACE("dyn_ack", tout << "2) erasing:\n" << mk_pp(p.first, m) << "\n" << mk_pp(p.second, m) << "\n";); m_triple.m_app2num_occs.erase(p.first, p.second, p.third); m.dec_ref(p.first); @@ -563,7 +558,6 @@ namespace smt { app_triple_lt f(m_triple.m_app2num_occs); // app_triple_lt is not a total order std::stable_sort(m_triple.m_to_instantiate.begin(), m_triple.m_to_instantiate.end(), f); - // IF_VERBOSE(10, if (num_deleted > 0) verbose_stream() << "dynamic ackermann GC: " << num_deleted << "\n";); } diff --git a/src/smt/theory_arith_core.h b/src/smt/theory_arith_core.h index 4e4464a52..8a2d9f3c9 100644 --- a/src/smt/theory_arith_core.h +++ b/src/smt/theory_arith_core.h @@ -3030,7 +3030,7 @@ namespace smt { template void theory_arith::propagate_bounds() { TRACE("propagate_bounds_detail", display(tout);); - unsigned num_prop = 0, count = 0; + unsigned count = 0; for (unsigned r_idx : m_to_check) { row & r = m_rows[r_idx]; if (r.get_base_var() != null_theory_var) { @@ -3039,34 +3039,19 @@ namespace smt { int upper_idx; is_row_useful_for_bound_prop(r, lower_idx, upper_idx); - ++num_prop; if (lower_idx >= 0) count += imply_bound_for_monomial(r, lower_idx, true); else if (lower_idx == -1) count += imply_bound_for_all_monomials(r, true); - else - --num_prop; - ++num_prop; if (upper_idx >= 0) count += imply_bound_for_monomial(r, upper_idx, false); else if (upper_idx == -1) count += imply_bound_for_all_monomials(r, false); - else - --num_prop; // sneaking cheap eq detection in this loop propagate_cheap_eq(r_idx); } - -#if 0 - theory_var v = r.get_base_var(); - if (!is_int(v) || get_value(v).is_int()) { - // If an integer value is not assigned to an integer value, then - // bound propagation can diverge. - m_in_to_check.remove(v); - } -#endif } } diff --git a/src/smt/theory_bv.cpp b/src/smt/theory_bv.cpp index ca327891c..5740285a2 100644 --- a/src/smt/theory_bv.cpp +++ b/src/smt/theory_bv.cpp @@ -1988,6 +1988,7 @@ namespace smt { while (curr != v); zero_one_bits const & _bits = m_zero_one_bits[v]; + (void)num_bits; SASSERT(_bits.size() == num_bits); bool_vector already_found; already_found.resize(bv_sz, false); diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index 135744f02..f0615293d 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -3495,10 +3495,8 @@ public: bool validate_eq(enode* x, enode* y) { static bool s_validating = false; - static unsigned s_count = 0; if (s_validating) return true; - ++s_count; flet _svalid(s_validating, true); context nctx(m, ctx().get_fparams(), ctx().get_params()); add_background(nctx); diff --git a/src/smt/theory_pb.cpp b/src/smt/theory_pb.cpp index 25c8e7195..ed3ff0942 100644 --- a/src/smt/theory_pb.cpp +++ b/src/smt/theory_pb.cpp @@ -2127,9 +2127,9 @@ namespace smt { tout << "sum: " << sum << " " << maxsum << " "; tout << ctx.get_assignment(c.lit()) << "\n";); - SASSERT(sum <= maxsum); - SASSERT((sum >= c.k()) == (ctx.get_assignment(c.lit()) == l_true)); - SASSERT((maxsum < c.k()) == (ctx.get_assignment(c.lit()) == l_false)); + VERIFY(sum <= maxsum); + VERIFY((sum >= c.k()) == (ctx.get_assignment(c.lit()) == l_true)); + VERIFY((maxsum < c.k()) == (ctx.get_assignment(c.lit()) == l_false)); } void theory_pb::validate_final_check(ineq& c) { diff --git a/src/tactic/smtlogics/qfnra_tactic.cpp b/src/tactic/smtlogics/qfnra_tactic.cpp index 5e5f2508b..79e0a4b39 100644 --- a/src/tactic/smtlogics/qfnra_tactic.cpp +++ b/src/tactic/smtlogics/qfnra_tactic.cpp @@ -25,14 +25,6 @@ Notes: #include "tactic/smtlogics/qflra_tactic.h" -static tactic * mk_qfnra_sat_solver(ast_manager& m, params_ref const& p, unsigned bv_size) { - params_ref nra2sat_p = p; - nra2sat_p.set_uint("nla2bv_max_bv_size", p.get_uint("nla2bv_max_bv_size", bv_size)); - - return and_then(mk_nla2bv_tactic(m, nra2sat_p), - mk_smt_tactic(m), - mk_fail_if_undecided_tactic()); -} tactic * mk_multilinear_ls_tactic(ast_manager & m, params_ref const & p, unsigned ls_time = 60) { params_ref p_mls = p; diff --git a/src/util/params.cpp b/src/util/params.cpp index 3440673b7..8ea7c1da3 100644 --- a/src/util/params.cpp +++ b/src/util/params.cpp @@ -390,7 +390,6 @@ public: void reset(char const * k); void validate(param_descrs const & p) { - symbol suffix, prefix; for (params::entry& e : m_entries) { param_kind expected = p.get_kind_in_module(e.first); if (expected == CPK_INVALID) {