From 09b8c0e7fa4804b24bc776825b323ab970045ecd Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 17 May 2016 15:59:06 -0700 Subject: [PATCH] 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);