mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-02-22 08:17:37 +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 Nikolaj Bjorner
parent 3c34c5c4d7
commit 78381bb285
4 changed files with 16 additions and 14 deletions
Download patch file Download diff file Expand all files Collapse all files

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