[Conventions] Refactor euf_completion to use structured bindings for closure and proof pairs

[github-actions]

This refactoring modernizes the EUF completion simplifier to use C++17 structured bindings instead of accessing .first and .second members of pairs.

Changes

File: src/ast/simplifiers/euf_completion.cpp

Scope: Comprehensive refactoring of closure and proof/dependency pair patterns

Sites refactored: 8 member accesses across 4 functions

Types:

• std::pair(ptr_vector<expr), expr*> (closure: variable list + body)
• std::pair(proof_ref, expr_dependency*) (proof + dependency)

Naming:

• [vars, body] for closures - clear semantics for variable list and body expression
• [pr, dep] or [prf, dep] for proof/dependency pairs

Functions Modified

1. completion::propagate_closures() - Closure propagation (2 sites)

• Line 734: Changed clos.second → auto [vars, body] = clos; for inline extraction
• Line 753: Changed clos.first → direct use of vars
• Eliminates repeated member access in closure processing

2. completion::get_canonical() - Canonicalization (2 sites)

• Line 1080: Changed clos.second → auto [vars, body] = clos;
• Line 1096: Changed clos.first → direct use of vars
• Makes the closure structure explicit

3. completion::explain_eq() - Equality explanation (1 site)

• Line 1191: Changed m_pr_dep[from_ptr(j)].second → auto [pr, dep] = m_pr_dep[from_ptr(j)];
• Extracts dependency from proof/dependency pair

4. completion::explain_conflict() - Conflict explanation (1 site)

• Line 1202: Changed m_pr_dep[from_ptr(j)].second → auto [pr, dep] = m_pr_dep[from_ptr(j)];
• Extracts dependency from proof/dependency pair

5. completion::prove_eq() - Equality proof (1 site)

• Line 1218: Changed m_pr_dep[from_ptr(j)].first → auto [prf, dep] = m_pr_dep[from_ptr(j)];
• Extracts proof from proof/dependency pair

6. completion::prove_conflict() - Conflict proof (1 site)

• Line 1232: Changed m_pr_dep[from_ptr(j)].first → auto [prf, dep] = m_pr_dep[from_ptr(j)];
• Extracts proof from proof/dependency pair

Benefits

1. Improved Readability: Meaningful names (vars/body, pr/dep) instead of .first/.second
2. Self-Documenting: The structure of closures and proof pairs is immediately clear
3. Code Simplification: Eliminates repeated member access in loops
4. Type Safety: Structured bindings provide compile-time type checking
5. Consistency: Aligns with modern C++17 idioms used throughout Z3

Semantic Context

The pairs represent different EUF completion concepts:

• Closures (vars, body): Quantifier variable list paired with body expression for abstraction
• Proof/Dependency (pr, dep): Proof object paired with dependency tracking for justifications

The refactoring makes these dual structures explicit through descriptive variable names, especially important in the complex EUF completion algorithm.

Code Change Summary

• Lines changed: 18 lines across 6 functions
• Net impact: +6 lines (improved clarity with structured bindings)
• Member accesses eliminated: 8 (.first/.second replaced with named variables)
• Readability improvement: Significant - complex closure operations now self-explanatory

Testing

• No functional changes to the EUF completion logic
• Existing unit tests for equality saturation 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 valuable for improving readability of complex E-matching and completion algorithms

AI generated by Code Conventions Analyzer