[Conventions] Refactor der.cpp to use structured bindings for expression/index pairs

[github-actions]

This refactoring modernizes the topological sort algorithm in der.cpp to use C++17 structured bindings instead of accessing .first and .second members of the frame pair.

Changes

File: src/ast/rewriter/der.cpp

Scope: Comprehensive refactoring of expression/index frame traversal

Sites refactored: 7+ member accesses in the main topological sort loop

Type: std::pair(expr*, unsigned) (expression + traversal index)

Naming: [e, idx] - clear expression and index semantics

Function Modified

der::top_sort() - Main topological sorting algorithm for variable elimination order

• Line 276: Changed frame & fr = todo.back(); expr * t = fr.first; → auto& [e, idx] = todo.back();
• Lines 277-329: Replaced all t references with e and all fr.second references with idx
• 7 member accesses simplified (multiple .first as t, multiple .second accesses)

Benefits

1. Improved Readability: Variable names e and idx are more descriptive than fr.first and fr.second
2. Code Simplification: Eliminates the need for the intermediate t variable
3. Clearer Intent: Makes it obvious that we're working with an expression and an index
4. Type Safety: Structured bindings provide compile-time type checking
5. Modern C++: Uses C++17 idiom consistently with Z3's modern codebase

Algorithm Context

The frame type represents a work item in the topological sort traversal:

• Expression (e): The AST node being visited
• Index (idx): The traversal state (0 = initial visit, 1 = revisit after dependencies, n = child index for APP nodes)

The refactoring makes this dual nature explicit through meaningful variable names.

Code Change Summary

• Lines changed: ~56 lines (full switch statement body)
• Net impact: Zero functional change, significantly improved readability
• Intermediate variables eliminated: 1 (t no longer needed)
• Member accesses eliminated: 7+ (replaced with direct structured binding references)

Testing

• No functional changes to the algorithm logic
• Existing unit tests for variable elimination 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

AI generated by Code Conventions Analyzer