Refactor theory_array_base to use structured bindings for enode pairs

[Copilot]

Modernizes array theory propagation code to use C++17 structured bindings instead of .first/.second member access on enode pairs.

Changes

File: src/smt/theory_array_base.cpp

• propagate(): 3 sites refactored to use structured bindings with semantic names

  • Store axiom pairs: auto [store, select]
  • Extensionality/congruence pairs: auto [a1, a2]

• propagate_selects(): Eliminated intermediate variables, direct binding to auto [r, sel]

Example

Before:

for (unsigned i = 0; i < m_axiom2_todo.size(); ++i)
    assert_store_axiom2_core(m_axiom2_todo[i].first, m_axiom2_todo[i].second);

enode_pair & pair = todo[qhead];
enode * r   = pair.first;
enode * sel = pair.second;

After:

for (unsigned i = 0; i < m_axiom2_todo.size(); ++i) {
    auto [store, select] = m_axiom2_todo[i];
    assert_store_axiom2_core(store, select);
}

auto [r, sel] = todo[qhead];

No functional changes—semantically equivalent to original code.

Original prompt

---

This section details on the original issue you should resolve

<issue_title>[Conventions] Refactor theory_array_base to use structured bindings for enode pairs</issue_title>
<issue_description>This refactoring modernizes the array theory propagation code to use C++17 structured bindings instead of accessing .first and .second members of enode pairs.

Changes

File: src/smt/theory_array_base.cpp

Scope: Comprehensive refactoring of enode pair propagation patterns

Sites refactored: 5 member accesses across 2 functions

Type: enode_pair (alias for std::pair(enode*, enode*))

Naming:

• [store, select] for store axiom pairs
• [a1, a2] for extensionality and congruence pairs
• [r, sel] for select propagation pairs

Functions Modified

1. theory_array_base::propagate() - Main propagation loop (3 sites)

• Line 432: m_axiom2_todo[i].first, m_axiom2_todo[i].second → auto [store, select] = m_axiom2_todo[i];
• Line 435: m_extensionality_todo[i].first, m_extensionality_todo[i].second → auto [a1, a2] = m_extensionality_todo[i];
• Line 437: m_congruent_todo[i].first, m_congruent_todo[i].second → auto [a1, a2] = m_congruent_todo[i];

2. theory_array_base::propagate_selects() - Select propagation (1 site)

• Lines 855-857: Eliminated intermediate variables pair, r, sel
• Now: auto [r, sel] = todo[qhead]; directly used

Benefits

1. Improved Readability: Meaningful names (store/select, a1/a2, r/sel) instead of .first/.second
2. Code Simplification: Eliminates intermediate variable declarations
3. Clearer Intent: Makes the pairing relationship explicit through variable names
4. Type Safety: Structured bindings provide compile-time type checking
5. Consistency: Aligns with modern C++17 idioms used throughout Z3

Semantic Context

The enode pairs represent different array theory relationships:

• Store axiom pairs (store, select): Store and select operations to reconcile
• Extensionality pairs (a1, a2): Two arrays to prove extensionally equal
• Congruence pairs (a1, a2): Two arrays to check for congruence
• Propagation pairs (r, sel): Array root and select operation for upward propagation

The refactoring makes these relationships clearer through descriptive variable names.

Code Change Summary

• Lines changed: 17 lines across 2 functions
• Net impact: -4 lines (code simplification)
• Intermediate variables eliminated: 3 (pair, r, sel in propagate_selects)
• Member accesses eliminated: 5 (.first/.second replaced with structured bindings)

Testing

• No functional changes to the array theory propagation logic
• Existing unit tests for array theory should pass unchanged
• The refactoring is semantically equivalent to the original code

Related Work

This continues the structured bindings modernization effort in Z3:

• Consistent with previous refactorings in SAT, SMT, and AST subsystems
• Part of ongoing C++17/C++20 adoption across the codebase
• Follows the naming convention of using semantically meaningful names for structured bindings
• Particularly relevant for enode_pair patterns used throughout the SMT solver

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 theory_array_base to use structured bindings for enode pairs #8393

---

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