[Conventions] Refactor theory_array_base to use structured bindings for enode pairs

[github-actions]

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