[Conventions] Refactor bound_manager to use structured bindings for limit pairs

[github-actions]

This refactoring modernizes the bound manager to use C++17 structured bindings instead of accessing .first and .second members of limit pairs.

Changes

File: src/ast/simplifiers/bound_manager.cpp

Scope: Refactoring of bound comparison logic for upper and lower bounds

Sites refactored: 4 member accesses across 2 functions

Type: limit (alias for std::pair(numeral, bool) - bound value + strictness flag)

Naming: [old_bound, old_strict] - clear semantics for bound value and strictness

Functions Modified

1. bound_manager::insert_upper() - Upper bound insertion

• Line 158: Changed comparison from old.first and old.second to structured bindings
• Added: auto [old_bound, old_strict] = old;
• Replaced: old.first → old_bound, old.second → old_strict

2. bound_manager::insert_lower() - Lower bound insertion

• Line 178: Changed comparison from old.first and old.second to structured bindings
• Added: auto [old_bound, old_strict] = old;
• Replaced: old.first → old_bound, old.second → old_strict

Benefits

1. Improved Readability: Variable names old_bound and old_strict are much more descriptive than old.first and old.second
2. Self-Documenting: The meaning of the pair components is immediately clear
3. Clearer Logic: The bound comparison expressions are easier to understand with meaningful 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 limit type represents a bound constraint:

• Bound value (old_bound): The numeric limit (rational number)
• Strictness flag (old_strict): Whether the bound is strict (< or >) vs non-strict (≤ or ≥)

The comparison logic checks if a new bound improves the existing bound:

• For upper bounds: New bound is better if it's smaller, or equal but stricter
• For lower bounds: New bound is better if it's larger, or equal but stricter

The refactoring makes this logic much clearer through descriptive variable names.

Code Change Summary

• Lines changed: 8 lines (4 in each function)
• Net impact: +2 lines (added structured binding declarations)
• Member accesses eliminated: 4 (.first/.second replaced with named variables)
• Readability improvement: Significant - complex boolean expressions now self-explanatory

Testing

• No functional changes to the bound management logic
• Existing unit tests for bound manager 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 comparison logic

AI generated by Code Conventions Analyzer