Recognize rational roots in closest-root isolation

[levnach]

What

In the closest-root isolation path (isolate_kth_root, used by the nlsat levelwise solver via isolate_roots_closest), detect when the unique root in an isolating interval is a rational number and return it as a basic rational numeral instead of constructing an algebraic_cell.

Why

Unlike the general isolate_roots(), the closest-root path does not factor the polynomial, so a reducible polynomial keeps its rational roots hidden inside algebraic cells. Such a cell is never converted to a rational later: interval refinement bisects at dyadic midpoints and can never land on a non-dyadic rational root. Every subsequent equality-flavored operation then pays the expensive machinery — sign evaluation at a sample point where the polynomial vanishes falls through to the resultant-based computation, and comparing two cells hiding the same rational ends in a Sturm-Tarski sequence on every comparison, with nothing cached.

Recognizing the rational at isolation time makes all downstream interactions exact and cheap. The detection uses the rational root theorem: refine the isolating interval to width < 1/|a_n| (the refine loop is adaptive and stops early if the interval is already tight), which leaves at most one candidate m/|a_n| in the interval, then confirm with a single exact sign evaluation.

Benchmarks

A/B runs on SMT-LIB QF_NRA (12,154 benchmarks), same commit and machine, differing only in the check being enabled (via a temporary parameter used for the experiment and removed from the final PR):

T=20	ON	OFF
sat / unsat	5531 / 5078	5531 / 5077
timeout	1545	1546

T=60	ON	OFF
sat / unsat	5633 / 5494	5632 / 5490
timeout	1027	1032

At T=60 the change solves 9 instances the baseline times out on and loses 5, net +5 solved; aggregate runtime is unchanged within noise (-0.17%). No errors, no model validation failures in either configuration.

🤖 Generated with Claude Code