[Conventions] Refactor dyn_ack to use structured bindings for app pairs and triples

[github-actions]

This PR refactors the dynamic Ackermann reduction module to use C++17 structured bindings for app_pair and app_triple patterns, improving code clarity and eliminating repeated .first, .second, .third access patterns.

Changes

File: src/smt/dyn_ack.cpp

Locations Refactored

1. app_pair_lt::operator() (lines 284-292)

   • Refactored comparison operator for application pairs
   • Type: std::pair(app*, app*) (pair of AST applications)
   • Naming: [a1, a2] and [b1, b2] for two compared pairs
   • Eliminates 4 .first/.second accesses (2 per pair)

2. dyn_ack_manager::gc() (lines 302-332)

   • Refactored garbage collection loop for application pairs
   • Type: app_pair (pair of applications)
   • Naming: [a1, a2] for app pair components
   • Eliminates 12+ .first/.second accesses in main GC loop
   • Clearer tracking of which app* is being referenced/dec_ref'd

3. dyn_ack_manager::del_clause_eh() (lines 352-370)

   • Refactored clause deletion event handler
   • Types: app_pair and app_triple
   • Naming: [a1, a2] for pairs, [t1, t2, t3] for triples
   • Eliminates 6 member accesses (4 for pair, 2 for triple in ASSERTs)

4. app_triple_lt::operator() (lines 512-520)

   • Refactored comparison operator for application triples
   • Type: triple(app*, app*, app*) (triple of applications)
   • Naming: [a1, a2, a3] and [b1, b2, b3] for compared triples
   • Eliminates 6 .first/.second/.third accesses (3 per triple)

5. dyn_ack_manager::gc_triples() (lines 530-563)

   • Refactored garbage collection for application triples
   • Type: app_triple
   • Naming: [a1, a2, a3] for triple components
   • Eliminates 18+ member accesses in triple GC loop

6. dyn_ack_manager::check_invariant() (lines 572-580, debug code)

   • Refactored debug invariant checker
   • Type: app_pair
   • Naming: [a1, a2] for pair components
   • Eliminates 2 .first/.second accesses

Total Impact

• 42+ member accesses eliminated (.first, .second, .third)
• 6 functions/operators refactored across pair and triple patterns
• Intermediate variables: Eliminated temporary extractions like p.first into local vars
• Clarity: Self-documenting variable names (a1, a2, a3) vs generic member access

Benefits

1. Readability: Clear variable names (a1, a2, t1, t2, t3) instead of .first/.second/.third
2. Less Error-Prone: No chance of accidentally swapping .first and .second in complex logic
3. Modern C++: Leverages C++17 structured bindings idiom
4. Maintainability: Easier to understand garbage collection and comparison logic
5. Consistency: Uniform pattern across all pair/triple handling

Examples

Before: app_pair comparison

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: Clear variable names

bool operator()(app_pair const & p1, app_pair const & p2) const {
    unsigned n1 = 0, n2 = 0;
    auto [a1, a2] = p1;
    m_app_pair2num_occs.find(a1, a2, n1);
    auto [b1, b2] = p2;
    m_app_pair2num_occs.find(b1, b2, n2);
    return n1 > n2;
}

Before: Triple garbage collection

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: Explicit component names

for (; it != end; ++it) {
    app_triple & p = *it;
    auto [a1, a2, a3] = p;
    if (m_triple.m_instantiated.contains(p)) {
        m.dec_ref(a1);
        m.dec_ref(a2);
        m.dec_ref(a3);
        SASSERT(!m_triple.m_app2num_occs.contains(a1, a2, a3));
        continue;
    }
}

Testing

• No functional changes to logic
• All member accesses replaced with equivalent structured bindings
• Garbage collection algorithms unchanged
• Debug assertions maintained

Notes

• Part of ongoing C++17 modernization effort
• Follows consistent naming: [a1, a2] for pairs, [a1, a2, a3] for triples
• Applied to both production and debug code paths

AI generated by Code Conventions Analyzer