Refactor dyn_ack.cpp to use structured bindings for app_pair/app_triple

[Copilot]

Refactor dyn_ack.cpp to use structured bindings - COMPLETE ✅

• Initial refactoring with structured bindings
• Rename variables from app1/app2/app3 to a1/a2/a3 per code review feedback
• Build verification - compiles successfully
• Unit tests - all 164 tests pass (100% success rate)

Changes

File modified: src/smt/dyn_ack.cpp

• Replaced all .first, .second, .third member access with structured bindings
• Used shorter variable names: a1, a2, a3 (and suffixed versions a1_1, a2_2, etc.)
• Updated 8 functions with modern C++ idioms

Functions refactored:

1. app_pair_lt::operator() - Comparison operator for app pairs
2. dyn_ack_manager::gc() - Garbage collection for pairs
3. dyn_ack_manager::del_clause_eh() - Clause deletion handler
4. app_triple_lt::operator() - Comparison operator for app triples
5. dyn_ack_manager::gc_triples() - Garbage collection for triples
6. dyn_ack_manager::check_invariant() - Debug invariant checker
7. dyn_ack_manager::reset_app_pairs() - Cleanup for pairs
8. dyn_ack_manager::reset_app_triples() - Cleanup for triples

Original prompt

---

This section details on the original issue you should resolve

<issue_title>[Conventions] Refactor dyn_ack.cpp to use C++17 structured bindings for app_pair/app_triple</issue_title>
<issue_description>## Refactor to use C++17 structured bindings

This PR refactors src/smt/dyn_ack.cpp to use C++17 structured bindings instead of accessing .first, .second, and .third members of app_pair and app_triple objects.

Changes

File modified: src/smt/dyn_ack.cpp

• Lines changed: 71 additions, 31 deletions
• Functions refactored:
  • app_pair_lt::operator() - Comparison operator for app pairs
  • dyn_ack_manager::gc() - Garbage collection for pairs
  • dyn_ack_manager::del_clause_eh() - Clause deletion handler
  • app_triple_lt::operator() - Comparison operator for app triples
  • dyn_ack_manager::gc_triples() - Garbage collection for triples
  • dyn_ack_manager::check_invariant() - Debug invariant checker

Benefits

1. Improved Readability

Structured bindings with meaningful names (app1, app2, app3) make the code intent clearer than generic .first, .second, .third accessors.

Before:

m_app_pair2num_occs.find(p1.first, p1.second, n1);
m_app_pair2num_occs.find(p2.first, p2.second, n2);

After:

auto [app1_1, app1_2] = p1;
auto [app2_1, app2_2] = p2;
m_app_pair2num_occs.find(app1_1, app1_2, n1);
m_app_triple2num_occs.find(app2_1, app2_2, n2);

2. Reduced Error Potential

Eliminates the risk of accidentally swapping .first and .second in complex logic, as each component has a distinct name.

3. Modern C++ Idiom

Uses C++17 structured bindings, which is the idiomatic way to decompose pairs and tuples in modern C++.

4. Better Maintenance

When reading code that manipulates multiple pairs/triples, descriptive names make it easier to track which elements belong to which object.

Example Refactorings

Pair comparison:

// Before
bool operator()(app_pair const & p1, app_pair const & p2) const {
    unsigned n1 = 0, n2 = 0;
    m_app_pair2num_occs.find(p1.first, p1.second, n1);
    m_app_pair2num_occs.find(p2.first, p2.second, n2);
    return n1 > n2;
}

// After
bool operator()(app_pair const & p1, app_pair const & p2) const {
    auto [app1_1, app1_2] = p1;
    auto [app2_1, app2_2] = p2;
    unsigned n1 = 0, n2 = 0;
    m_app_pair2num_occs.find(app1_1, app1_2, n1);
    m_app_pair2num_occs.find(app2_1, app2_2, n2);
    return n1 > n2;
}

Triple handling in garbage collection:

// Before
for (; it != end; ++it) {
    app_triple & p = *it;
    if (m_triple.m_instantiated.contains(p)) {
        m.dec_ref(p.first);
        m.dec_ref(p.second);
        m.dec_ref(p.third);
        SASSERT(!m_triple.m_app2num_occs.contains(p.first, p.second, p.third));
        continue;
    }
    // ...
}

// After
for (; it != end; ++it) {
    app_triple & p = *it;
    auto [app1, app2, app3] = p;
    if (m_triple.m_instantiated.contains(p)) {
        m.dec_ref(app1);
        m.dec_ref(app2);
        m.dec_ref(app3);
        SASSERT(!m_triple.m_app2num_occs.contains(app1, app2, app3));
        continue;
    }
    // ...
}

Testing

• Functional equivalence: No changes to logic, only variable access patterns
• All call sites updated: All uses of .first, .second, .third replaced with structured bindings
• Debug assertions preserved: SASSERT statements updated with new variable names

Context

This refactoring is part of a larger C++ modernization effort in Z3:

• std::optional refactoring: 14 PRs, 57 call sites modernized
• Structured bindings: 4th PR in this series (previous: SAT bin_clause, SMT dyn_ack app_pair, SMT equality handlers)
• Target: Continue systematic modernization across the codebase

Subsystem

SMT - Dynamic Ackermann's reduction

This change affects the dynamic Ackermann's reduction implementation, which tracks pairs and triples of applications for congruence closure instantiation.

AI generated by Code Conventions Analyzer

Comments on the Issue (you are @copilot in this section)

Custom agent used: agentic-workflows
GitHub Agentic Workflows (gh-aw) - Create, debug, and upgrade AI-powered workflows with intelligent prompt routing

• Fixes [Conventions] Refactor dyn_ack.cpp to use C++17 structured bindings for app_pair/app_triple #8353

---

✨ Let Copilot coding agent set things up for you — coding agent works faster and does higher quality work when set up for your repo.

[NikolajBjorner]

@copilot call it a1 instead of app1, a2 instead of app2, a3 instead of app3

[NikolajBjorner]

https://gh.io/copilot-coding-agent-docs call it a1 instead of app1, a2 instead of app2, a3 instead of app3

[NikolajBjorner]

@copilot call it a1 instead of app1, a2 instead of app2, a3 instead of app3

[Copilot]

@copilot call it a1 instead of app1, a2 instead of app2, a3 instead of app3

Done! Renamed all structured binding variables to use shorter names: a1, a2, a3 (and suffixed versions like a1_1, a2_2, etc.). See commit 8eb8a91.