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

Refactor SMT core: use structured bindings for enode_pair access (#8427)

Browse source 
* Initial plan

* Refactor SMT core to use C++17 structured bindings for enode pairs

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

* Use const& in structured bindings to avoid copying

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

* Refactor variable unpacking in DEBUG_CODE

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
Co-authored-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Copilot 2026-01-29 19:01:49 -08:00 • committed by GitHub
parent 078be3bd65
commit 477e4d695d
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
4 changed files with 16 additions and 14 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/smt/seq_eq_solver.cpp
View file

@ -101,8 +101,8 @@ void theory_seq::add_consequence(bool uses_eq, expr_ref_vector const& clause) {
linearize(dep, eqs, lits);
for (auto& lit : lits)
lit.neg();
for (auto eq : eqs)
lits.push_back(~mk_eq(eq.first->get_expr(), eq.second->get_expr(), false));
for (auto const& [n1, n2] : eqs)
lits.push_back(~mk_eq(n1->get_expr(), n2->get_expr(), false));
for (auto f : clause)
lits.push_back(mk_literal(f));
add_axiom(lits);

4
src/smt/smt_conflict_resolution.cpp
View file

@ -201,9 +201,9 @@ namespace smt {
js->get_antecedents(*this);
}
while (!m_todo_eqs.empty()) {
enode_pair p = m_todo_eqs.back();
auto [n1, n2] = m_todo_eqs.back();
m_todo_eqs.pop_back();
eq2literals(p.first, p.second);
eq2literals(n1, n2);
}
if (m_todo_js_qhead == m_todo_js.size()) {
m_antecedents = nullptr;

7
src/smt/smt_context_pp.cpp
View file

@ -487,8 +487,8 @@ namespace smt {
fmls.push_back(n);
}
for (unsigned i = 0; i < num_eq_antecedents; ++i) {
enode_pair const & p = eq_antecedents[i];
n = m.mk_eq(p.first->get_expr(), p.second->get_expr());
auto const& [n1, n2] = eq_antecedents[i];
n = m.mk_eq(n1->get_expr(), n2->get_expr());
fmls.push_back(n);
}
if (x && y) {
@ -697,7 +697,8 @@ namespace smt {
}
std::ostream& operator<<(std::ostream& out, enode_eq_pp const& p) {
return out << enode_pp(p.p.first, p.ctx) << " = " << enode_pp(p.p.second, p.ctx) << "\n";
auto const& [n1, n2] = p.p;
return out << enode_pp(n1, p.ctx) << " = " << enode_pp(n2, p.ctx) << "\n";
}
void context::log_stats() {

15
src/smt/smt_justification.cpp
View file

@ -321,26 +321,27 @@ namespace smt {
region& r = ctx.get_region();
m_eqs = new (r) enode_pair[num_eqs];
std::uninitialized_copy(eqs, eqs + num_eqs, m_eqs);
DEBUG_CODE({
DEBUG_CODE(
for (unsigned i = 0; i < num_eqs; ++i) {
SASSERT(eqs[i].first->get_root() == eqs[i].second->get_root());
enode_pair const & [n1, n2] = eqs[i];
SASSERT(n1->get_root() == n2->get_root());
}
});
);
}
void ext_simple_justification::get_antecedents(conflict_resolution & cr) {
simple_justification::get_antecedents(cr);
for (unsigned i = 0; i < m_num_eqs; ++i) {
enode_pair const & p = m_eqs[i];
cr.mark_eq(p.first, p.second);
auto const& [n1, n2] = m_eqs[i];
cr.mark_eq(n1, n2);
}
}
bool ext_simple_justification::antecedent2proof(conflict_resolution & cr, ptr_buffer<proof> & result) {
bool visited = simple_justification::antecedent2proof(cr, result);
for (unsigned i = 0; i < m_num_eqs; ++i) {
enode_pair const & p = m_eqs[i];
proof * pr = cr.get_proof(p.first, p.second);
auto const& [n1, n2] = m_eqs[i];
proof * pr = cr.get_proof(n1, n2);
if (pr == nullptr)
visited = false;
else