From 96e157e201308d7beba556f62b145edc9263d0a7 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 17 May 2016 13:54:22 -0700 Subject: [PATCH 1/4] fix warnings for unused variables Signed-off-by: Nikolaj Bjorner --- src/ackermannization/lackr.cpp | 5 +- src/ast/ast.cpp | 1 + src/ast/rewriter/bv_trailing.cpp | 10 +- src/ast/simplifier/simplifier.cpp | 1 + src/duality/duality_rpfp.cpp | 3 +- src/math/euclid/euclidean_solver.cpp | 4 +- src/math/polynomial/upolynomial.cpp | 7 +- .../polynomial/upolynomial_factorization.cpp | 6 +- src/math/simplex/simplex_def.h | 1 + src/math/simplex/sparse_matrix_def.h | 13 +-- src/muz/pdr/pdr_farkas_learner.cpp | 1 + src/muz/rel/dl_external_relation.cpp | 3 +- src/muz/rel/dl_finite_product_relation.cpp | 9 +- src/muz/rel/udoc_relation.cpp | 3 +- src/muz/transforms/dl_mk_bit_blast.cpp | 3 +- .../dl_mk_quantifier_abstraction.cpp | 3 +- src/nlsat/nlsat_explain.cpp | 3 +- src/nlsat/nlsat_interval_set.cpp | 16 +-- src/nlsat/nlsat_solver.cpp | 35 +++---- src/opt/hitting_sets.cpp | 3 +- src/parsers/smt2/smt2parser.cpp | 3 + src/qe/qe.cpp | 3 +- src/qe/qe_arith_plugin.cpp | 21 ++-- src/qe/qe_sat_tactic.cpp | 3 +- src/sat/sat_integrity_checker.cpp | 8 +- src/sat/sat_sls.cpp | 97 ++++++++++--------- src/sat/sat_solver.cpp | 8 +- src/smt/smt_conflict_resolution.cpp | 5 +- src/smt/smt_context.cpp | 10 +- src/smt/theory_arith_aux.h | 2 +- src/smt/theory_array.cpp | 3 +- src/smt/theory_bv.cpp | 9 +- src/smt/theory_datatype.cpp | 3 +- src/smt/theory_diff_logic_def.h | 33 +++---- src/smt/theory_fpa.cpp | 19 ++-- src/smt/theory_wmaxsat.cpp | 2 +- src/util/mpf.cpp | 4 +- src/util/mpff.cpp | 1 + 38 files changed, 180 insertions(+), 184 deletions(-) diff --git a/src/ackermannization/lackr.cpp b/src/ackermannization/lackr.cpp index b1a58c01b..461d2080f 100644 --- a/src/ackermannization/lackr.cpp +++ b/src/ackermannization/lackr.cpp @@ -134,7 +134,6 @@ void lackr::eager_enc() { const fun2terms_map::iterator e = m_fun2terms.end(); for (fun2terms_map::iterator i = m_fun2terms.begin(); i != e; ++i) { checkpoint(); - func_decl* const fd = i->m_key; app_set * const ts = i->get_value(); const app_set::iterator r = ts->end(); for (app_set::iterator j = ts->begin(); j != r; ++j) { @@ -143,8 +142,8 @@ void lackr::eager_enc() { for (; k != r; ++k) { app * const t1 = *j; app * const t2 = *k; - SASSERT(t1->get_decl() == fd); - SASSERT(t2->get_decl() == fd); + SASSERT(t1->get_decl() == i->m_key); + SASSERT(t2->get_decl() == i->m_key); if (t1 == t2) continue; ackr(t1,t2); } diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp index 0365a267e..fcf9365e3 100644 --- a/src/ast/ast.cpp +++ b/src/ast/ast.cpp @@ -1495,6 +1495,7 @@ void ast_manager::copy_families_plugins(ast_manager const & from) { if (m_family_manager.has_family(fid)) tout << get_family_id(fid_name) << "\n";); if (!m_family_manager.has_family(fid)) { family_id new_fid = mk_family_id(fid_name); + (void)new_fid; TRACE("copy_families_plugins", tout << "new target fid created: " << new_fid << " fid_name: " << fid_name << "\n";); } TRACE("copy_families_plugins", tout << "target fid: " << get_family_id(fid_name) << "\n";); diff --git a/src/ast/rewriter/bv_trailing.cpp b/src/ast/rewriter/bv_trailing.cpp index 414854f3a..cf50ab0e2 100644 --- a/src/ast/rewriter/bv_trailing.cpp +++ b/src/ast/rewriter/bv_trailing.cpp @@ -67,9 +67,10 @@ struct bv_trailing::imp { } expr_ref out1(m); expr_ref out2(m); - const unsigned rm1 = remove_trailing(e1, min, out1, TRAILING_DEPTH); - const unsigned rm2 = remove_trailing(e2, min, out2, TRAILING_DEPTH); - SASSERT(rm1 == min && rm2 == min); + DEBUG_CODE( + const unsigned rm1 = remove_trailing(e1, min, out1, TRAILING_DEPTH); + const unsigned rm2 = remove_trailing(e2, min, out2, TRAILING_DEPTH); + SASSERT(rm1 == min && rm2 == min);); const bool are_eq = m.are_equal(out1, out2); result = are_eq ? m.mk_true() : m.mk_eq(out1, out2); return are_eq ? BR_DONE : BR_REWRITE2; @@ -122,9 +123,8 @@ struct bv_trailing::imp { expr_ref tmp(m); for (unsigned i = 0; i < num; ++i) { expr * const curr = a->get_arg(i); - const unsigned crm = remove_trailing(curr, to_rm, tmp, depth - 1); + VERIFY(to_rm == remove_trailing(curr, to_rm, tmp, depth - 1)); new_args.push_back(tmp); - SASSERT(crm == to_rm); } result = m.mk_app(m_util.get_fid(), OP_BADD, new_args.size(), new_args.c_ptr()); return to_rm; diff --git a/src/ast/simplifier/simplifier.cpp b/src/ast/simplifier/simplifier.cpp index 895aa529b..63731c679 100644 --- a/src/ast/simplifier/simplifier.cpp +++ b/src/ast/simplifier/simplifier.cpp @@ -63,6 +63,7 @@ void simplifier::operator()(expr * s, expr_ref & r, proof_ref & p) { m_need_reset = true; reinitialize(); expr * s_orig = s; + (void)s_orig; expr * old_s; expr * result; proof * result_proof; diff --git a/src/duality/duality_rpfp.cpp b/src/duality/duality_rpfp.cpp index c47662ddf..c86ff9f62 100755 --- a/src/duality/duality_rpfp.cpp +++ b/src/duality/duality_rpfp.cpp @@ -2365,8 +2365,7 @@ namespace Duality { Term CanonIneqTerm(const Term &p){ Term term,bound; Term ps = p.simplify(); - bool ok = IsCanonIneq(ps,term,bound); - assert(ok); + VERIFY(IsCanonIneq(ps,term,bound)); return term - bound; } diff --git a/src/math/euclid/euclidean_solver.cpp b/src/math/euclid/euclidean_solver.cpp index af11d4304..b33dbf3aa 100644 --- a/src/math/euclid/euclidean_solver.cpp +++ b/src/math/euclid/euclidean_solver.cpp @@ -580,8 +580,8 @@ struct euclidean_solver::imp { void substitute_most_recent_solution(var x) { SASSERT(!m_solution.empty()); - equation & eq = *(m_solution.back()); - TRACE("euclidean_solver", tout << "applying solution for x" << x << "\n"; display(tout, eq); tout << "\n";); + TRACE("euclidean_solver", tout << "applying solution for x" << x << "\n"; + display(tout, *(m_solution.back())); tout << "\n";); occs & use_list = m_occs[x]; occs::iterator it = use_list.begin(); occs::iterator end = use_list.end(); diff --git a/src/math/polynomial/upolynomial.cpp b/src/math/polynomial/upolynomial.cpp index 78ce912f4..aa26ccf4c 100644 --- a/src/math/polynomial/upolynomial.cpp +++ b/src/math/polynomial/upolynomial.cpp @@ -2759,6 +2759,7 @@ namespace upolynomial { bool manager::refine_core(unsigned sz, numeral const * p, int sign_a, mpbq_manager & bqm, mpbq & a, mpbq & b) { SASSERT(sign_a == eval_sign_at(sz, p, a)); int sign_b = -sign_a; + (void)sign_b; SASSERT(sign_b == eval_sign_at(sz, p, b)); SASSERT(sign_a == -sign_b); SASSERT(sign_a != 0 && sign_b != 0); @@ -2810,9 +2811,8 @@ namespace upolynomial { bool manager::refine(unsigned sz, numeral const * p, mpbq_manager & bqm, mpbq & a, mpbq & b, unsigned prec_k) { int sign_a = eval_sign_at(sz, p, a); - int sign_b = -sign_a; - SASSERT(eval_sign_at(sz, p, b) == sign_b); - SASSERT(sign_a != 0 && sign_b != 0); + SASSERT(eval_sign_at(sz, p, b) == -sign_a); + SASSERT(sign_a != 0); return refine_core(sz, p, sign_a, bqm, a, b, prec_k); } @@ -2928,6 +2928,7 @@ namespace upolynomial { SASSERT(sign_a == eval_sign_at(sz, p, a)); } int sign_b = -sign_a; + (void) sign_b; SASSERT(sign_b == eval_sign_at(sz, p, b)); SASSERT(sign_a != 0 && sign_b != 0); if (has_zero_roots(sz, p)) { diff --git a/src/math/polynomial/upolynomial_factorization.cpp b/src/math/polynomial/upolynomial_factorization.cpp index b36658bba..5a7aefa18 100644 --- a/src/math/polynomial/upolynomial_factorization.cpp +++ b/src/math/polynomial/upolynomial_factorization.cpp @@ -371,9 +371,10 @@ void zp_square_free_factor(zp_manager & upm, numeral_vector const & f, zp_factor bool zp_factor(zp_manager & upm, numeral_vector const & f, zp_factors & factors) { - unsigned p = get_p_from_manager(upm.m()); - TRACE("polynomial::factorization", tout << "polynomial::factor("; upm.display(tout, f); tout << ") over Z_" << p << endl;); + TRACE("polynomial::factorization", + unsigned p = get_p_from_manager(upm.m()); + tout << "polynomial::factor("; upm.display(tout, f); tout << ") over Z_" << p << endl;); // get the sq-free parts (all of them will be monic) zp_factors sq_free_factors(upm); @@ -435,6 +436,7 @@ bool zp_factor_square_free_berlekamp(zp_manager & upm, numeral_vector const & f, // process the null space vectors (skip first one, it's [1, 0, ..., 0]) while generating the factors unsigned d = upm.degree(f); + (void)d; scoped_numeral_vector v_k(zpm); while (Q_I.next_null_space_vector(v_k)) { diff --git a/src/math/simplex/simplex_def.h b/src/math/simplex/simplex_def.h index 6ca4048ad..cb86e2a85 100644 --- a/src/math/simplex/simplex_def.h +++ b/src/math/simplex/simplex_def.h @@ -998,6 +998,7 @@ namespace simplex { template bool simplex::well_formed_row(row const& r) const { var_t s = m_row2base[r.id()]; + (void)s; SASSERT(m_vars[s].m_base2row == r.id()); SASSERT(m_vars[s].m_is_base); // SASSERT(m.is_neg(m_vars[s].m_base_coeff)); diff --git a/src/math/simplex/sparse_matrix_def.h b/src/math/simplex/sparse_matrix_def.h index 09a8a9225..78a4e8301 100644 --- a/src/math/simplex/sparse_matrix_def.h +++ b/src/math/simplex/sparse_matrix_def.h @@ -509,12 +509,13 @@ namespace simplex { dead.insert(i); continue; } - SASSERT(!vars.contains(e.m_var)); - SASSERT(!m.is_zero(e.m_coeff)); - SASSERT(e.m_var != dead_id); - col_entry const& c = m_columns[e.m_var].m_entries[e.m_col_idx]; - SASSERT((unsigned)c.m_row_id == row_id); - SASSERT((unsigned)c.m_row_idx == i); + DEBUG_CODE( + SASSERT(!vars.contains(e.m_var)); + SASSERT(!m.is_zero(e.m_coeff)); + SASSERT(e.m_var != dead_id); + col_entry const& c = m_columns[e.m_var].m_entries[e.m_col_idx]; + SASSERT((unsigned)c.m_row_id == row_id); + SASSERT((unsigned)c.m_row_idx == i);); vars.insert(e.m_var); } int idx = r.m_first_free_idx; diff --git a/src/muz/pdr/pdr_farkas_learner.cpp b/src/muz/pdr/pdr_farkas_learner.cpp index 0565cb23b..54d9ada89 100644 --- a/src/muz/pdr/pdr_farkas_learner.cpp +++ b/src/muz/pdr/pdr_farkas_learner.cpp @@ -923,6 +923,7 @@ namespace pdr { if (p->get_decl_kind() == PR_ASSERTED && bs.contains(m.get_fact(p))) { expr* fact = m.get_fact(p); + (void)p0; TRACE("farkas_learner", tout << mk_ll_pp(p0,m) << "\n"; tout << "Add: " << mk_pp(p,m) << "\n";); diff --git a/src/muz/rel/dl_external_relation.cpp b/src/muz/rel/dl_external_relation.cpp index f32509473..e9c24abd3 100644 --- a/src/muz/rel/dl_external_relation.cpp +++ b/src/muz/rel/dl_external_relation.cpp @@ -338,9 +338,8 @@ namespace datalog { : m_plugin(p), m_condition(condition, p.get_ast_manager()), m_filter_fn(p.get_ast_manager()) { - ast_manager& m = p.get_ast_manager(); p.mk_filter_fn(relation_sort, condition, m_filter_fn); - SASSERT(m.is_bool(condition)); + SASSERT(p.get_ast_manager().is_bool(condition)); } virtual void operator()(relation_base & r) { diff --git a/src/muz/rel/dl_finite_product_relation.cpp b/src/muz/rel/dl_finite_product_relation.cpp index 86fef433b..879e29699 100644 --- a/src/muz/rel/dl_finite_product_relation.cpp +++ b/src/muz/rel/dl_finite_product_relation.cpp @@ -1566,13 +1566,12 @@ namespace datalog { return; } - finite_product_relation_plugin & plugin = r.get_plugin(); - if(!m_neg_intersection_join) { - } scoped_rel intersection = get((*m_neg_intersection_join)(r, neg)); - SASSERT(&intersection->get_plugin()==&plugin); //the result of join is also finite product - SASSERT(r.get_signature()==intersection->get_signature()); + DEBUG_CODE( + finite_product_relation_plugin & plugin = r.get_plugin(); + SASSERT(&intersection->get_plugin()==&plugin); //the result of join is also finite product + SASSERT(r.get_signature()==intersection->get_signature());); table_base & r_table = r.get_table(); table_plugin & tplugin = r_table.get_plugin(); relation_manager & rmgr = r.get_manager(); diff --git a/src/muz/rel/udoc_relation.cpp b/src/muz/rel/udoc_relation.cpp index dda674131..22e70a367 100644 --- a/src/muz/rel/udoc_relation.cpp +++ b/src/muz/rel/udoc_relation.cpp @@ -404,7 +404,7 @@ namespace datalog { rename_fn(udoc_relation const& t, unsigned cycle_len, const unsigned * cycle) : convenient_relation_rename_fn(t.get_signature(), cycle_len, cycle) { udoc_plugin& p = t.get_plugin(); - ast_manager& m = p.get_ast_manager(); + relation_signature const& sig1 = t.get_signature(); relation_signature const& sig2 = get_result_signature(); unsigned_vector permutation0, column_info; @@ -429,6 +429,7 @@ namespace datalog { SASSERT(column == t.get_num_bits()); TRACE("doc", + ast_manager& m = p.get_ast_manager(); sig1.output(m, tout << "sig1: "); tout << "\n"; sig2.output(m, tout << "sig2: "); tout << "\n"; tout << "permute: "; diff --git a/src/muz/transforms/dl_mk_bit_blast.cpp b/src/muz/transforms/dl_mk_bit_blast.cpp index 6d1225641..98172f041 100644 --- a/src/muz/transforms/dl_mk_bit_blast.cpp +++ b/src/muz/transforms/dl_mk_bit_blast.cpp @@ -70,13 +70,12 @@ namespace datalog { func_interp* f = model->get_func_interp(p); if (!f) continue; expr_ref body(m); - unsigned arity_p = p->get_arity(); unsigned arity_q = q->get_arity(); TRACE("dl", model_v2_pp(tout, *model); tout << mk_pp(p, m) << "\n"; tout << mk_pp(q, m) << "\n";); - SASSERT(0 < arity_p); + SASSERT(0 < p->get_arity()); SASSERT(f); model->register_decl(p, f->copy()); func_interp* g = alloc(func_interp, m, arity_q); diff --git a/src/muz/transforms/dl_mk_quantifier_abstraction.cpp b/src/muz/transforms/dl_mk_quantifier_abstraction.cpp index 57948a2ff..d3fe1004a 100644 --- a/src/muz/transforms/dl_mk_quantifier_abstraction.cpp +++ b/src/muz/transforms/dl_mk_quantifier_abstraction.cpp @@ -71,9 +71,8 @@ namespace datalog { svector const& is_bound = m_bound[i]; func_interp* f = old_model->get_func_interp(p); expr_ref body(m); - unsigned arity_p = p->get_arity(); unsigned arity_q = q->get_arity(); - SASSERT(0 < arity_p); + SASSERT(0 < p->get_arity()); func_interp* g = alloc(func_interp, m, arity_q); if (f) { diff --git a/src/nlsat/nlsat_explain.cpp b/src/nlsat/nlsat_explain.cpp index 23480eed4..92a80375e 100644 --- a/src/nlsat/nlsat_explain.cpp +++ b/src/nlsat/nlsat_explain.cpp @@ -1165,8 +1165,7 @@ namespace nlsat { if (max_var(new_lit) < max) { // The conflicting core may have redundant literals. // We should check whether new_lit is true in the current model, and discard it if that is the case - lbool val = m_solver.value(new_lit); - SASSERT(val != l_undef); + VERIFY(m_solver.value(new_lit) != l_undef); if (m_solver.value(new_lit) == l_false) add_literal(new_lit); new_lit = true_literal; diff --git a/src/nlsat/nlsat_interval_set.cpp b/src/nlsat/nlsat_interval_set.cpp index 68609cb3f..44e1128d1 100644 --- a/src/nlsat/nlsat_interval_set.cpp +++ b/src/nlsat/nlsat_interval_set.cpp @@ -102,14 +102,14 @@ namespace nlsat { // Check if the intervals are valid, ordered, and are disjoint. bool check_interval_set(anum_manager & am, unsigned sz, interval const * ints) { - for (unsigned i = 0; i < sz; i++) { - interval const & curr = ints[i]; - SASSERT(check_interval(am, curr)); - if (i < sz - 1) { - interval const & next = ints[i+1]; - SASSERT(check_no_overlap(am, curr, next)); - } - } + DEBUG_CODE( + for (unsigned i = 0; i < sz; i++) { + interval const & curr = ints[i]; + SASSERT(check_interval(am, curr)); + if (i < sz - 1) { + SASSERT(check_no_overlap(am, curr, ints[i+1])); + } + }); return true; } diff --git a/src/nlsat/nlsat_solver.cpp b/src/nlsat/nlsat_solver.cpp index ae3f1252b..4f9854d87 100644 --- a/src/nlsat/nlsat_solver.cpp +++ b/src/nlsat/nlsat_solver.cpp @@ -1728,27 +1728,28 @@ namespace nlsat { // ----------------------- bool check_watches() const { - for (var x = 0; x < num_vars(); x++) { - clause_vector const & cs = m_watches[x]; - unsigned sz = cs.size(); - for (unsigned i = 0; i < sz; i++) { - clause const & c = *(cs[i]); - SASSERT(max_var(c) == x); - } - } + DEBUG_CODE( + for (var x = 0; x < num_vars(); x++) { + clause_vector const & cs = m_watches[x]; + unsigned sz = cs.size(); + for (unsigned i = 0; i < sz; i++) { + SASSERT(max_var(*(cs[i])) == x); + } + }); return true; } bool check_bwatches() const { - for (bool_var b = 0; b < m_bwatches.size(); b++) { - clause_vector const & cs = m_bwatches[b]; - unsigned sz = cs.size(); - for (unsigned i = 0; i < sz; i++) { - clause const & c = *(cs[i]); - SASSERT(max_var(c) == null_var); - SASSERT(max_bvar(c) == b); - } - } + DEBUG_CODE( + for (bool_var b = 0; b < m_bwatches.size(); b++) { + clause_vector const & cs = m_bwatches[b]; + unsigned sz = cs.size(); + for (unsigned i = 0; i < sz; i++) { + clause const & c = *(cs[i]); + SASSERT(max_var(c) == null_var); + SASSERT(max_bvar(c) == b); + } + }); return true; } diff --git a/src/opt/hitting_sets.cpp b/src/opt/hitting_sets.cpp index 8bbad6683..678d7924e 100644 --- a/src/opt/hitting_sets.cpp +++ b/src/opt/hitting_sets.cpp @@ -762,6 +762,7 @@ namespace opt { } bool invariant() { + DEBUG_CODE( for (unsigned i = 0; i < m_fwatch.size(); ++i) { for (unsigned j = 0; j < m_fwatch[i].size(); ++j) { set const& S = *m_F[m_fwatch[i][j]]; @@ -773,7 +774,7 @@ namespace opt { set const& S = *m_T[m_twatch[i][j]]; SASSERT(S[0] == i || S[1] == i); } - } + }); return true; } diff --git a/src/parsers/smt2/smt2parser.cpp b/src/parsers/smt2/smt2parser.cpp index a995c5917..17a931cc3 100644 --- a/src/parsers/smt2/smt2parser.cpp +++ b/src/parsers/smt2/smt2parser.cpp @@ -473,6 +473,7 @@ namespace smt2 { void parse_sexpr() { unsigned stack_pos = sexpr_stack().size(); + (void)stack_pos; unsigned num_frames = 0; do { unsigned line = m_scanner.get_line(); @@ -631,6 +632,7 @@ namespace smt2 { void parse_psort() { unsigned stack_pos = psort_stack().size(); + (void)stack_pos; unsigned num_frames = 0; do { if (curr_is_identifier()) { @@ -693,6 +695,7 @@ namespace smt2 { void parse_sort(char const* context) { unsigned stack_pos = sort_stack().size(); + (void)stack_pos; unsigned num_frames = 0; do { if (curr_is_identifier()) { diff --git a/src/qe/qe.cpp b/src/qe/qe.cpp index 1df22e385..9742d2051 100644 --- a/src/qe/qe.cpp +++ b/src/qe/qe.cpp @@ -1899,8 +1899,7 @@ namespace qe { // The variable v is to be assigned a value in a range. // void constrain_assignment() { - expr* fml = m_current->fml(); - SASSERT(fml); + SASSERT(m_current->fml()); rational k; app* x; if (!find_min_weight(x, k)) { diff --git a/src/qe/qe_arith_plugin.cpp b/src/qe/qe_arith_plugin.cpp index 8bb3fa6e2..38861df65 100644 --- a/src/qe/qe_arith_plugin.cpp +++ b/src/qe/qe_arith_plugin.cpp @@ -1153,21 +1153,20 @@ namespace qe { bool get_bound(contains_app& contains_x, app* a) { - ast_manager& m = m_util.get_manager(); - app* x = contains_x.x(); - if (m_mark.is_marked(a) || + bool has_bound = + m_mark.is_marked(a) || get_le_bound(contains_x, a) || get_lt_bound(contains_x, a) || get_divides(contains_x, a) || - get_nested_divs(contains_x, a)) { - TRACE("qe_verbose", tout << "Bound for " << mk_pp(x, m) << " within " << mk_pp(a, m) << "\n";); + get_nested_divs(contains_x, a); + if (has_bound) { m_mark.mark(a, true); - return true; - } - else { - TRACE("qe", tout << "No bound for " << mk_pp(x, m) << " within " << mk_pp(a, m) << "\n";); - return false; } + TRACE("qe_verbose", + ast_manager& m = m_util.get_manager(); + app* x = contains_x.x(); + tout << has_bound << " bound for " << mk_pp(x, m) << " within " << mk_pp(a, m) << "\n";); + return has_bound; } unsigned lt_size() { return m_lt_terms.size(); } @@ -2323,7 +2322,6 @@ public: unsigned sz = bounds.size(is_strict, !is_lower); bool is_strict_real = !is_eq_ctx && m_util.is_real(x) && !is_strict_ctx; bool strict_resolve = is_strict || is_strict_ctx || is_strict_real; - app* atm = bounds.atoms(is_strict_ctx, is_lower)[index]; for (unsigned i = 0; i < sz; ++i) { app* e = bounds.atoms(is_strict, !is_lower)[i]; @@ -2341,6 +2339,7 @@ public: m_ctx.add_constraint(true, mk_not(e), tmp); TRACE("qe_verbose", + app* atm = bounds.atoms(is_strict_ctx, is_lower)[index]; tout << mk_pp(atm, m) << " "; tout << mk_pp(e, m) << " ==>\n"; tout << mk_pp(tmp, m) << "\n"; diff --git a/src/qe/qe_sat_tactic.cpp b/src/qe/qe_sat_tactic.cpp index 455c1d08e..c2912692c 100644 --- a/src/qe/qe_sat_tactic.cpp +++ b/src/qe/qe_sat_tactic.cpp @@ -603,8 +603,7 @@ namespace qe { m_solver.assert_expr(m.mk_iff(proxies.back(), m_assignments[i].get())); TRACE("qe", tout << "assignment: " << mk_pp(m_assignments[i].get(), m) << "\n";); } - lbool is_sat = m_solver.check(proxies.size(), proxies.c_ptr()); - SASSERT(is_sat == l_false); + VERIFY(l_false == m_solver.check(proxies.size(), proxies.c_ptr())); unsigned core_size = m_solver.get_unsat_core_size(); for (unsigned i = 0; i < core_size; ++i) { core.push_back(proxy_map.find(m_solver.get_unsat_core_expr(i))); diff --git a/src/sat/sat_integrity_checker.cpp b/src/sat/sat_integrity_checker.cpp index d0052b8c2..ac2a51c4d 100644 --- a/src/sat/sat_integrity_checker.cpp +++ b/src/sat/sat_integrity_checker.cpp @@ -40,8 +40,7 @@ namespace sat { if (it->is_clause()) { if (it->get_clause_offset() == cls_off) { // the blocked literal must be in the clause. - literal l = it->get_blocked_literal(); - SASSERT(c.contains(l)); + SASSERT(c.contains(it->get_blocked_literal())); return true; } } @@ -154,10 +153,11 @@ namespace sat { } bool integrity_checker::check_watches() const { + DEBUG_CODE( vector::const_iterator it = s.m_watches.begin(); vector::const_iterator end = s.m_watches.end(); for (unsigned l_idx = 0; it != end; ++it, ++l_idx) { - literal l = ~to_literal(l_idx); + literal l = ~to_literal(l_idx); watch_list const & wlist = *it; CTRACE("sat_bug", s.was_eliminated(l.var()) && !wlist.empty(), tout << "l: " << l << "\n"; @@ -193,7 +193,7 @@ namespace sat { break; } } - } + }); return true; } diff --git a/src/sat/sat_sls.cpp b/src/sat/sat_sls.cpp index 76e222f02..7efc0ce0b 100644 --- a/src/sat/sat_sls.cpp +++ b/src/sat/sat_sls.cpp @@ -269,35 +269,36 @@ namespace sat { } void sls::check_invariant() { - for (unsigned i = 0; i < m_clauses.size(); ++i) { - clause const& c = *m_clauses[i]; - bool is_sat = c.satisfied_by(m_model); - SASSERT(is_sat != m_false.contains(i)); - SASSERT(is_sat == (m_num_true[i] > 0)); - } + DEBUG_CODE( + for (unsigned i = 0; i < m_clauses.size(); ++i) { + clause const& c = *m_clauses[i]; + bool is_sat = c.satisfied_by(m_model); + SASSERT(is_sat != m_false.contains(i)); + SASSERT(is_sat == (m_num_true[i] > 0)); + }); } void sls::check_use_list() { - - for (unsigned i = 0; i < m_clauses.size(); ++i) { - clause const& c = *m_clauses[i]; - for (unsigned j = 0; j < c.size(); ++j) { - unsigned idx = c[j].index(); - SASSERT(m_use_list[idx].contains(i)); - } - } - - for (unsigned i = 0; i < m_use_list.size(); ++i) { - literal lit = to_literal(i); - for (unsigned j = 0; j < m_use_list[i].size(); ++j) { - clause const& c = *m_clauses[m_use_list[i][j]]; - bool found = false; - for (unsigned k = 0; !found && k < c.size(); ++k) { - found = c[k] == lit; + DEBUG_CODE( + for (unsigned i = 0; i < m_clauses.size(); ++i) { + clause const& c = *m_clauses[i]; + for (unsigned j = 0; j < c.size(); ++j) { + unsigned idx = c[j].index(); + SASSERT(m_use_list[idx].contains(i)); } - SASSERT(found); } - } + + for (unsigned i = 0; i < m_use_list.size(); ++i) { + literal lit = to_literal(i); + for (unsigned j = 0; j < m_use_list[i].size(); ++j) { + clause const& c = *m_clauses[m_use_list[i][j]]; + bool found = false; + for (unsigned k = 0; !found && k < c.size(); ++k) { + found = c[k] == lit; + } + SASSERT(found); + } + }); } void sls::display(std::ostream& out) const { @@ -556,8 +557,7 @@ namespace sat { void wsls::recompute_hscores(literal lit) { SASSERT(value_at(lit, m_model) == l_true); - bool_var v = lit.var(); - TRACE("sat", tout << v << " := " << m_hscore[v] << "\n";); + TRACE("sat", tout << lit.var() << " := " << m_hscore[lit.var()] << "\n";); unsigned_vector const& use1 = get_use(lit); unsigned sz = use1.size(); for (unsigned i = 0; i < sz; ++i) { @@ -647,28 +647,29 @@ namespace sat { // The hscore is the reward for flipping the truth value of variable v. // hscore(v) = Sum weight(c) for num_true(c) = 0 and v in c // - Sum weight(c) for num_true(c) = 1 and (v in c, M(v) or !v in c and !M(v)) - for (unsigned v = 0; v < s.num_vars(); ++v) { - int hs = compute_hscore(v); - CTRACE("sat", hs != m_hscore[v], display(tout << v << " - computed: " << hs << " - assigned: " << m_hscore[v] << "\n");); - SASSERT(m_hscore[v] == hs); - } - - // The score(v) is the reward on soft clauses for flipping v. - for (unsigned j = 0; j < m_soft.size(); ++j) { - unsigned v = m_soft[j].var(); - double ss = (l_true == value_at(m_soft[j], m_model))?(-m_weights[j]):m_weights[j]; - SASSERT(m_sscore[v] == ss); - } - - // m_H are values such that m_hscore > 0 and sscore = 0. - for (bool_var v = 0; v < m_hscore.size(); ++v) { - SASSERT((m_hscore[v] > 0 && !m_tabu[v] && m_sscore[v] == 0) == m_H.contains(v)); - } - - // m_S are values such that hscore = 0, sscore > 0 - for (bool_var v = 0; v < m_sscore.size(); ++v) { - SASSERT((m_hscore[v] == 0 && m_sscore[v] > 0 && !m_tabu[v]) == m_S.contains(v)); - } + DEBUG_CODE( + for (unsigned v = 0; v < s.num_vars(); ++v) { + int hs = compute_hscore(v); + CTRACE("sat", hs != m_hscore[v], display(tout << v << " - computed: " << hs << " - assigned: " << m_hscore[v] << "\n");); + SASSERT(m_hscore[v] == hs); + } + + // The score(v) is the reward on soft clauses for flipping v. + for (unsigned j = 0; j < m_soft.size(); ++j) { + unsigned v = m_soft[j].var(); + double ss = (l_true == value_at(m_soft[j], m_model))?(-m_weights[j]):m_weights[j]; + SASSERT(m_sscore[v] == ss); + } + + // m_H are values such that m_hscore > 0 and sscore = 0. + for (bool_var v = 0; v < m_hscore.size(); ++v) { + SASSERT((m_hscore[v] > 0 && !m_tabu[v] && m_sscore[v] == 0) == m_H.contains(v)); + } + + // m_S are values such that hscore = 0, sscore > 0 + for (bool_var v = 0; v < m_sscore.size(); ++v) { + SASSERT((m_hscore[v] == 0 && m_sscore[v] > 0 && !m_tabu[v]) == m_S.contains(v)); + }); } void wsls::display(std::ostream& out) const { diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index f636c726b..78067238a 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -80,8 +80,7 @@ namespace sat { SASSERT(!src.was_eliminated(v)); bool ext = src.m_external[v] != 0; bool dvar = src.m_decision[v] != 0; - bool_var new_v = mk_var(ext, dvar); - SASSERT(v == new_v); + VERIFY(v == mk_var(ext, dvar)); } } { @@ -407,9 +406,8 @@ namespace sat { unsigned num_lits = cls.size(); for (unsigned i = 1; i < num_lits; i++) { literal l = cls[i]; - lbool val = value(l); - CTRACE("sat", val != l_false, tout << l << ":=" << val;); - SASSERT(val == l_false); + CTRACE("sat", value(l) != l_false, tout << l << ":=" << value(l);); + SASSERT(value(l) == l_false); if (max_false_idx == UINT_MAX || lvl(l) > lvl(cls[max_false_idx])) max_false_idx = i; } diff --git a/src/smt/smt_conflict_resolution.cpp b/src/smt/smt_conflict_resolution.cpp index 86593b0f2..e3c2be123 100644 --- a/src/smt/smt_conflict_resolution.cpp +++ b/src/smt/smt_conflict_resolution.cpp @@ -99,9 +99,10 @@ namespace smt { This method may update m_antecedents, m_todo_js and m_todo_eqs. */ void conflict_resolution::eq_justification2literals(enode * lhs, enode * rhs, eq_justification js) { - ast_manager& m = get_manager(); SASSERT(m_antecedents); - TRACE("conflict_detail", tout << mk_pp(lhs->get_owner(), m) << " = " << mk_pp(rhs->get_owner(), m); + TRACE("conflict_detail", + ast_manager& m = get_manager(); + tout << mk_pp(lhs->get_owner(), m) << " = " << mk_pp(rhs->get_owner(), m); switch (js.get_kind()) { case eq_justification::AXIOM: tout << " axiom\n"; break; case eq_justification::EQUATION: diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index 7d07f3997..07f4440ff 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -2259,6 +2259,7 @@ namespace smt { } unsigned ilvl = 0; + (void)ilvl; for (unsigned j = 0; j < num; j++) { expr * atom = cls->get_atom(j); bool sign = cls->get_atom_sign(j); @@ -2855,8 +2856,7 @@ namespace smt { propagate(); if (was_consistent && inconsistent()) { // logical context became inconsistent during user PUSH - bool res = resolve_conflict(); // build the proof - SASSERT(!res); + VERIFY(!resolve_conflict()); // build the proof } push_scope(); m_base_scopes.push_back(base_scope()); @@ -3110,8 +3110,7 @@ namespace smt { else { TRACE("after_internalization", display(tout);); if (inconsistent()) { - bool res = resolve_conflict(); // build the proof - SASSERT(!res); + VERIFY(!resolve_conflict()); // build the proof r = l_false; } else { @@ -3197,8 +3196,7 @@ namespace smt { init_assumptions(num_assumptions, assumptions); TRACE("after_internalization", display(tout);); if (inconsistent()) { - bool res = resolve_conflict(); // build the proof - SASSERT(!res); + VERIFY(!resolve_conflict()); // build the proof mk_unsat_core(); r = l_false; } diff --git a/src/smt/theory_arith_aux.h b/src/smt/theory_arith_aux.h index b4f887245..88676b4d9 100644 --- a/src/smt/theory_arith_aux.h +++ b/src/smt/theory_arith_aux.h @@ -1784,7 +1784,7 @@ namespace smt { template typename theory_arith::max_min_t theory_arith::max_min(theory_var v, bool max, bool maintain_integrality, bool& has_shared) { expr* e = get_enode(v)->get_owner(); - + (void)e; SASSERT(!maintain_integrality || valid_assignment()); SASSERT(satisfy_bounds()); SASSERT(!is_quasi_base(v)); diff --git a/src/smt/theory_array.cpp b/src/smt/theory_array.cpp index c60efe1b1..ef6b0e776 100644 --- a/src/smt/theory_array.cpp +++ b/src/smt/theory_array.cpp @@ -75,8 +75,7 @@ namespace smt { ast_manager& m = get_manager(); context& ctx = get_context(); theory_var r = theory_array_base::mk_var(n); - theory_var r2 = m_find.mk_var(); - SASSERT(r == r2); + VERIFY(r == m_find.mk_var()); SASSERT(r == static_cast(m_var_data.size())); m_var_data.push_back(alloc(var_data)); var_data * d = m_var_data[r]; diff --git a/src/smt/theory_bv.cpp b/src/smt/theory_bv.cpp index 3d6e341fa..2945c8c93 100644 --- a/src/smt/theory_bv.cpp +++ b/src/smt/theory_bv.cpp @@ -457,8 +457,7 @@ namespace smt { void theory_bv::fixed_var_eh(theory_var v) { numeral val; - bool r = get_fixed_value(v, val); - SASSERT(r); + VERIFY(get_fixed_value(v, val)); unsigned sz = get_bv_size(v); value_sort_pair key(val, sz); theory_var v2; @@ -554,9 +553,8 @@ namespace smt { void theory_bv::internalize_bv2int(app* n) { SASSERT(!get_context().e_internalized(n)); - ast_manager & m = get_manager(); context& ctx = get_context(); - TRACE("bv", tout << mk_bounded_pp(n, m) << "\n";); + TRACE("bv", tout << mk_bounded_pp(n, get_manager()) << "\n";); process_args(n); mk_enode(n); if (!ctx.relevancy()) { @@ -1142,9 +1140,8 @@ namespace smt { } void theory_bv::assign_eh(bool_var v, bool is_true) { - context & ctx = get_context(); atom * a = get_bv2a(v); - TRACE("bv", tout << "assert: v" << v << " #" << ctx.bool_var2expr(v)->get_id() << " is_true: " << is_true << "\n";); + TRACE("bv", tout << "assert: v" << v << " #" << get_context().bool_var2expr(v)->get_id() << " is_true: " << is_true << "\n";); if (a->is_bit()) { // The following optimization is not correct. // Boolean variables created for performing bit-blasting are reused. diff --git a/src/smt/theory_datatype.cpp b/src/smt/theory_datatype.cpp index 02b8f9514..e5c8b1313 100644 --- a/src/smt/theory_datatype.cpp +++ b/src/smt/theory_datatype.cpp @@ -198,8 +198,7 @@ namespace smt { theory_var theory_datatype::mk_var(enode * n) { theory_var r = theory::mk_var(n); - theory_var r2 = m_find.mk_var(); - SASSERT(r == r2); + VERIFY(r == m_find.mk_var()); SASSERT(r == static_cast(m_var_data.size())); m_var_data.push_back(alloc(var_data)); var_data * d = m_var_data[r]; diff --git a/src/smt/theory_diff_logic_def.h b/src/smt/theory_diff_logic_def.h index cca78e9c0..98f94c6d2 100644 --- a/src/smt/theory_diff_logic_def.h +++ b/src/smt/theory_diff_logic_def.h @@ -273,8 +273,7 @@ bool theory_diff_logic::internalize_atom(app * n, bool gate_ctx) { template void theory_diff_logic::internalize_eq_eh(app * atom, bool_var v) { context & ctx = get_context(); - ast_manager& m = get_manager(); - TRACE("arith", tout << mk_pp(atom, m) << "\n";); + TRACE("arith", tout << mk_pp(atom, get_manager()) << "\n";); app * lhs = to_app(atom->get_arg(0)); app * rhs = to_app(atom->get_arg(1)); app * s; @@ -606,7 +605,6 @@ void theory_diff_logic::new_edge(dl_var src, dl_var dst, unsigned num_edges atom* a = 0; m_bool_var2atom.find(bv, a); SASSERT(a); - edge_id e_id = a->get_pos(); literal_vector lits; for (unsigned i = 0; i < num_edges; ++i) { @@ -616,7 +614,7 @@ void theory_diff_logic::new_edge(dl_var src, dl_var dst, unsigned num_edges TRACE("dl_activity", tout << mk_pp(le, get_manager()) << "\n"; - tout << "edge: " << e_id << "\n"; + tout << "edge: " << a->get_pos() << "\n"; ctx.display_literals_verbose(tout, lits.size(), lits.c_ptr()); tout << "\n"; ); @@ -927,18 +925,19 @@ void theory_diff_logic::display(std::ostream & out) const { template bool theory_diff_logic::is_consistent() const { - context& ctx = get_context(); - for (unsigned i = 0; i < m_atoms.size(); ++i) { - atom* a = m_atoms[i]; - bool_var bv = a->get_bool_var(); - lbool asgn = ctx.get_assignment(bv); - if (ctx.is_relevant(ctx.bool_var2expr(bv)) && asgn != l_undef) { - SASSERT((asgn == l_true) == a->is_true()); - int edge_id = a->get_asserted_edge(); - SASSERT(m_graph.is_enabled(edge_id)); - SASSERT(m_graph.is_feasible(edge_id)); - } - } + DEBUG_CODE( + context& ctx = get_context(); + for (unsigned i = 0; i < m_atoms.size(); ++i) { + atom* a = m_atoms[i]; + bool_var bv = a->get_bool_var(); + lbool asgn = ctx.get_assignment(bv); + if (ctx.is_relevant(ctx.bool_var2expr(bv)) && asgn != l_undef) { + SASSERT((asgn == l_true) == a->is_true()); + int edge_id = a->get_asserted_edge(); + SASSERT(m_graph.is_enabled(edge_id)); + SASSERT(m_graph.is_feasible(edge_id)); + } + }); return m_graph.is_feasible(); } @@ -1194,9 +1193,9 @@ theory_diff_logic::maximize(theory_var v, expr_ref& blocker, bool& has_shar ast_manager& m = get_manager(); update_simplex(S); - objective_term const& objective = m_objectives[v]; TRACE("arith", + objective_term const& objective = m_objectives[v]; for (unsigned i = 0; i < objective.size(); ++i) { tout << "Coefficient " << objective[i].second << " of theory_var " << objective[i].first << "\n"; diff --git a/src/smt/theory_fpa.cpp b/src/smt/theory_fpa.cpp index 543b1348e..dfba7c170 100644 --- a/src/smt/theory_fpa.cpp +++ b/src/smt/theory_fpa.cpp @@ -52,9 +52,8 @@ namespace smt { expr_ref bv(m); bv = m_th.wrap(m.mk_const(f)); unsigned bv_sz = m_th.m_bv_util.get_bv_size(bv); - unsigned ebits = m_th.m_fpa_util.get_ebits(s); unsigned sbits = m_th.m_fpa_util.get_sbits(s); - SASSERT(bv_sz == ebits + sbits); + SASSERT(bv_sz == m_th.m_fpa_util.get_ebits(s) + sbits); m_th.m_converter.mk_fp(m_bv_util.mk_extract(bv_sz - 1, bv_sz - 1, bv), m_bv_util.mk_extract(bv_sz - 2, sbits - 1, bv), m_bv_util.mk_extract(sbits - 2, 0, bv), @@ -231,10 +230,11 @@ namespace smt { } app * theory_fpa::fpa_value_proc::mk_value(model_generator & mg, ptr_vector & values) { - ast_manager & m = m_th.get_manager(); - TRACE("t_fpa_detail", for (unsigned i = 0; i < values.size(); i++) - tout << "value[" << i << "] = " << mk_ismt2_pp(values[i], m) << std::endl;); + TRACE("t_fpa_detail", + ast_manager & m = m_th.get_manager(); + for (unsigned i = 0; i < values.size(); i++) + tout << "value[" << i << "] = " << mk_ismt2_pp(values[i], m) << std::endl;); mpf_manager & mpfm = m_fu.fm(); unsynch_mpz_manager & mpzm = mpfm.mpz_manager(); @@ -254,8 +254,7 @@ namespace smt { rational all_r(0); scoped_mpz all_z(mpzm); - bool r = m_bu.is_numeral(values[0], all_r, bv_sz); - SASSERT(r); + VERIFY(m_bu.is_numeral(values[0], all_r, bv_sz)); SASSERT(bv_sz == (m_ebits + m_sbits)); SASSERT(all_r.is_int()); mpzm.set(all_z, all_r.to_mpq().numerator()); @@ -316,8 +315,7 @@ namespace smt { unsigned bv_sz; rational val(0); - bool r = m_bu.is_numeral(values[0], val, bv_sz); - SASSERT(r); + VERIFY(m_bu.is_numeral(values[0], val, bv_sz)); SASSERT(bv_sz == 3); switch (val.get_uint64()) @@ -422,9 +420,8 @@ namespace smt { expr_ref bv(m); bv = wrap(e_conv); unsigned bv_sz = m_bv_util.get_bv_size(bv); - unsigned ebits = m_fpa_util.get_ebits(m.get_sort(e_conv)); unsigned sbits = m_fpa_util.get_sbits(m.get_sort(e_conv)); - SASSERT(bv_sz == ebits + sbits); + SASSERT(bv_sz == m_fpa_util.get_ebits(m.get_sort(e_conv)) + sbits); m_converter.mk_fp(m_bv_util.mk_extract(bv_sz - 1, bv_sz - 1, bv), m_bv_util.mk_extract(bv_sz - 2, sbits - 1, bv), m_bv_util.mk_extract(sbits - 2, 0, bv), diff --git a/src/smt/theory_wmaxsat.cpp b/src/smt/theory_wmaxsat.cpp index 9ed944d2c..e52475d06 100644 --- a/src/smt/theory_wmaxsat.cpp +++ b/src/smt/theory_wmaxsat.cpp @@ -260,7 +260,6 @@ void theory_wmaxsat::block() { return; } ++m_stats.m_num_blocks; - ast_manager& m = get_manager(); context& ctx = get_context(); literal_vector lits; compare_cost compare_cost(*this); @@ -274,6 +273,7 @@ void theory_wmaxsat::block() { lits.push_back(~literal(m_var2bool[costs[i]])); } TRACE("opt", + ast_manager& m = get_manager(); tout << "block: "; for (unsigned i = 0; i < lits.size(); ++i) { expr_ref tmp(m); diff --git a/src/util/mpf.cpp b/src/util/mpf.cpp index e84298231..0fcff0da0 100644 --- a/src/util/mpf.cpp +++ b/src/util/mpf.cpp @@ -1092,6 +1092,7 @@ void mpf_manager::round_to_integral(mpf_rounding_mode rm, mpf const & x, mpf & o bool tie = m_mpz_manager.eq(rem, shiftm1_p); bool less_than_tie = m_mpz_manager.lt(rem, shiftm1_p); bool more_than_tie = m_mpz_manager.gt(rem, shiftm1_p); + (void)less_than_tie; TRACE("mpf_dbg", tout << "tie= " << tie << "; tie = " << more_than_tie << std::endl;); if (tie) { if ((rm == MPF_ROUND_NEAREST_TEVEN && m_mpz_manager.is_odd(div)) || @@ -1888,6 +1889,7 @@ void mpf_manager::round(mpf_rounding_mode rm, mpf & o) { const mpz & p_m1 = m_powers2(o.sbits+2); const mpz & p_m2 = m_powers2(o.sbits+3); + (void)p_m1; TRACE("mpf_dbg", tout << "p_m1 = " << m_mpz_manager.to_string(p_m1) << std::endl << "p_m2 = " << m_mpz_manager.to_string(p_m2) << std::endl;); @@ -2079,7 +2081,7 @@ void mpf_manager::round_sqrt(mpf_rounding_mode rm, mpf & o) { bool round = !m_mpz_manager.is_even(o.significand); m_mpz_manager.machine_div2k(o.significand, 1); bool last = !m_mpz_manager.is_even(o.significand); - + (void)last; bool inc = false; // Specialized rounding for sqrt, as there are no negative cases (or half-way cases?) diff --git a/src/util/mpff.cpp b/src/util/mpff.cpp index e5d3cf24c..d26b3743c 100644 --- a/src/util/mpff.cpp +++ b/src/util/mpff.cpp @@ -1395,6 +1395,7 @@ unsigned mpff_manager::prev_power_of_two(mpff const & a) { bool mpff_manager::check(mpff const & n) const { // n is zero or the most significand bit of the most significand word is 1. unsigned * s = sig(n); + (void)s; SASSERT(is_zero(n) || (s[m_precision - 1] & MIN_MSW) != 0); // if n is zero, then the sign must be 0 SASSERT(!is_zero(n) || n.m_sign == 0); From 40f8e16273a4fd8f11f1f64c342e00f33773f87c Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 17 May 2016 14:00:30 -0700 Subject: [PATCH 2/4] removing warnings for unused variables, #579 Signed-off-by: Nikolaj Bjorner --- src/math/simplex/sparse_matrix_def.h | 9 +++++---- src/qe/qe.cpp | 5 +++-- src/smt/theory_fpa.cpp | 5 +++-- src/smt/theory_pb.cpp | 10 ++++------ 4 files changed, 15 insertions(+), 14 deletions(-) diff --git a/src/math/simplex/sparse_matrix_def.h b/src/math/simplex/sparse_matrix_def.h index 78a4e8301..b050e45e1 100644 --- a/src/math/simplex/sparse_matrix_def.h +++ b/src/math/simplex/sparse_matrix_def.h @@ -542,10 +542,11 @@ namespace simplex { continue; } SASSERT(!rows.contains(c.m_row_id)); - _row const& row = m_rows[c.m_row_id]; - _row_entry const& r = row.m_entries[c.m_row_idx]; - SASSERT(r.m_var == v); - SASSERT((unsigned)r.m_col_idx == i); + DEBUG_CODE( + _row const& row = m_rows[c.m_row_id]; + _row_entry const& r = row.m_entries[c.m_row_idx]; + SASSERT(r.m_var == v); + SASSERT((unsigned)r.m_col_idx == i);); rows.insert(c.m_row_id); } int idx = col.m_first_free_idx; diff --git a/src/qe/qe.cpp b/src/qe/qe.cpp index 9742d2051..721e38942 100644 --- a/src/qe/qe.cpp +++ b/src/qe/qe.cpp @@ -861,11 +861,12 @@ namespace qe { void operator()(expr_ref& fml, atom_set& pos, atom_set& neg) { expr_ref orig(fml); - ast_manager& m = fml.get_manager(); m_nnf_core(fml); m_normalize_literals(fml); m_collect_atoms(fml, pos, neg); - TRACE("qe", tout << mk_ismt2_pp(orig, m) << "\n-->\n" << mk_ismt2_pp(fml, m) << "\n";); + TRACE("qe", + ast_manager& m = fml.get_manager(); + tout << mk_ismt2_pp(orig, m) << "\n-->\n" << mk_ismt2_pp(fml, m) << "\n";); } void reset() { diff --git a/src/smt/theory_fpa.cpp b/src/smt/theory_fpa.cpp index dfba7c170..59bcf40e8 100644 --- a/src/smt/theory_fpa.cpp +++ b/src/smt/theory_fpa.cpp @@ -306,9 +306,10 @@ namespace smt { app * theory_fpa::fpa_rm_value_proc::mk_value(model_generator & mg, ptr_vector & values) { SASSERT(values.size() == 1); - ast_manager & m = m_th.get_manager(); - TRACE("t_fpa_detail", for (unsigned i = 0; i < values.size(); i++) + TRACE("t_fpa_detail", + ast_manager & m = m_th.get_manager(); + for (unsigned i = 0; i < values.size(); i++) tout << "value[" << i << "] = " << mk_ismt2_pp(values[i], m) << std::endl;); app * result = 0; diff --git a/src/smt/theory_pb.cpp b/src/smt/theory_pb.cpp index a1aebf3e1..273bffd93 100644 --- a/src/smt/theory_pb.cpp +++ b/src/smt/theory_pb.cpp @@ -787,8 +787,7 @@ namespace smt { } for (unsigned i = 0; i < ineqs->size(); ++i) { - ineq* c = (*ineqs)[i]; - SASSERT(c->is_ge()); + SASSERT((*ineqs)[i]->is_ge()); if (assign_watch_ge(v, is_true, *ineqs, i)) { // i was removed from watch list. --i; @@ -1834,13 +1833,12 @@ namespace smt { void theory_pb::validate_assign(ineq const& c, literal_vector const& lits, literal l) const { uint_set nlits; - context& ctx = get_context(); for (unsigned i = 0; i < lits.size(); ++i) { - SASSERT(ctx.get_assignment(lits[i]) == l_true); + SASSERT(get_context().get_assignment(lits[i]) == l_true); nlits.insert((~lits[i]).index()); } - SASSERT(ctx.get_assignment(l) == l_undef); - SASSERT(ctx.get_assignment(c.lit()) == l_true); + SASSERT(get_context().get_assignment(l) == l_undef); + SASSERT(get_context().get_assignment(c.lit()) == l_true); nlits.insert(l.index()); numeral sum = numeral::zero(); for (unsigned i = 0; i < c.size(); ++i) { From 09b8c0e7fa4804b24bc776825b323ab970045ecd Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 17 May 2016 15:59:06 -0700 Subject: [PATCH 3/4] removing warnings for unused variables, #579 Signed-off-by: Nikolaj Bjorner --- src/ast/seq_decl_plugin.cpp | 5 ++--- src/cmd_context/cmd_context_to_goal.cpp | 3 +-- src/sat/sat_bceq.cpp | 9 +++++---- src/sat/sat_clause_set.cpp | 3 ++- src/smt/qi_queue.cpp | 9 +++------ src/smt/smt_model_finder.cpp | 26 ++++++++++++------------- src/smt/theory_seq.cpp | 6 ++---- 7 files changed, 27 insertions(+), 34 deletions(-) diff --git a/src/ast/seq_decl_plugin.cpp b/src/ast/seq_decl_plugin.cpp index 708da5602..21af0773a 100644 --- a/src/ast/seq_decl_plugin.cpp +++ b/src/ast/seq_decl_plugin.cpp @@ -277,13 +277,12 @@ bool seq_decl_plugin::is_sort_param(sort* s, unsigned& idx) { } bool seq_decl_plugin::match(ptr_vector& binding, sort* s, sort* sP) { - ast_manager& m = *m_manager; if (s == sP) return true; unsigned i; if (is_sort_param(sP, i)) { if (binding.size() <= i) binding.resize(i+1); if (binding[i] && (binding[i] != s)) return false; - TRACE("seq_verbose", tout << "setting binding @ " << i << " to " << mk_pp(s, m) << "\n";); + TRACE("seq_verbose", tout << "setting binding @ " << i << " to " << mk_pp(s, *m_manager) << "\n";); binding[i] = s; return true; } @@ -302,7 +301,7 @@ bool seq_decl_plugin::match(ptr_vector& binding, sort* s, sort* sP) { return true; } else { - TRACE("seq", tout << "Could not match " << mk_pp(s, m) << " and " << mk_pp(sP, m) << "\n";); + TRACE("seq", tout << "Could not match " << mk_pp(s, *m_manager) << " and " << mk_pp(sP, *m_manager) << "\n";); return false; } } diff --git a/src/cmd_context/cmd_context_to_goal.cpp b/src/cmd_context/cmd_context_to_goal.cpp index 26cb2766b..c0b4379aa 100644 --- a/src/cmd_context/cmd_context_to_goal.cpp +++ b/src/cmd_context/cmd_context_to_goal.cpp @@ -31,8 +31,7 @@ void assert_exprs_from(cmd_context const & ctx, goal & t) { ptr_vector::const_iterator it = ctx.begin_assertions(); ptr_vector::const_iterator end = ctx.end_assertions(); ptr_vector::const_iterator it2 = ctx.begin_assertion_names(); - ptr_vector::const_iterator end2 = ctx.end_assertion_names(); - SASSERT(end - it == end2 - it2); + SASSERT(end - it == ctx.end_assertion_names() - it2); for (; it != end; ++it, ++it2) { t.assert_expr(*it, proofs_enabled ? m.mk_asserted(*it) : 0, m.mk_leaf(*it2)); } diff --git a/src/sat/sat_bceq.cpp b/src/sat/sat_bceq.cpp index a194cdfd8..9ff286aaa 100644 --- a/src/sat/sat_bceq.cpp +++ b/src/sat/sat_bceq.cpp @@ -345,10 +345,11 @@ namespace sat { } void bceq::verify_sweep() { - for (unsigned i = 0; i < m_L.size(); ++i) { - uint64 b = eval_clause(*m_L[i]); - SASSERT((~b) == 0); - } + DEBUG_CODE( + for (unsigned i = 0; i < m_L.size(); ++i) { + uint64 b = eval_clause(*m_L[i]); + SASSERT((~b) == 0); + }); } struct u64_hash { unsigned operator()(uint64 u) const { return (unsigned)u; } }; diff --git a/src/sat/sat_clause_set.cpp b/src/sat/sat_clause_set.cpp index 29c761130..1c424cce3 100644 --- a/src/sat/sat_clause_set.cpp +++ b/src/sat/sat_clause_set.cpp @@ -64,6 +64,7 @@ namespace sat { } bool clause_set::check_invariant() const { + DEBUG_CODE( { clause_vector::const_iterator it = m_set.begin(); clause_vector::const_iterator end = m_set.end(); @@ -83,7 +84,7 @@ namespace sat { SASSERT(pos < m_set.size()); SASSERT(m_set[pos]->id() == id); } - } + }); return true; } diff --git a/src/smt/qi_queue.cpp b/src/smt/qi_queue.cpp index 35dd19087..f9413be72 100644 --- a/src/smt/qi_queue.cpp +++ b/src/smt/qi_queue.cpp @@ -367,8 +367,7 @@ namespace smt { unsigned sz = m_delayed_entries.size(); for (unsigned i = 0; i < sz; i++) { entry & e = m_delayed_entries[i]; - fingerprint * f = e.m_qb; - TRACE("qi_queue", tout << f << ", cost: " << e.m_cost << ", instantiated: " << e.m_instantiated << "\n";); + TRACE("qi_queue", tout << e.m_qb << ", cost: " << e.m_cost << ", instantiated: " << e.m_instantiated << "\n";); if (!e.m_instantiated && e.m_cost <= m_params.m_qi_lazy_threshold && (!init || e.m_cost < min_cost)) { init = true; min_cost = e.m_cost; @@ -379,11 +378,10 @@ namespace smt { for (unsigned i = 0; i < sz; i++) { entry & e = m_delayed_entries[i]; fingerprint * f = e.m_qb; - quantifier * qa = static_cast(f->get_data()); TRACE("qi_queue", tout << f << ", cost: " << e.m_cost << ", instantiated: " << e.m_instantiated << "\n";); if (!e.m_instantiated && e.m_cost <= min_cost) { TRACE("qi_queue", - tout << "lazy quantifier instantiation...\n" << mk_pp(qa, m_manager) << "\ncost: " << e.m_cost << "\n";); + tout << "lazy quantifier instantiation...\n" << mk_pp(static_cast(f->get_data()), m_manager) << "\ncost: " << e.m_cost << "\n";); result = false; m_instantiated_trail.push_back(i); m_stats.m_num_lazy_instances++; @@ -397,11 +395,10 @@ namespace smt { for (unsigned i = 0; i < m_delayed_entries.size(); i++) { entry & e = m_delayed_entries[i]; fingerprint * f = e.m_qb; - quantifier * qa = static_cast(f->get_data()); TRACE("qi_queue", tout << f << ", cost: " << e.m_cost << ", instantiated: " << e.m_instantiated << "\n";); if (!e.m_instantiated && e.m_cost <= m_params.m_qi_lazy_threshold) { TRACE("qi_queue", - tout << "lazy quantifier instantiation...\n" << mk_pp(qa, m_manager) << "\ncost: " << e.m_cost << "\n";); + tout << "lazy quantifier instantiation...\n" << mk_pp(static_cast(f->get_data()), m_manager) << "\ncost: " << e.m_cost << "\n";); result = false; m_instantiated_trail.push_back(i); m_stats.m_num_lazy_instances++; diff --git a/src/smt/smt_model_finder.cpp b/src/smt/smt_model_finder.cpp index 1f8f6dabe..1f4f26b06 100644 --- a/src/smt/smt_model_finder.cpp +++ b/src/smt/smt_model_finder.cpp @@ -2899,15 +2899,16 @@ namespace smt { } bool check_satisfied_residue_invariant() { - qsset::iterator it = m_satisfied.begin(); - qsset::iterator end = m_satisfied.end(); - for (; it != end; ++it) { - quantifier * q = *it; - SASSERT(!m_residue.contains(q)); - quantifier_info * qi = get_qinfo(q); - SASSERT(qi != 0); - SASSERT(qi->get_the_one() != 0); - } + DEBUG_CODE( + qsset::iterator it = m_satisfied.begin(); + qsset::iterator end = m_satisfied.end(); + for (; it != end; ++it) { + quantifier * q = *it; + SASSERT(!m_residue.contains(q)); + quantifier_info * qi = get_qinfo(q); + SASSERT(qi != 0); + SASSERT(qi->get_the_one() != 0); + }); return true; } @@ -3546,12 +3547,9 @@ namespace smt { bool asserted_something = false; quantifier * flat_q = get_flat_quantifier(q); unsigned num_decls = q->get_num_decls(); - unsigned flat_num_decls = flat_q->get_num_decls(); - unsigned num_sks = sks.size(); // Remark: sks were created for the flat version of q. - SASSERT(num_sks == flat_num_decls); - SASSERT(flat_num_decls >= num_decls); - SASSERT(num_sks >= num_decls); + SASSERT(flat_q->get_num_decls() == sks.size()); + SASSERT(sks.size() >= num_decls); for (unsigned i = 0; i < num_decls; i++) { expr * sk = sks.get(num_decls - i - 1); instantiation_set const * s = get_uvar_inst_set(q, i); diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index 72d8929b8..f2bd8be84 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -3244,8 +3244,7 @@ void theory_seq::add_at_axiom(expr* e) { step(s, idx, re, i, j, t) -> nth(s, idx) == t & len(s) > idx */ void theory_seq::propagate_step(literal lit, expr* step) { - context& ctx = get_context(); - SASSERT(ctx.get_assignment(lit) == l_true); + SASSERT(get_context().get_assignment(lit) == l_true); expr* re, *acc, *s, *idx, *i, *j; VERIFY(is_step(step, s, idx, re, i, j, acc)); TRACE("seq", tout << mk_pp(step, m) << " -> " << mk_pp(acc, m) << "\n";); @@ -3265,9 +3264,8 @@ void theory_seq::propagate_step(literal lit, expr* step) { lit => s = (nth s 0) ++ (nth s 1) ++ ... ++ (nth s idx) ++ (tail s idx) */ void theory_seq::ensure_nth(literal lit, expr* s, expr* idx) { - context& ctx = get_context(); rational r; - SASSERT(ctx.get_assignment(lit) == l_true); + SASSERT(get_context().get_assignment(lit) == l_true); VERIFY(m_autil.is_numeral(idx, r) && r.is_unsigned()); unsigned _idx = r.get_unsigned(); expr_ref head(m), tail(m), conc(m), len1(m), len2(m); From cc3bfe8da22e53ba74dbec25f04c2fb32db10ea4 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 17 May 2016 16:02:08 -0700 Subject: [PATCH 4/4] removing warnings for unused variables, #579 Signed-off-by: Nikolaj Bjorner --- src/smt/qi_queue.cpp | 10 ++++------ src/smt/smt_model_finder.cpp | 3 +-- src/smt/theory_seq.cpp | 3 +-- 3 files changed, 6 insertions(+), 10 deletions(-) diff --git a/src/smt/qi_queue.cpp b/src/smt/qi_queue.cpp index f9413be72..711cdc336 100644 --- a/src/smt/qi_queue.cpp +++ b/src/smt/qi_queue.cpp @@ -377,11 +377,10 @@ namespace smt { bool result = true; for (unsigned i = 0; i < sz; i++) { entry & e = m_delayed_entries[i]; - fingerprint * f = e.m_qb; - TRACE("qi_queue", tout << f << ", cost: " << e.m_cost << ", instantiated: " << e.m_instantiated << "\n";); + TRACE("qi_queue", tout << e.m_qb << ", cost: " << e.m_cost << ", instantiated: " << e.m_instantiated << "\n";); if (!e.m_instantiated && e.m_cost <= min_cost) { TRACE("qi_queue", - tout << "lazy quantifier instantiation...\n" << mk_pp(static_cast(f->get_data()), m_manager) << "\ncost: " << e.m_cost << "\n";); + tout << "lazy quantifier instantiation...\n" << mk_pp(static_cast(e.m_qb->get_data()), m_manager) << "\ncost: " << e.m_cost << "\n";); result = false; m_instantiated_trail.push_back(i); m_stats.m_num_lazy_instances++; @@ -394,11 +393,10 @@ namespace smt { bool result = true; for (unsigned i = 0; i < m_delayed_entries.size(); i++) { entry & e = m_delayed_entries[i]; - fingerprint * f = e.m_qb; - TRACE("qi_queue", tout << f << ", cost: " << e.m_cost << ", instantiated: " << e.m_instantiated << "\n";); + TRACE("qi_queue", tout << e.m_qb << ", cost: " << e.m_cost << ", instantiated: " << e.m_instantiated << "\n";); if (!e.m_instantiated && e.m_cost <= m_params.m_qi_lazy_threshold) { TRACE("qi_queue", - tout << "lazy quantifier instantiation...\n" << mk_pp(static_cast(f->get_data()), m_manager) << "\ncost: " << e.m_cost << "\n";); + tout << "lazy quantifier instantiation...\n" << mk_pp(static_cast(e.m_qb->get_data()), m_manager) << "\ncost: " << e.m_cost << "\n";); result = false; m_instantiated_trail.push_back(i); m_stats.m_num_lazy_instances++; diff --git a/src/smt/smt_model_finder.cpp b/src/smt/smt_model_finder.cpp index 1f4f26b06..5dc0dd8ec 100644 --- a/src/smt/smt_model_finder.cpp +++ b/src/smt/smt_model_finder.cpp @@ -3545,10 +3545,9 @@ namespace smt { // // Since we only care about q (and its bindings), it only makes sense to restrict the variables of q. bool asserted_something = false; - quantifier * flat_q = get_flat_quantifier(q); unsigned num_decls = q->get_num_decls(); // Remark: sks were created for the flat version of q. - SASSERT(flat_q->get_num_decls() == sks.size()); + SASSERT(get_flat_quantifier(q)->get_num_decls() == sks.size()); SASSERT(sks.size() >= num_decls); for (unsigned i = 0; i < num_decls; i++) { expr * sk = sks.get(num_decls - i - 1); diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index f2bd8be84..97189ce4c 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -3741,7 +3741,6 @@ expr_ref theory_seq::mk_step(expr* s, expr* idx, expr* re, unsigned i, unsigned rej(s, idx, re, i) -> len(s) > idx if i is final */ void theory_seq::propagate_acc_rej_length(literal lit, expr* e) { - context& ctx = get_context(); expr *s, * idx, *re; unsigned src; eautomaton* aut = 0; @@ -3752,7 +3751,7 @@ void theory_seq::propagate_acc_rej_length(literal lit, expr* e) { } if (m_util.str.is_length(idx)) return; SASSERT(m_autil.is_numeral(idx)); - SASSERT(ctx.get_assignment(lit) == l_true); + SASSERT(get_context().get_assignment(lit) == l_true); bool is_final = aut->is_final_state(src); if (is_final == is_acc) { propagate_lit(0, 1, &lit, mk_literal(m_autil.mk_ge(m_util.str.mk_length(s), idx)));