mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-05-25 11:26:21 +00:00
Code Activity

Refactor SMT equality handlers to use C++17 structured bindings (#8321)

Browse source 
* Initial plan

* Refactor SMT equality handlers to use C++17 structured bindings

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
This commit is contained in:
Copilot 2026-01-24 12:07:38 -08:00 • committed by GitHub
parent 301d0e061f
commit c88c781f3b
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
2 changed files with 17 additions and 17 deletions
Download patch file Download diff file Expand all files Collapse all files

8
src/smt/arith_eq_adapter.cpp
View file

@ -258,12 +258,12 @@ namespace smt {
TRACE(arith_eq_adapter, tout << "restart\n";); TRACE(arith_eq_adapter, tout << "restart\n";);
enode_pair_vector tmp(m_restart_pairs); enode_pair_vector tmp(m_restart_pairs);
m_restart_pairs.reset(); m_restart_pairs.reset();
for (auto const& p : tmp) { for (auto const& [n1, n2] : tmp) {
if (ctx.inconsistent()) if (ctx.inconsistent())
break; break;
TRACE(arith_eq_adapter, tout << "creating arith_eq_adapter axioms at the base level #" << p.first->get_owner_id() << " #" << TRACE(arith_eq_adapter, tout << "creating arith_eq_adapter axioms at the base level #" << n1->get_owner_id() << " #" <<
p.second->get_owner_id() << "\n";); n2->get_owner_id() << "\n";);
mk_axioms(p.first, p.second); mk_axioms(n1, n2);
} }
} }

26
src/smt/theory_seq.cpp
View file

@ -598,9 +598,9 @@ bool theory_seq::check_extensionality(expr* e1, enode* n1, enode* n2) {
m_exclude.update(o1, o2); m_exclude.update(o1, o2);
return true; return true;
} }
for (auto const& p : m_new_eqs) { for (auto const& [first, second] : m_new_eqs) {
if (m_exclude.contains(p.first, p.second)) { if (m_exclude.contains(first, second)) {
TRACE(seq, tout << "excluded " << mk_pp(p.first, m) << " " << mk_pp(p.second, m) << "\n";); TRACE(seq, tout << "excluded " << mk_pp(first, m) << " " << mk_pp(second, m) << "\n";);
return true; return true;
} }
} }
@ -926,10 +926,10 @@ bool theory_seq::simplify_eq(expr_ref_vector& ls, expr_ref_vector& rs, dependenc
} }
TRACE(seq, TRACE(seq,
tout << "reduced to\n"; tout << "reduced to\n";
for (auto p : new_eqs) { for (auto [first, second] : new_eqs) {
tout << mk_bounded_pp(p.first, m, 2) << "\n"; tout << mk_bounded_pp(first, m, 2) << "\n";
tout << " = \n"; tout << " = \n";
tout << mk_bounded_pp(p.second, m, 2) << "\n"; tout << mk_bounded_pp(second, m, 2) << "\n";
} }
); );
m_seq_rewrite.add_seqs(ls, rs, new_eqs); m_seq_rewrite.add_seqs(ls, rs, new_eqs);
@ -939,11 +939,11 @@ bool theory_seq::simplify_eq(expr_ref_vector& ls, expr_ref_vector& rs, dependenc
} }
TRACE(seq_verbose, TRACE(seq_verbose,
tout << ls << " = " << rs << "\n";); tout << ls << " = " << rs << "\n";);
for (auto const& p : new_eqs) { for (auto const& [first, second] : new_eqs) {
if (ctx.inconsistent()) if (ctx.inconsistent())
break; break;
expr_ref li(p.first, m); expr_ref li(first, m);
expr_ref ri(p.second, m); expr_ref ri(second, m);
seq::eq_ptr r; seq::eq_ptr r;
m_eq_deps = deps; m_eq_deps = deps;
if (m_eq.reduce(li, ri, r)) { if (m_eq.reduce(li, ri, r)) {
@ -961,8 +961,8 @@ bool theory_seq::simplify_eq(expr_ref_vector& ls, expr_ref_vector& rs, dependenc
} }
TRACE(seq_verbose, TRACE(seq_verbose,
if (!ls.empty() || !rs.empty()) tout << ls << " = " << rs << ";\n"; if (!ls.empty() || !rs.empty()) tout << ls << " = " << rs << ";\n";
for (auto const& p : new_eqs) { for (auto const& [first, second] : new_eqs) {
tout << mk_pp(p.first, m) << " = " << mk_pp(p.second, m) << ";\n"; tout << mk_pp(first, m) << " = " << mk_pp(second, m) << ";\n";
}); });
@ -2424,8 +2424,8 @@ void theory_seq::validate_fmls(enode_pair_vector const& eqs, literal_vector cons
ctx.literal2expr(lit, fml); ctx.literal2expr(lit, fml);
fmls.push_back(fml); fmls.push_back(fml);
} }
for (auto const& p : eqs) { for (auto const& [n1, n2] : eqs) {
fmls.push_back(m.mk_eq(p.first->get_expr(), p.second->get_expr())); fmls.push_back(m.mk_eq(n1->get_expr(), n2->get_expr()));
} }
TRACE(seq, tout << fmls << "\n";); TRACE(seq, tout << fmls << "\n";);