mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-03-11 15:50:29 +00:00
Code Activity

Fix unused variable build warnings in theory_finite_set, theory_finite_set_size, theory_nseq

Browse source 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
This commit is contained in:
copilot-swe-agent[bot] 2026-03-10 18:52:40 +00:00
parent 9c1d9af6d7
commit 472d9bde6c
3 changed files with 3 additions and 10 deletions
Download patch file Download diff file Expand all files Collapse all files

5
src/smt/theory_finite_set.cpp
View file

@ -171,7 +171,6 @@ namespace smt {
void theory_finite_set::add_in_axioms(enode *in, var_data *d) {
SASSERT(u.is_in(in->get_expr()));
auto e = in->get_arg(0)->get_expr();
auto set1 = in->get_arg(1);
for (enode *setop : d->m_parent_setops) {
SASSERT(
any_of(enode::args(setop), [&](enode *arg) { return in->get_arg(1)->get_root() == arg->get_root(); }));
@ -437,12 +436,11 @@ namespace smt {
return lit == arg;
};
auto lit1 = clause.get(0);
auto lit2 = clause.get(1);
auto position = 0;
if (is_complement_to(is_true, lit1, e))
position = 0;
else {
SASSERT(is_complement_to(is_true, lit2, e));
SASSERT(is_complement_to(is_true, clause.get(1), e));
position = 1;
}
@ -833,7 +831,6 @@ namespace smt {
}
app *mk_range_value(model_generator &mg, expr_ref_vector const &values) {
unsigned i = 0;
arith_value av(th.m);
av.init(&th.ctx);
vector<std::tuple<rational, enode *, bool>> elems;

1
src/smt/theory_finite_set_size.cpp
View file

@ -201,7 +201,6 @@ namespace smt {
for (auto [a, b] : th.m_diseqs) {
auto x = th.get_enode(a);
auto y = th.get_enode(b);
diseq d = {a, b};
if (n2b.contains(x) && n2b.contains(y)) {
arith_util a(m);
auto d1 = mk_diff(x, y);

7
src/smt/theory_nseq.cpp
View file

@ -54,7 +54,6 @@ namespace smt {
bool theory_nseq::internalize_atom(app* atom, bool /*gate_ctx*/) {
context& ctx = get_context();
ast_manager& m = get_manager();
// str.in_re atoms are boolean predicates: register as bool_var
// so that assign_eh fires when the SAT solver assigns them.
@ -761,7 +760,6 @@ namespace smt {
bool theory_nseq::propagate_length_lemma(literal lit, seq::length_constraint const& lc) {
context& ctx = get_context();
ast_manager& m = get_manager();
// unconditional constraints: assert as theory axiom
if (lc.m_kind == seq::length_kind::nonneg) {
@ -783,7 +781,7 @@ namespace smt {
lit));
ctx.assign(lit, js);
TRACE(seq, tout << "nseq length propagation: " << mk_pp(lc.m_expr, m)
TRACE(seq, tout << "nseq length propagation: " << mk_pp(lc.m_expr, get_manager())
<< " (" << eqs.size() << " eqs, " << lits.size() << " lits)\n";);
++m_num_length_axioms;
return true;
@ -813,7 +811,6 @@ namespace smt {
}
bool theory_nseq::assert_length_constraints() {
ast_manager& m = get_manager();
context& ctx = get_context();
vector<seq::length_constraint> constraints;
m_nielsen.generate_length_constraints(constraints);
@ -825,7 +822,7 @@ namespace smt {
ctx.internalize(e, true);
literal lit = ctx.get_literal(e);
if (ctx.get_assignment(lit) != l_true) {
TRACE(seq, tout << "nseq length lemma: " << mk_pp(e, m) << "\n";);
TRACE(seq, tout << "nseq length lemma: " << mk_pp(e, get_manager()) << "\n";);
propagate_length_lemma(lit, lc);
new_axiom = true;
}