mirror of
https://github.com/Z3Prover/z3
synced 2026-07-16 03:55:42 +00:00
2490e86d3f
## Summary Follow-up to #10001 addressing @NikolajBjorner's review comment: > isn't this nearly identical AI generated code to the other file? There has to be some modular approach to deal with sorting vectors? #10001 introduced two nearly-identical copies of a bounds-safe, mutation-aware index-permutation merge sort: - `algebraic_numbers.cpp::merge_sort_roots_perm` - `nlsat/levelwise.cpp::merge_sort_perm` Both exist because the comparator (`anum_manager::compare`/`lt`) is **not pure**: it mutates the algebraic numbers it compares (refining isolating intervals) and may throw on the resource limit, which makes `std::sort` undefined behavior (the original SIGSEGV). ## Change Extract the algorithm into a single shared helper `util/index_sort_with_mutations.h` (`stable_index_merge_sort`). The long rationale for why `std::sort` is unsafe and merge sort is safe now lives in exactly one place. Both call sites become thin wrappers that build the scratch buffer and forward their local comparator. No behavioral change: same stable O(n log n) merge sort over an index permutation. ## Verification CMake/Ninja Release build: - `test-z3 /seq algebraic_numbers` — PASS - `test-z3 /seq algebraic` — PASS - NRA/NIA smoke solves with `nlsat.lws=true` return expected sat/unsat. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> |
||
|---|---|---|
| .. | ||
| tactic | ||
| CMakeLists.txt | ||
| levelwise.cpp | ||
| levelwise.h | ||
| nlsat_assignment.h | ||
| nlsat_clause.cpp | ||
| nlsat_clause.h | ||
| nlsat_common.cpp | ||
| nlsat_common.h | ||
| nlsat_evaluator.cpp | ||
| nlsat_evaluator.h | ||
| nlsat_explain.cpp | ||
| nlsat_explain.h | ||
| nlsat_interval_set.cpp | ||
| nlsat_interval_set.h | ||
| nlsat_justification.h | ||
| nlsat_params.pyg | ||
| nlsat_scoped_literal_vector.h | ||
| nlsat_simple_checker.cpp | ||
| nlsat_simple_checker.h | ||
| nlsat_simplify.cpp | ||
| nlsat_simplify.h | ||
| nlsat_solver.cpp | ||
| nlsat_solver.h | ||
| nlsat_types.cpp | ||
| nlsat_types.h | ||
| nlsat_variable_ordering_strategy.cpp | ||
| nlsat_variable_ordering_strategy.h | ||