Merge with branch lws (#8498)

* t0 Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * t1 Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * t2 * scaffoldin * scaffolding Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * closer to the paper Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * more scaffolding Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * define symbolic_interval Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * t Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * use std::map instead of std::unordered_map Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * more accurate init of the relation between polynomial properties Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * t Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * pass anum_manager to levelwise, crash on sign Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * pass pmanager Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * create free function display functions * use new display functions * pass nlsat::solver to levelwise Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * add trace tag for levelwise Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * refactor Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * refactor Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * define indexed root expression Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * refact lws Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * refact lws Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * refactor lws Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * trying to figure out right indices Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * rename explain::main_operator to compute_conflict_explanation * preprocess the input of levelwise to drop a level Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * ttt Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * renaming Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * rename Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * work on seed_properties Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * work on seed_properties Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * work on seed_properties Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * move a comment Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * t Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * t Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * t Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * t Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * t Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * t Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * t Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * t Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * t Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * t Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * simplify Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * simplify Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * debug Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * refactor and assert _irreducible Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * add a display method Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * t Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * t Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * t Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * t Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * t Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * t Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * simplify Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * simplify Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * remove erase_from_Q Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * ignore holds properties Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * t Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * t Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * t Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * t Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * t Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * t Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * t Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * t Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * got a section Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * t Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * introdure mk_prop Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * t Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * t Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * remove a parameter Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * t Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * t Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * t Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * t Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * add parameter to suppress/enable levelwise Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * t Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * comment * t Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * fixing factoring and hitting NOT_IMPLEMENTED on ir_ord Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * adding ir_ord Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * produce more literals but creating sat lemmas Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * t Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * try iterative factoring Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * new file Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * create irreducible polynomials on init Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * add a guard on m_fail Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * t Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * process level 0 as well Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * remove a warning Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * debug Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * t Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * prepare to fill the relation Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * filling the relation Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * separate the lower and upper bound root functions Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * fix an assert statement Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * create a better queue on properties Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * normalize before pushing Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * relax an assert Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * rebase with master Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * add stats to track levelwise calls Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * catch and fail on an exception Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * fix a bug in Rule 4.2 Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * remove debug instruction Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * call levelwise on a correct set of polynomials Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * cosmetics Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * use polynomial_ref instead of poly* Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * do not refactor again multivariate polynomials Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * canonicalize polinomals in todo_set Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * t Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * t Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * canonicalize polynomials in nlsat Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * t * normalize polynomials Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * try not to fail in add_sgn_inv_leading_coeff_for Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * use the cache consistently Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * unsound state Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * unsound state Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * handle the zero case in add_ord_inv_resultant Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * optimizations by using cached psc Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * t Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * make normalize optional Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * Revert "make normalize optional" This reverts commit c80cfb0b8e3e260aec6dabaf2e686e347b514896. * t Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * cleanup and more caching Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * t Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * better sort of root functions Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * index bug Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * with resultant calculation ignore one of p and q with a common root Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * fix the duplicate bug Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * t * simplify by removing back propagation Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * t * t Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * t Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * hook up different relation build strategies for lws Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * introduce isolate_root_closest Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * fix a bug with non-adding ldcf Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * simple choice of non-vanishing Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * restore choose_non_zero_coeff Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * efficient sort of root functions Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * avoid ldcf with the projective theorem Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * omit some disc Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * use std_vector more Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * avoid a compare call Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * try optimizing build_interval_and_relation Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * discard a discriminant only in the section case Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * refactor Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * refactor * refactor Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * cache the polynomial roots Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * Revert "cache the polynomial roots" This reverts commit aefcd16aaad2cbd4de804c8de47678886eb8ba92. * ignore const non-null witnesses Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * toward more like SMT-RAT split Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * align with SMT-RAT Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * t Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * disables some heuristics in section Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * Implement chain noLdcf optimization matching SMT-RAT Add find_partition_boundary() helper to locate the boundary between lower and upper root partitions in m_rfunc. Implement compute_omit_lc_sector_chain() and compute_omit_lc_section_chain() following SMT-RAT's OneCellCAD.h logic: - Omit ldcf for extreme of lower chain (index 0) if it appears on upper side - Omit ldcf for extreme of upper chain (last index) if it appears on lower side Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com> * Restrict noDisc optimization to section_lowest_degree only Match SMT-RAT behavior: noDisc (discriminant omission for leaves connected only to section polynomial) is only applied for sectionHeuristic == 3 (lowest_degree), not for biggest_cell or chain. Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com> * Cache partition boundary to avoid repeated algebraic number comparisons Store the partition boundary (index of first root > sample) in relation_E after sorting root functions. Use this cached value in compute_omit_lc_sector_chain() and compute_omit_lc_section_chain() instead of recomputing via algebraic number comparisons. Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com> * Refactor levelwise: consolidate partition indices into m_l_rf/m_u_rf Replace scattered local l_index/u_index parameters and m_partition_boundary with two impl members: - m_l_rf: position of lower bound in m_rel.m_rfunc - m_u_rf: position of upper bound in m_rel.m_rfunc (UINT_MAX in section case) This simplifies the code by: - Removing parameter passing through multiple function calls - Removing redundant m_partition_boundary from relation_E - Making the partition state explicit in impl Also clean up nlsat_explain.cpp to trust root_function_interval invariants: - Section case: assert l and l_index are valid instead of defensive check - Sector bounds: !l_inf()/!u_inf() implies valid polynomial and index Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com> * Refactor levelwise: use member variables for per-level state Replace local variables and function parameters with member variables: - m_level_ps: polynomials at current level (owned) - m_level_tags: tags for each polynomial (owned) - m_witnesses: non-zero coefficient witnesses - m_poly_has_roots: which polynomials have roots - m_todo: pointer to todo_set Functions now use these member variables directly: - extract_max_tagged() fills m_level_ps/m_level_tags and sets m_level - process_level() and process_top_level() are now parameterless - All helper functions use member variables instead of parameters Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com> * Refactor levelwise: change m_todo from pointer to member - Change m_todo from todo_set* to todo_set - Initialize m_todo in constructor initializer list - Use m_todo.reset() in single_cell_work instead of creating local todo_set - Replace pointer access (m_todo->) with member access (m_todo.) Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com> * Add dynamic heuristic selection for levelwise projection Implement weight-based dynamic selection of projection heuristics in levelwise CAD. The weight function w(p, level) = deg(p, level) estimates projection complexity, with w(res(a,b)) ≈ w(a) + w(b). At each level, all three heuristics (biggest_cell, chain, lowest_degree) are evaluated and the one with minimum estimated resultant weight is selected. When fewer than 2 root functions exist, the default heuristic is used since all produce equivalent results. Add parameter nlsat.lws_dynamic_heuristic (default: true) to enable or disable dynamic selection. When disabled, the static heuristic from lws_sector_rel_mode/lws_section_rel_mode is used. Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com> * local optimization Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * call omit_lc only when both bounds are present Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * use std_vector Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * remove m_level_tags Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * count added lcs in the heuriistic estimates Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * add both side spanning tree heuristic Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * Fix nlsat projection bug: ensure polynomials with assumptions are also projected When polynomials are added as assumptions (via add_assumption or ensure_sign), they must also be added to the projection set (m_todo) to ensure proper cell construction. Previously, assumptions were added without corresponding projection, leading to unsound lemmas. Fixes: 1. In normalize(): collect lower-stage polynomials in m_lower_stage_polys and add them to m_ps in main() before projection. 2. In ensure_sign(): call insert_fresh_factors_in_todo(p) after adding assumption. 3. In project_cdcac(): when levelwise fails, use flet to set m_add_all_coeffs=true for the fallback projection. * Remove deprecated project_original and cell_sample parameter - Remove project_original() function from nlsat_explain.cpp - Remove m_sample_cell_project member variable - Simplify project() to just call project_cdcac() - Remove cell_sample parameter from nlsat_params.pyg - Update nlsat_solver.cpp to remove cell_sample() references - Update nlsat_explain.h constructor signature * Enforce bound polynomial LC protection in compute_omit_lc functions Move the invariant that bound-defining polynomials must never have their LC omitted from add_level_projections_sector() into the source functions: - compute_omit_lc_both_sides() - compute_omit_lc_chain_extremes() This centralizes the protection and removes the redundant override check. * fix the build Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * bug fixes Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * restore a deleted function Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * remove sector/section stats Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * Simplify levelwise: remove chain/lowest_degree heuristics, unify relation mode - Remove chain and lowest_degree heuristics, keep only biggest_cell and spanning_tree - Unify m_sector_relation_mode and m_section_relation_mode into single m_rel_mode - Remove lws_rel_mode, lws_sector_rel_mode, lws_section_rel_mode, lws_dynamic_heuristic params - lws_spt_threshold < 2 now disables spanning tree (single tuning parameter) - Restore noDisc optimization for spanning_tree leaves connected to boundary - Add noDisc for sector with same_boundary_poly (treat like section case) - Significant code reduction (~390 lines removed) Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * fix bug with skipping too many discriminants Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * t Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * simplifications and bug fixes in lws, use static_tree only with sector + different bound polynomials, otherwise us biggest cell Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * bug fixes and cleanup Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * add the discriminant in degenerated case Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * fix a bug with skipping a vanishing discriminant Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * remove the unsound optimization Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * fiddle with heuristics Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * preserve random seed in nlsat_solver::check_lemma Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * fix a typo in poly_has_roots Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * add lc(p) and disc(p) for a rootless p in section case Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * remove warnings Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * untracking .beads Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * fix the explosion in m_todo with lws.false Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * fix issue 8397 Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * set default to nlsat.lws=false for the merge with master Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * set nlsat.lws=true by default, enable levelwise Signed-off-by: Lev Nachmanson <levnach@hotmail.com> --------- Signed-off-by: Lev Nachmanson <levnach@hotmail.com> Co-authored-by: Claude Opus 4.5 <noreply@anthropic.com>
2026-03-31 08:39:01 +00:00 · 2026-02-04 07:52:02 -10:00 · 2026-02-04 07:52:02 -10:00 · 63f05ff6e6
commit 63f05ff6e6
parent 1f855efa09
22 changed files with 4002 additions and 267 deletions
--- a/src/math/polynomial/algebraic_numbers.cpp
+++ b/src/math/polynomial/algebraic_numbers.cpp
@ -678,6 +678,169 @@ namespace algebraic_numbers {
            isolate_roots(up, roots);
        }

+        unsigned sign_variations_at_mpq(upolynomial::upolynomial_sequence const & seq, mpq const & b) {
+            unsigned sz = seq.size();
+            if (sz <= 1)
+                return 0;
+            unsigned r = 0;
+            int sign = 0, prev_sign = 0;
+            for (unsigned i = 0; i < sz; ++i) {
+                unsigned psz      = seq.size(i);
+                mpz const * p     = seq.coeffs(i);
+                sign = static_cast<int>(upm().eval_sign_at(psz, p, b));
+                if (sign == 0)
+                    continue;
+                if (prev_sign != 0 && sign != prev_sign)
+                    r++;
+                prev_sign = sign;
+            }
+            return r;
+        }
+
+        // Isolate the i-th real root of sqf_p (1-based), where sqf_p is square-free and univariate.
+        // Return the root as an algebraic number in r. The polynomial stored in the result is sqf_p.
+        void isolate_kth_root(scoped_upoly const & sqf_p, upolynomial::upolynomial_sequence const & seq, unsigned i, numeral & r) {
+            SASSERT(i > 0);
+            unsigned sz = sqf_p.size();
+            mpz const * p = sqf_p.data();
+            SASSERT(sz > 0);
+            if (sz == 2) {
+                // Linear polynomial ax + b: root is -b/a (always rational).
+                scoped_mpq q(qm());
+                qm().set(q, p[0], p[1]);
+                qm().neg(q);
+                set(r, q);
+                return;
+            }
+            unsigned pos_k = upm().knuth_positive_root_upper_bound(sz, p);
+            unsigned neg_k = upm().knuth_negative_root_upper_bound(sz, p);
+
+            scoped_mpbq lo(bqm()), hi(bqm()), mid(bqm());
+            unsigned vminus = upm().sign_variations_at_minus_inf(seq);
+            unsigned v0     = upm().sign_variations_at_zero(seq);
+            unsigned vplus  = upm().sign_variations_at_plus_inf(seq);
+            unsigned le0_cnt = vminus - v0; // roots in (-oo, 0]
+
+            unsigned vlo, vhi;
+            unsigned target;
+            if (i <= le0_cnt) {
+                // Isolate within (-2^neg_k, 0] to keep the interval on the non-positive side.
+                bqm().power(mpbq(2), neg_k, lo);
+                bqm().neg(lo);
+                bqm().set(hi, 0);
+                vlo = vminus;
+                vhi = v0;
+                target = i;
+            }
+            else {
+                // Isolate within (0, 2^pos_k] to keep the interval on the non-negative side.
+                bqm().set(lo, 0);
+                bqm().power(mpbq(2), pos_k, hi);
+                vlo = v0;
+                vhi = vplus;
+                target = i - le0_cnt;
+            }
+
+            // Sanity: sqf_p has at least i roots.
+            SASSERT(vlo >= vhi);
+            SASSERT(i <= vminus - vplus);
+            SASSERT(target > 0);
+            SASSERT(target <= vlo - vhi);
+            while (vlo > vhi + 1) {
+                checkpoint();
+                bqm().add(lo, hi, mid);
+                bqm().div2(mid);
+                unsigned vmid = upm().sign_variations_at(seq, mid);
+                unsigned left_cnt = vlo - vmid; // roots in (lo, mid]
+                if (target <= left_cnt) {
+                    bqm().set(hi, mid);
+                    vhi = vmid;
+                }
+                else {
+                    bqm().set(lo, mid);
+                    vlo = vmid;
+                    target -= left_cnt;
+                }
+            }
+            SASSERT(vlo == vhi + 1);
+
+            // If the upper endpoint is exactly a dyadic root, return it as a basic number.
+            if (upm().eval_sign_at(sz, p, hi) == 0) {
+                scoped_mpq q(qm());
+                to_mpq(qm(), hi, q);
+                set(r, q);
+                return;
+            }
+
+            // Convert the isolating interval into a refinable one (or discover a dyadic root on the way).
+            scoped_mpbq a(bqm()), b(bqm());
+            bqm().set(a, lo);
+            bqm().set(b, hi);
+            if (!upm().isolating2refinable(sz, p, bqm(), a, b)) {
+                scoped_mpq q(qm());
+                to_mpq(qm(), a, q);
+                set(r, q);
+                return;
+            }
+
+            del(r);
+            r = mk_algebraic_cell(sz, p, a, b, false /* minimal */);
+            SASSERT(acell_inv(*r.to_algebraic()));
+        }
+
+        // Closest-root isolation for an (integer) univariate polynomial.
+        void isolate_roots_closest_univariate(polynomial_ref const & p, mpq const & s, numeral_vector & roots, svector<unsigned> & indices) {
+            SASSERT(is_univariate(p));
+            SASSERT(roots.empty());
+            indices.reset();
+
+            if (::is_zero(p) || ::is_const(p))
+                return;
+
+            // Convert to dense univariate form and take the square-free part.
+            scoped_upoly & up = m_isolate_tmp1;
+            scoped_upoly & sqf_p = m_isolate_tmp3;
+            up.reset();
+            sqf_p.reset();
+            upm().to_numeral_vector(p, up);
+            if (up.empty())
+                return;
+            upm().square_free(up.size(), up.data(), sqf_p);
+            if (sqf_p.empty() || upm().degree(sqf_p) == 0)
+                return;
+
+            upolynomial::scoped_upolynomial_sequence seq(upm());
+            upm().sturm_seq(sqf_p.size(), sqf_p.data(), seq);
+            unsigned vminus = upm().sign_variations_at_minus_inf(seq);
+            unsigned vplus  = upm().sign_variations_at_plus_inf(seq);
+            if (vminus <= vplus)
+                return;
+
+            unsigned vs = sign_variations_at_mpq(seq, s);
+            unsigned total = vminus - vplus;
+            unsigned k = vminus - vs; // #roots in (-oo, s]
+
+            if (upm().eval_sign_at(sqf_p.size(), sqf_p.data(), s) == 0) {
+                roots.push_back(numeral());
+                set(roots.back(), s);
+                indices.push_back(k);
+                return;
+            }
+
+            // predecessor (<= s)
+            if (k > 0) {
+                roots.push_back(numeral());
+                isolate_kth_root(sqf_p, seq, k, roots.back());
+                indices.push_back(k);
+            }
+            // successor (> s)
+            if (k < total) {
+                roots.push_back(numeral());
+                isolate_kth_root(sqf_p, seq, k + 1, roots.back());
+                indices.push_back(k + 1);
+            }
+        }
+
        void mk_root(scoped_upoly const & up, unsigned i, numeral & r) {
            // TODO: implement version that finds i-th root without isolating all roots.
            if (i == 0)
@ -2547,6 +2710,77 @@ namespace algebraic_numbers {
            }
        }

+        void isolate_roots_closest(polynomial_ref const & p, polynomial::var2anum const & x2v, mpq const & s, numeral_vector & roots, svector<unsigned> & indices) {
+            TRACE(isolate_roots, tout << "isolating closest roots of: " << p << " around " << m_qmanager.to_string(s) << "\n";);
+            SASSERT(roots.empty());
+            indices.reset();
+
+            polynomial::manager & ext_pm = p.m();
+            if (ext_pm.is_zero(p) || ext_pm.is_const(p))
+                return;
+
+            if (ext_pm.is_univariate(p)) {
+                isolate_roots_closest_univariate(p, s, roots, indices);
+                return;
+            }
+
+            // eliminate rationals
+            polynomial_ref p_prime(ext_pm);
+            var2basic x2v_basic(*this, x2v);
+            p_prime = ext_pm.substitute(p, x2v_basic);
+            if (ext_pm.is_zero(p_prime) || ext_pm.is_const(p_prime))
+                return;
+
+            if (ext_pm.is_univariate(p_prime)) {
+                polynomial::var x = ext_pm.max_var(p_prime);
+                if (x2v.contains(x)) {
+                    // The remaining variable is assigned, the actual unassigned variable vanished when we replaced rational values.
+                    // So, the polynomial does not have any roots.
+                    return;
+                }
+                isolate_roots_closest_univariate(p_prime, s, roots, indices);
+                return;
+            }
+
+            // Fallback: isolate all roots then select closest ones.
+            scoped_numeral_vector all(m_wrapper);
+            isolate_roots(p, x2v, all);
+            if (all.empty())
+                return;
+
+            scoped_numeral sv(m_wrapper);
+            set(sv, s);
+
+            unsigned lower = UINT_MAX, upper = UINT_MAX;
+            for (unsigned k = 0; k < all.size(); ++k) {
+                auto cmp = compare(all[k], sv);
+                if (cmp <= 0)
+                    lower = k;
+                else {
+                    upper = k;
+                    break;
+                }
+            }
+
+            if (lower != UINT_MAX && eq(all[lower], s)) {
+                roots.push_back(numeral());
+                set(roots.back(), all[lower]);
+                indices.push_back(lower + 1);
+                return;
+            }
+
+            if (lower != UINT_MAX) {
+                roots.push_back(numeral());
+                set(roots.back(), all[lower]);
+                indices.push_back(lower + 1);
+            }
+            if (upper != UINT_MAX) {
+                roots.push_back(numeral());
+                set(roots.back(), all[upper]);
+                indices.push_back(upper + 1);
+            }
+        }
+
        sign eval_at_mpbq(polynomial_ref const & p, polynomial::var2anum const & x2v, polynomial::var x, mpbq const & v) {
            scoped_mpq  qv(qm());
            to_mpq(qm(), v, qv);
@ -3011,6 +3245,10 @@ namespace algebraic_numbers {
        m_imp->isolate_roots(p, x2v, roots);
    }

+    void manager::isolate_roots_closest(polynomial_ref const & p, polynomial::var2anum const & x2v, mpq const & s, numeral_vector & roots, svector<unsigned> & indices) {
+        m_imp->isolate_roots_closest(p, x2v, s, roots, indices);
+    }
+
    void manager::isolate_roots(polynomial_ref const & p, polynomial::var2anum const & x2v, numeral_vector & roots, svector<sign> & signs) {
        m_imp->isolate_roots(p, x2v, roots, signs);
    }
--- a/src/math/polynomial/algebraic_numbers.h
+++ b/src/math/polynomial/algebraic_numbers.h
@ -169,6 +169,19 @@ namespace algebraic_numbers {
        */
        void isolate_roots(polynomial_ref const & p, polynomial::var2anum const & x2v, numeral_vector & roots);

+        /**
+           \brief Isolate the closest real roots of a multivariate polynomial p around the rational point s.
+
+           The method behaves like isolate_roots(p, x2v, roots) but only returns:
+           - the last root r such that r <= s (if it exists), and
+           - the first root r such that r >  s (if it exists),
+           or a single root if s itself is a root.
+
+           The returned roots are sorted increasingly. The associated 1-based root indices
+           (with respect to the full increasing root list) are stored in \c indices.
+        */
+        void isolate_roots_closest(polynomial_ref const & p, polynomial::var2anum const & x2v, mpq const & s, numeral_vector & roots, svector<unsigned> & indices);
+
        /**
           \brief Isolate the roots of the given polynomial, and compute its sign between them.
        */
--- a/src/math/polynomial/polynomial_cache.cpp
+++ b/src/math/polynomial/polynomial_cache.cpp
@ -128,7 +128,7 @@ namespace polynomial {
            m_factor_cache.reset();
        }

-        unsigned pid(polynomial * p) const { return m.id(p); }
+        unsigned pid(const polynomial * p) const { return m.id(p); }
        
        polynomial * mk_unique(polynomial * p) {
            if (m_in_cache.get(pid(p), false))
@ -141,6 +141,28 @@ namespace polynomial {
            return p_prime;
        }

+        bool contains(const polynomial * p) const {
+            return m_in_cache.get(pid(p), false);
+        }
+
+        bool contains_chain(polynomial * p, polynomial * q, var x) const {
+            if (!m_in_cache.get(pid(p), false)) {
+                polynomial * const * p2 = m_poly_table.find_core(p);
+                if (!p2)
+                    return false;
+                p = *p2;
+            }
+            if (!m_in_cache.get(pid(q), false)) {
+                polynomial * const * q2 = m_poly_table.find_core(q);
+                if (!q2)
+                    return false;
+                q = *q2;
+            }
+            unsigned h = hash_u_u(pid(p), pid(q));
+            psc_chain_entry key(p, q, x, h);
+            return m_psc_chain_cache.contains(&key);
+        }
+
        void psc_chain(polynomial * p, polynomial * q, var x, polynomial_ref_vector & S) {
            p = mk_unique(p);
            q = mk_unique(q);
@ -213,6 +235,14 @@ namespace polynomial {
        return m_imp->mk_unique(p);
    }

+    bool cache::contains(const polynomial * p) const {
+        return m_imp->contains(p);
+    }
+
+    bool cache::contains_chain(polynomial const * p, polynomial const * q, var x) const {
+        return m_imp->contains_chain(const_cast<polynomial*>(p), const_cast<polynomial*>(q), x);
+    }
+
    void cache::psc_chain(polynomial const * p, polynomial const * q, var x, polynomial_ref_vector & S) {
        m_imp->psc_chain(const_cast<polynomial*>(p), const_cast<polynomial*>(q), x, S);
    }
--- a/src/math/polynomial/polynomial_cache.h
+++ b/src/math/polynomial/polynomial_cache.h
@ -34,9 +34,10 @@ namespace polynomial {
        manager & m() const;
        manager & pm() const { return m(); }
        polynomial * mk_unique(polynomial * p);
+        bool contains(const polynomial * p) const;
+        bool contains_chain(polynomial const * p, polynomial const * q, var x) const;
        void psc_chain(polynomial const * p, polynomial const * q, var x, polynomial_ref_vector & S);
        void factor(polynomial const * p, polynomial_ref_vector & distinct_factors);
        void reset();
    };
 };
-