mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-06-01 22:57:51 +00:00
Code Activity

Refactor theory_lra: Use structured bindings for pair patterns (#8387)

Browse source 
* Initial plan

* Refactor theory_lra.cpp with structured bindings for pair patterns

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-27 13:57:43 -08:00 • committed by Nikolaj Bjorner
parent d1489f0d13
commit 20d9b8645b
1 changed files with 26 additions and 25 deletions
Download patch file Download diff file Expand all files Collapse all files

51
src/smt/theory_lra.cpp
View file

@ -401,9 +401,9 @@ class theory_lra::imp {
theory_var w = mk_var(n1); theory_var w = mk_var(n1);
lpvar vj = register_theory_var_in_lar_solver(v); lpvar vj = register_theory_var_in_lar_solver(v);
lpvar wj = register_theory_var_in_lar_solver(w); lpvar wj = register_theory_var_in_lar_solver(w);
auto lu_constraints = lp().add_equality(vj, wj); auto [lower_ci, upper_ci] = lp().add_equality(vj, wj);
add_def_constraint(lu_constraints.first); add_def_constraint(lower_ci);
add_def_constraint(lu_constraints.second); add_def_constraint(upper_ci);
} }
} }
else if (is_app(n) && a.get_family_id() == to_app(n)->get_family_id()) { else if (is_app(n) && a.get_family_id() == to_app(n)->get_family_id()) {
@ -1915,8 +1915,8 @@ public:
expr_ref fml(m); expr_ref fml(m);
expr_ref_vector ts(m); expr_ref_vector ts(m);
rational rhs = c.rhs(); rational rhs = c.rhs();
for (auto cv : c.coeffs()) { for (auto [coeff, var] : c.coeffs()) {
ts.push_back(multerm(cv.first, var2expr(cv.second))); ts.push_back(multerm(coeff, var2expr(var)));
} }
switch (c.kind()) { switch (c.kind()) {
case lp::LE: fml = a.mk_le(a.mk_add(ts.size(), ts.data()), a.mk_numeral(rhs, true)); break; case lp::LE: fml = a.mk_le(a.mk_add(ts.size(), ts.data()), a.mk_numeral(rhs, true)); break;
@ -3330,13 +3330,13 @@ public:
if (vec.size() <= tv) { if (vec.size() <= tv) {
vec.resize(tv + 1, constraint_bound(UINT_MAX, rational())); vec.resize(tv + 1, constraint_bound(UINT_MAX, rational()));
} }
constraint_bound& b = vec[tv]; auto& [ci_ref, bound] = vec[tv];
if (b.first == UINT_MAX || (is_lower? b.second < v : b.second > v)) { if (ci_ref == UINT_MAX || (is_lower? bound < v : bound > v)) {
TRACE(arith, tout << "tighter bound " << tv << "\n";); TRACE(arith, tout << "tighter bound " << tv << "\n";);
m_history.push_back(vec[tv]); m_history.push_back(vec[tv]);
ctx().push_trail(history_trail<constraint_bound>(vec, tv, m_history)); ctx().push_trail(history_trail<constraint_bound>(vec, tv, m_history));
b.first = ci; ci_ref = ci;
b.second = v; bound = v;
} }
return true; return true;
} }
@ -3450,8 +3450,8 @@ public:
TRACE(arith, TRACE(arith,
for (auto c : m_core) for (auto c : m_core)
ctx().display_detailed_literal(tout << ctx().get_assign_level(c.var()) << " " << c << " ", c) << "\n"; ctx().display_detailed_literal(tout << ctx().get_assign_level(c.var()) << " " << c << " ", c) << "\n";
for (auto e : m_eqs) for (auto [n1, n2] : m_eqs)
tout << pp(e.first) << " = " << pp(e.second) << "\n"; tout << pp(n1) << " = " << pp(n2) << "\n";
tout << " ==> " << pp(x) << " = " << pp(y) << "\n"; tout << " ==> " << pp(x) << " = " << pp(y) << "\n";
); );
@ -3530,8 +3530,9 @@ public:
break; break;
} }
case equality_source: { case equality_source: {
SASSERT(m_equalities[idx].first != nullptr); auto [n1, n2] = m_equalities[idx];
SASSERT(m_equalities[idx].second != nullptr); SASSERT(n1 != nullptr);
SASSERT(n2 != nullptr);
m_eqs.push_back(m_equalities[idx]); m_eqs.push_back(m_equalities[idx]);
break; break;
} }
@ -3587,8 +3588,8 @@ public:
m_eqs.size(), m_eqs.data(), m_params.size(), m_params.data()))); m_eqs.size(), m_eqs.data(), m_params.size(), m_params.data())));
} }
else { else {
for (auto const& eq : m_eqs) { for (auto const& [n1, n2] : m_eqs) {
m_core.push_back(th.mk_eq(eq.first->get_expr(), eq.second->get_expr(), false)); m_core.push_back(th.mk_eq(n1->get_expr(), n2->get_expr(), false));
} }
for (literal & c : m_core) { for (literal & c : m_core) {
c.neg(); c.neg();
@ -3648,16 +3649,15 @@ public:
m_nla->am().set(r, 0); m_nla->am().set(r, 0);
while (!m_todo_terms.empty()) { while (!m_todo_terms.empty()) {
rational wcoeff = m_todo_terms.back().second; auto [term, wcoeff] = m_todo_terms.back();
t = m_todo_terms.back().first;
m_todo_terms.pop_back(); m_todo_terms.pop_back();
lp::lar_term const& term = lp().get_term(t); lp::lar_term const& term_ref = lp().get_term(term);
TRACE(nl_value, lp().print_term(term, tout) << "\n";); TRACE(nl_value, lp().print_term(term_ref, tout) << "\n";);
scoped_anum r1(m_nla->am()); scoped_anum r1(m_nla->am());
rational c1(0); rational c1(0);
m_nla->am().set(r1, c1.to_mpq()); m_nla->am().set(r1, c1.to_mpq());
m_nla->am().add(r, r1, r); m_nla->am().add(r, r1, r);
for (lp::lar_term::ival arg : term) { for (lp::lar_term::ival arg : term_ref) {
auto wi = arg.j(); auto wi = arg.j();
c1 = arg.coeff() * wcoeff; c1 = arg.coeff() * wcoeff;
if (lp().column_has_term(wi)) { if (lp().column_has_term(wi)) {
@ -3973,8 +3973,8 @@ public:
ctx().literal2expr(c, tmp); ctx().literal2expr(c, tmp);
nctx.assert_expr(tmp); nctx.assert_expr(tmp);
} }
for (auto const& eq : m_eqs) { for (auto const& [n1, n2] : m_eqs) {
nctx.assert_expr(m.mk_eq(eq.first->get_expr(), eq.second->get_expr())); nctx.assert_expr(m.mk_eq(n1->get_expr(), n2->get_expr()));
} }
} }
@ -4237,10 +4237,11 @@ public:
out << bpp(e) << " " << ctx().get_assignment(lit) << "\n"; out << bpp(e) << " " << ctx().get_assignment(lit) << "\n";
break; break;
} }
case equality_source: case equality_source: {
out << pp(m_equalities[idx].first) << " = " auto [n1, n2] = m_equalities[idx];
<< pp(m_equalities[idx].second) << "\n"; out << pp(n1) << " = " << pp(n2) << "\n";
break; break;
}
case definition_source: { case definition_source: {
theory_var v = m_definitions[idx]; theory_var v = m_definitions[idx];
if (v != null_theory_var) if (v != null_theory_var)