From fc304618284ba31d2fd167bbc97377e0bfb108d5 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 20 Oct 2022 09:09:06 -0700 Subject: [PATCH] unused variables Signed-off-by: Nikolaj Bjorner --- src/cmd_context/extra_cmds/proof_cmds.cpp | 9 ++++----- src/math/simplex/model_based_opt.cpp | 2 +- src/muz/base/dl_rule_subsumption_index.h | 4 ++-- src/muz/spacer/spacer_cluster.cpp | 1 + src/muz/spacer/spacer_convex_closure.cpp | 1 + src/muz/spacer/spacer_sem_matcher.cpp | 2 +- src/muz/transforms/dl_mk_slice.cpp | 4 +++- src/sat/smt/euf_solver.cpp | 2 -- src/shell/drat_frontend.cpp | 1 - src/smt/theory_str.cpp | 4 ++-- src/test/dl_relation.cpp | 2 +- src/test/simplifier.cpp | 5 +++++ 12 files changed, 21 insertions(+), 16 deletions(-) diff --git a/src/cmd_context/extra_cmds/proof_cmds.cpp b/src/cmd_context/extra_cmds/proof_cmds.cpp index bf12157c1..9c9b9ed62 100644 --- a/src/cmd_context/extra_cmds/proof_cmds.cpp +++ b/src/cmd_context/extra_cmds/proof_cmds.cpp @@ -57,10 +57,9 @@ Proof checker for clauses created during search. * Replay proof entierly, then walk backwards extracting reduced proof. */ class proof_trim { - cmd_context& ctx; - ast_manager& m; - sat::proof_trim trim; - euf::theory_checker m_checker; + ast_manager& m; + sat::proof_trim trim; + euf::theory_checker m_checker; vector m_clauses; bool_vector m_is_infer; symbol m_rup; @@ -88,7 +87,7 @@ class proof_trim { public: proof_trim(cmd_context& ctx): - ctx(ctx), + // ctx(ctx), m(ctx.m()), trim(gparams::get_module("sat"), m.limit()), m_checker(m) { diff --git a/src/math/simplex/model_based_opt.cpp b/src/math/simplex/model_based_opt.cpp index 7ab246c6e..cb3a5be4d 100644 --- a/src/math/simplex/model_based_opt.cpp +++ b/src/math/simplex/model_based_opt.cpp @@ -116,7 +116,7 @@ namespace opt { model_based_opt::def model_based_opt::def::substitute(unsigned v, def const& other) const { def result; vector const& vs1 = m_vars; - vector const& vs2 = other.m_vars; + // vector const& vs2 = other.m_vars; rational coeff(0); for (auto const& [id, c] : vs1) { if (id == v) { diff --git a/src/muz/base/dl_rule_subsumption_index.h b/src/muz/base/dl_rule_subsumption_index.h index 9c29683b3..3783be3dc 100644 --- a/src/muz/base/dl_rule_subsumption_index.h +++ b/src/muz/base/dl_rule_subsumption_index.h @@ -29,7 +29,7 @@ namespace datalog { typedef obj_hashtable app_set; ast_manager & m; - context & m_context; + // context & m_context; rule_ref_vector m_ref_holder; @@ -42,7 +42,7 @@ namespace datalog { public: rule_subsumption_index(context & ctx) : m(ctx.get_manager()), - m_context(ctx), + // m_context(ctx), m_ref_holder(ctx.get_rule_manager()) {} ~rule_subsumption_index() { diff --git a/src/muz/spacer/spacer_cluster.cpp b/src/muz/spacer/spacer_cluster.cpp index 13ef17c26..b03562b12 100644 --- a/src/muz/spacer/spacer_cluster.cpp +++ b/src/muz/spacer/spacer_cluster.cpp @@ -381,6 +381,7 @@ void lemma_cluster_finder::cluster(lemma_ref &lemma) { for (const lemma_ref &l : neighbours) { SASSERT(cluster->can_contain(l)); bool added = cluster->add_lemma(l, false); + (void)added; CTRACE("cluster_stats", added, tout << "Added neighbour lemma\n" << mk_and(l->get_cube()) << "\n";); } diff --git a/src/muz/spacer/spacer_convex_closure.cpp b/src/muz/spacer/spacer_convex_closure.cpp index 476821643..2c11642c5 100644 --- a/src/muz/spacer/spacer_convex_closure.cpp +++ b/src/muz/spacer/spacer_convex_closure.cpp @@ -261,6 +261,7 @@ bool convex_closure::infer_div_pred(const vector &data, rational &m, }); SASSERT(data.size() > 1); SASSERT(is_sorted(data)); + (void)is_sorted; m = rational(2); diff --git a/src/muz/spacer/spacer_sem_matcher.cpp b/src/muz/spacer/spacer_sem_matcher.cpp index b0eeb51a3..8a79662a9 100644 --- a/src/muz/spacer/spacer_sem_matcher.cpp +++ b/src/muz/spacer/spacer_sem_matcher.cpp @@ -84,7 +84,7 @@ bool sem_matcher::operator()(expr * e1, expr * e2, substitution & s, bool &pos) top = false; if (n1->get_decl() != n2->get_decl()) { - expr *e1 = nullptr, *e2 = nullptr, *e3 = nullptr, *e4 = nullptr, *e5 = nullptr; + expr *e1 = nullptr, *e2 = nullptr; rational val1, val2; // x<=y == !(x>y) diff --git a/src/muz/transforms/dl_mk_slice.cpp b/src/muz/transforms/dl_mk_slice.cpp index 834bb41ef..25888cb68 100644 --- a/src/muz/transforms/dl_mk_slice.cpp +++ b/src/muz/transforms/dl_mk_slice.cpp @@ -260,7 +260,9 @@ namespace datalog { rm(ctx.get_rule_manager()), m_pinned_rules(rm), m_pinned_exprs(m), - m_unifier(ctx) {} + m_unifier(ctx) { + (void)m_ctx; + } void insert(rule* orig_rule, rule* slice_rule, unsigned sz, unsigned const* renaming) { m_rule2slice.insert(orig_rule, slice_rule); diff --git a/src/sat/smt/euf_solver.cpp b/src/sat/smt/euf_solver.cpp index 3d4af371f..5086dea98 100644 --- a/src/sat/smt/euf_solver.cpp +++ b/src/sat/smt/euf_solver.cpp @@ -232,7 +232,6 @@ namespace euf { auto* ext = sat::constraint_base::to_extension(idx); th_proof_hint* hint = nullptr; bool has_theory = false; - bool has_nested_theory = false; if (ext == this) get_antecedents(l, constraint::from_idx(idx), r, probing); else { @@ -250,7 +249,6 @@ namespace euf { sat::literal lit = sat::null_literal; ext->get_antecedents(lit, idx, r, probing); has_theory = true; - has_nested_theory = true; } } m_egraph.end_explain(); diff --git a/src/shell/drat_frontend.cpp b/src/shell/drat_frontend.cpp index b0b711ef0..7484684f2 100644 --- a/src/shell/drat_frontend.cpp +++ b/src/shell/drat_frontend.cpp @@ -18,7 +18,6 @@ Copyright (c) 2020 Microsoft Corporation class drup_checker { sat::drat& m_drat; sat::literal_vector m_units; - bool m_check_inputs = false; void add_units() { auto const& units = m_drat.units(); diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp index 955241efd..1e12f8bd3 100644 --- a/src/smt/theory_str.cpp +++ b/src/smt/theory_str.cpp @@ -2470,10 +2470,8 @@ namespace smt { TRACE("str", tout << "SKIP: both concats are already in the same equivalence class" << std::endl;); } else { expr_ref_vector items(m); - int pos = 0; for (auto itor : resolvedMap) { items.push_back(ctx.mk_eq_atom(itor.first, itor.second)); - pos += 1; } expr_ref premise(mk_and(items), m); expr_ref conclusion(ctx.mk_eq_atom(node, resultAst), m); @@ -4539,6 +4537,7 @@ namespace smt { and_item.push_back(ctx.mk_eq_atom(mk_strlen(m), m_autil.mk_add(mk_strlen(str1Ast), mk_strlen(commonVar)) )); pos += 1; + (void)pos; // addItems[0] = mk_length(t, commonVar); // addItems[1] = mk_length(t, str2Ast); @@ -6439,6 +6438,7 @@ namespace smt { expr_ref arg2_eq (ctx.mk_eq_atom(arg2, suffixAst), m); and_items.push_back(arg2_eq); and_count += 1; + (void) and_count; arrangement_disjunction.push_back(mk_and(and_items)); } diff --git a/src/test/dl_relation.cpp b/src/test/dl_relation.cpp index 9969ada2f..1646350f2 100644 --- a/src/test/dl_relation.cpp +++ b/src/test/dl_relation.cpp @@ -247,7 +247,7 @@ namespace datalog { { relation_base* b1 = br.mk_full(nullptr, sig); relation_base* b2 = br.mk_full(nullptr, sig); - unsigned x0x3[2] = { 0, 3 }; + // unsigned x0x3[2] = { 0, 3 }; unsigned x1x3[2] = { 1, 3 }; unsigned x2x3[2] = { 2, 3 }; scoped_ptr id1 = br.mk_filter_identical_fn(*b1, 2, x1x3); diff --git a/src/test/simplifier.cpp b/src/test/simplifier.cpp index d716a1268..7bfa72db8 100644 --- a/src/test/simplifier.cpp +++ b/src/test/simplifier.cpp @@ -93,6 +93,7 @@ static void test_datatypes() { int_list = Z3_mk_list_sort(ctx, Z3_mk_string_symbol(ctx, "int_list"), int_ty, &nil_decl, &is_nil_decl, &cons_decl, &is_cons_decl, &head_decl, &tail_decl); + (void) int_list; nil = Z3_mk_app(ctx, nil_decl, 0, nullptr); Z3_ast a = Z3_simplify(ctx, Z3_mk_app(ctx, is_nil_decl, 1, &nil)); @@ -166,6 +167,7 @@ static void test_array() { Z3_ast n4 = Z3_mk_numeral(ctx, "4", i); Z3_ast s1 = Z3_mk_const(ctx, Z3_mk_string_symbol(ctx,"s1"), i); Z3_ast s2 = Z3_mk_const(ctx, Z3_mk_string_symbol(ctx,"s2"), i); + (void) s2; Z3_ast c1 = Z3_mk_const_array(ctx, i, n1); Z3_ast x1 = Z3_mk_store(ctx, Z3_mk_store(ctx, c1, n2, n3), n1, n4); @@ -175,6 +177,7 @@ static void test_array() { Z3_ast xs[4] = { x1, x2, x3, x4}; Z3_ast exy = Z3_mk_eq(ctx, x2, x1); Z3_ast rxy = Z3_simplify(ctx, exy); + (void)rxy; TRACE("simplifier", tout << Z3_ast_to_string(ctx, rxy) << "\n";); TRACE("simplifier", tout << Z3_ast_to_string(ctx, Z3_simplify(ctx, Z3_mk_eq(ctx, x2, x3))) << "\n";); @@ -195,6 +198,8 @@ static void test_array() { Z3_ast sel1 = Z3_mk_select(ctx, x1, n1); Z3_ast sel2 = Z3_mk_select(ctx, x1, n4); + (void)sel1; + (void)sel2; TRACE("simplifier", tout << Z3_ast_to_string(ctx, Z3_simplify(ctx, sel1)) << "\n";