From b12882d94a52c2eb1e3c9b38c6285f725d96dad5 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 31 Jul 2017 21:56:13 -0700 Subject: [PATCH] a few more spacer related warning messages Signed-off-by: Nikolaj Bjorner --- src/muz/spacer/spacer_antiunify.cpp | 8 +-- src/muz/spacer/spacer_farkas_learner.cpp | 4 +- src/muz/spacer/spacer_generalizers.cpp | 5 +- src/muz/spacer/spacer_legacy_frames.cpp | 1 + src/muz/spacer/spacer_prop_solver.cpp | 1 + src/muz/spacer/spacer_qe_project.cpp | 3 +- src/muz/spacer/spacer_unsat_core_plugin.cpp | 76 +++++++++------------ 7 files changed, 44 insertions(+), 54 deletions(-) diff --git a/src/muz/spacer/spacer_antiunify.cpp b/src/muz/spacer/spacer_antiunify.cpp index 6c382a723..7dae59b6a 100644 --- a/src/muz/spacer/spacer_antiunify.cpp +++ b/src/muz/spacer/spacer_antiunify.cpp @@ -335,8 +335,8 @@ bool naive_convex_closure::compute_closure(anti_unifier& au, ast_manager& m, // for each substitution entry bool is_first_key = true; - unsigned lower_bound; - unsigned upper_bound; + unsigned lower_bound = 0; + unsigned upper_bound = 0; for (const auto& pair : au.get_substitution(0)) { // construct vector expr* key = &pair.get_key(); @@ -355,8 +355,8 @@ bool naive_convex_closure::compute_closure(anti_unifier& au, ast_manager& m, } // check whether vector represents interval - unsigned current_lower_bound; - unsigned current_upper_bound; + unsigned current_lower_bound = 0; + unsigned current_upper_bound = 0; // if vector represents interval if (get_range(entries, current_lower_bound, current_upper_bound)) { diff --git a/src/muz/spacer/spacer_farkas_learner.cpp b/src/muz/spacer/spacer_farkas_learner.cpp index 29d238cc9..47bc474ef 100644 --- a/src/muz/spacer/spacer_farkas_learner.cpp +++ b/src/muz/spacer/spacer_farkas_learner.cpp @@ -389,11 +389,11 @@ void farkas_learner::get_lemmas(proof* root, expr_set const& bs, expr_ref_vector simplify_bounds(lemmas); } -void farkas_learner::get_asserted(proof* p, expr_set const& bs, ast_mark& b_closed, obj_hashtable& lemma_set, expr_ref_vector& lemmas) +void farkas_learner::get_asserted(proof* p0, expr_set const& bs, ast_mark& b_closed, obj_hashtable& lemma_set, expr_ref_vector& lemmas) { ast_manager& m = lemmas.get_manager(); ast_mark visited; - proof* p0 = p; + proof* p = p0; ptr_vector todo; todo.push_back(p); diff --git a/src/muz/spacer/spacer_generalizers.cpp b/src/muz/spacer/spacer_generalizers.cpp index 9f8757024..40e5c2c4d 100644 --- a/src/muz/spacer/spacer_generalizers.cpp +++ b/src/muz/spacer/spacer_generalizers.cpp @@ -133,9 +133,7 @@ void unsat_core_generalizer::operator()(lemma_ref &lemma) unsigned uses_level; expr_ref_vector core(m); - bool r; - r = pt.is_invariant(lemma->level(), lemma->get_expr(), uses_level, &core); - SASSERT(r); + VERIFY(pt.is_invariant(lemma->level(), lemma->get_expr(), uses_level, &core)); CTRACE("spacer", old_sz > core.size(), tout << "unsat core reduced lemma from: " @@ -185,6 +183,7 @@ void lemma_array_eq_generalizer::operator() (lemma_ref &lemma) // -- find array constants ast_manager &m = lemma->get_ast_manager(); manager &pm = m_ctx.get_manager(); + (void)pm; expr_ref_vector core(m); expr_ref v(m); diff --git a/src/muz/spacer/spacer_legacy_frames.cpp b/src/muz/spacer/spacer_legacy_frames.cpp index 77e6f5650..6c732ecc0 100644 --- a/src/muz/spacer/spacer_legacy_frames.cpp +++ b/src/muz/spacer/spacer_legacy_frames.cpp @@ -79,6 +79,7 @@ bool pred_transformer::legacy_frames::propagate_to_next_level(unsigned src_level { ast_manager &m = m_pt.get_ast_manager(); + (void) m; if (m_levels.size() <= src_level) { return true; } if (m_levels [src_level].empty()) { return true; } diff --git a/src/muz/spacer/spacer_prop_solver.cpp b/src/muz/spacer/spacer_prop_solver.cpp index 27225315c..719443457 100644 --- a/src/muz/spacer/spacer_prop_solver.cpp +++ b/src/muz/spacer/spacer_prop_solver.cpp @@ -264,6 +264,7 @@ lbool prop_solver::check_assumptions(const expr_ref_vector & _hard, else { m_ctx->assert_expr(bg[i]); } unsigned soft_sz = soft.size(); + (void) soft_sz; lbool res = internal_check_assumptions(hard, soft); if (!m_use_push_bg) { m_ctx->pop(1); } diff --git a/src/muz/spacer/spacer_qe_project.cpp b/src/muz/spacer/spacer_qe_project.cpp index 62c9c2643..c06854cb0 100644 --- a/src/muz/spacer/spacer_qe_project.cpp +++ b/src/muz/spacer/spacer_qe_project.cpp @@ -788,7 +788,7 @@ namespace qe { } unsigned find_max(model& mdl, bool do_pos) { - unsigned result; + unsigned result = UINT_MAX; bool found = false; bool found_strict = false; rational found_val (0), r, r_plus_x, found_c; @@ -2078,6 +2078,7 @@ namespace qe { sort* v_sort = m.get_sort (v); sort* val_sort = get_array_range (v_sort); sort* idx_sort = get_array_domain (v_sort, 0); + (void) idx_sort; unsigned start = m_idx_reprs.size (); // append at the end diff --git a/src/muz/spacer/spacer_unsat_core_plugin.cpp b/src/muz/spacer/spacer_unsat_core_plugin.cpp index a352a2460..66abb32c6 100644 --- a/src/muz/spacer/spacer_unsat_core_plugin.cpp +++ b/src/muz/spacer/spacer_unsat_core_plugin.cpp @@ -444,10 +444,10 @@ void unsat_core_plugin_farkas_lemma::compute_linear_combination(const vector 0); @@ -457,12 +457,9 @@ void unsat_core_plugin_farkas_lemma::compute_linear_combination(const vector ordered_basis; obj_map map; unsigned counter = 0; - for (const auto& linear_combination : m_linear_combinations) - { - for (const auto& pair : linear_combination) - { - if (!map.contains(pair.first)) - { + for (const auto& linear_combination : m_linear_combinations) { + for (const auto& pair : linear_combination) { + if (!map.contains(pair.first)) { ordered_basis.push_back(pair.first); map.insert(pair.first, counter++); } @@ -472,14 +469,12 @@ void unsat_core_plugin_farkas_lemma::compute_linear_combination(const vector coeffs; - for (unsigned i=0; i < matrix.num_rows(); ++i) - { + for (unsigned i=0; i < matrix.num_rows(); ++i) { coeffs.push_back(expr_ref_vector(m)); } @@ -532,19 +526,17 @@ void unsat_core_plugin_farkas_lemma::compute_linear_combination(const vectorassert_expr(lb); s->assert_expr(ub); - } } - + } + // assert: forall i,j: a_ij = sum_k w_ik * s_jk for (unsigned i=0; i < matrix.num_rows(); ++i) { @@ -568,34 +560,30 @@ void unsat_core_plugin_farkas_lemma::compute_linear_combination(const vectorcheck_sat(0,0); // if sat extract model and add corresponding linear combinations to core - if (res == lbool::l_true) - { + if (res == lbool::l_true) { model_ref model; s->get_model(model); - - for (int k=0; k < n; ++k) - { - ptr_vector literals; - vector coefficients; - for (unsigned j=0; j < matrix.num_cols(); ++j) - { + + for (unsigned k=0; k < n; ++k) { + ptr_vector literals; + vector coefficients; + for (unsigned j=0; j < matrix.num_cols(); ++j) { expr_ref evaluation(m); - + model.get()->eval(bounded_vectors[j][k].get(), evaluation, false); - if (!util.is_zero(evaluation)) - { + if (!util.is_zero(evaluation)) { literals.push_back(ordered_basis[j]); coefficients.push_back(rational(1)); - } - } + } + } SASSERT(!literals.empty()); // since then previous outer loop would have found solution already - expr_ref linear_combination(m); - compute_linear_combination(coefficients, literals, linear_combination); - - m_learner.add_lemma_to_core(linear_combination); - } + expr_ref linear_combination(m); + compute_linear_combination(coefficients, literals, linear_combination); + + m_learner.add_lemma_to_core(linear_combination); + } return; - } + } } }