nlsat/anum: share mutation-aware merge sort in one helper (#10006)

## 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>

src/util/index_sort_with_mutations.h

@@ -0,0 +1,79 @@
+/*++
+Copyright (c) 2026 Microsoft Corporation
+
+Module Name:
+
+    index_sort_with_mutations.h
+
+Abstract:
+
+    Bounds-safe, mutation-aware stable merge sort of an index permutation.
+
+    This exists to be shared between sites whose ordering comparator is NOT a
+    fixed strict weak ordering over a single sort -- typically because the
+    comparator MUTATES the objects it compares (e.g. algebraic numbers, whose
+    comparison refines their isolating intervals) and may even throw when a
+    resource limit is hit mid-sort. Against such a comparator std::sort
+    (introsort) is undefined behavior: it relies on a comparator-derived
+    sentinel and re-compares a pivot repeatedly, so a comparison that
+    transiently strengthens from "uncertain" to "decided" invalidates the
+    sentinel and its *unguarded* insertion pass walks off the array -> an
+    out-of-bounds read -> SIGSEGV (a try/catch could not help).
+
+    Merge sort is safe BECAUSE of how it meets a mutating comparator:
+      1. It never re-compares a pair (each unordered pair is compared at exactly
+         one merge level), so "the verdict for this pair changed" cannot occur
+         within the sort.
+      2. It uses no comparator-derived sentinel; every loop bound is arithmetic
+         (i < mid, j < hi), so an inconsistent comparator can only yield a wrong
+         order, never an out-of-bounds access or non-termination.
+      3. If the comparator's refinement is monotone toward a true order, runs
+         are ordered by decided verdicts that later refinement cannot un-decide,
+         so each run stays sorted and deeper merges inherit cheaper comparisons.
+    It runs in O(n log n) comparisons and O(n) scratch, is stable, and unwinds
+    cleanly if the comparator throws on cancellation.
+
+Author:
+
+    Lev Nachmanson 2026
+
+--*/
+#pragma once
+
+#include <algorithm>
+
+/**
+   \brief Stable merge sort of an index permutation.
+
+   \c perm and \c scratch must each point to an array of \c n unsigned values;
+   \c perm holds the permutation to sort (typically 0..n-1). \c less(a, b) takes
+   two element indices and returns true iff element \c a must come strictly
+   before element \c b. On return \c perm holds the sorted permutation and
+   \c scratch has been used as working space. Equal/undecided pairs keep their
+   relative order (stable).
+*/
+template<typename Less>
+void stable_index_merge_sort(unsigned* perm, unsigned* scratch, unsigned n, Less less) {
+    if (n < 2)
+        return;
+    unsigned* src = perm;
+    unsigned* dst = scratch;
+    for (unsigned width = 1; width < n; width <<= 1) {
+        for (unsigned lo = 0; lo < n; lo += (width << 1)) {
+            unsigned mid = std::min(lo + width, n);
+            unsigned hi = std::min(lo + (width << 1), n);
+            unsigned i = lo, j = mid, k = lo;
+            // Take from the right run only on a strict decrease, so equal/
+            // undecided pairs keep their relative order (stable).
+            while (i < mid && j < hi)
+                dst[k++] = less(src[j], src[i]) ? src[j++] : src[i++];
+            while (i < mid)
+                dst[k++] = src[i++];
+            while (j < hi)
+                dst[k++] = src[j++];
+        }
+        std::swap(src, dst);
+    }
+    if (src != perm)
+        std::copy(src, src + n, perm);
+}