Refactor der.cpp topological sort to use structured bindings

[Copilot]

Modernizes der_sort_vars() topological sort traversal to use C++17 structured bindings instead of pair member access.

Changes

Before:

frame & fr = todo.back();
expr * t   = fr.first;
// ... later in code
if (done.is_marked(t)) { ... }
if (fr.second == 0) { ... }
fr.second = 1;

After:

auto& [e, idx] = todo.back();
// ... later in code
if (done.is_marked(e)) { ... }
if (idx == 0) { ... }
idx = 1;

Impact

• Eliminates intermediate variable t
• Replaces 10+ generic pair accessors with semantically meaningful names
• e clearly represents the AST expression being visited
• idx clearly represents the traversal state (0=initial, 1=post-children, n=child index)
• No functional changes to algorithm logic

Original prompt

---

This section details on the original issue you should resolve

<issue_title>[Conventions] Refactor der.cpp to use structured bindings for expression/index pairs</issue_title>
<issue_description>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

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 der.cpp to use structured bindings for expression/index pairs #8392

---

💡 You can make Copilot smarter by setting up custom instructions, customizing its development environment and configuring Model Context Protocol (MCP) servers. Learn more Copilot coding agent tips in the docs.