nla: row-implied bound propagation and a bounds-only linear probe

Effectively-linear nonlinear queries (monomials whose factors are pinned by
fixed constants, as in F* machine-arithmetic) were starved in solver 6: the
factor columns lacked bound sides that theory_arith asserts into its tableau
via row-implied bound propagation, so interval reasoning of products never
fired and the search fell into Grobner/Horner/nlsat churn.

- monomial_bounds::propagate_row_implied_bounds: assert row-implied bounds of
  violated monomials' columns as LP column bounds, incrementally on changed
  columns and at final check ahead of the lemma passes; level 1 fills only
  missing sides from fixed-anchored rows, arith.nl.propagate_row_bounds_improve
  escalates to improvements (bounds-only mode).
- guards: bit-size cap on derived bounds (arith.nl.propagate_row_bounds_max_bits),
  perfect-square patching skipped over 256 bits, exponential bounded-nlsat
  backoff, quotient-lemma coefficient gate (arith.nl.grobner_quotient_max_bits),
  bit-size-gated fixed substitution (arith.nl.grobner_subs_fixed_max_bits),
  optional grobner deferral on bounds progress.
- linear probe: smt.arith.nl.linear_probe runs a short bounds-only kernel in
  its own ast_manager before the main SMT search (smt_solver), falling back
  unchanged; nl-linear-probe tactic for strategies.

F* regression suite: 17-18/19 solved all-seeds vs 16/19 for both the legacy
solver and baseline; Pulse.Lib.ForEvery-1 and failedQueries-FStar.Math.Euclid-3
solved for the first time; queries-FStar.UInt128-10 reaches 234-235/235
sub-queries. QF_NIA samples (2x128 files): identical totals, no disagreements.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

src/math/lp/lar_solver.h

@@ -109,6 +109,7 @@ class lar_solver : public column_namer {
     bool sizes_are_correct() const;
     bool implied_bound_is_correctly_explained(implied_bound const& be, const vector<std::pair<mpq, unsigned>>& explanation) const;
 
+public:
     template <typename T>
     unsigned calculate_implied_bounds_for_row(unsigned row_index, lp_bound_propagator<T>& bp) {
         if (A_r().m_rows[row_index].size() > settings().max_row_length_for_bound_propagation || row_has_a_big_num(row_index))
@@ -119,6 +120,7 @@ class lar_solver : public column_namer {
             zero_of_type<numeric_pair<mpq>>(),
             bp);
     }
+private:
 
     static void clean_popped_elements_for_heap(unsigned n, lpvar_heap& set);
     static void clean_popped_elements(unsigned n, indexed_uint_set& set);

src/math/lp/lp_settings.h

@@ -124,6 +124,7 @@ struct statistics {
     unsigned m_nla_add_bounds = 0;
     unsigned m_nla_propagate_bounds = 0;
     unsigned m_nla_propagate_eq = 0;
+    unsigned m_nla_propagate_row_bounds = 0;
     unsigned m_nla_lemmas = 0;
     unsigned m_nra_calls = 0;
     unsigned m_nla_bounds_improvements = 0;
@@ -173,6 +174,7 @@ struct statistics {
         st.update("arith-nla-add-bounds", m_nla_add_bounds);
         st.update("arith-nla-propagate-bounds", m_nla_propagate_bounds);
         st.update("arith-nla-propagate-eq", m_nla_propagate_eq);
+        st.update("arith-nla-propagate-row-bounds", m_nla_propagate_row_bounds);
         st.update("arith-nla-lemmas", m_nla_lemmas);
         st.update("arith-nra-calls", m_nra_calls);   
         st.update("arith-bounds-improvements", m_nla_bounds_improvements);

src/math/lp/monomial_bounds.cpp

@@ -11,6 +11,7 @@
 #include "math/lp/nla_core.h"
 #include "math/lp/nla_intervals.h"
 #include "math/lp/numeric_pair.h"
+#include "math/lp/lp_bound_propagator.h"
 
 namespace nla {
 
@@ -580,8 +581,8 @@ namespace nla {
             rational U(dep.upper(range));
             if (U.root(p, r) && improves_upper(r)) {
                 auto cmp = dep.upper_is_open(range) ? llc::LT : llc::LE;
-                propagate_lp_bound(v, cmp, r, dep.get_upper_dep(range));
-                tightened = true;
+                if (propagate_lp_bound(v, cmp, r, dep.get_upper_dep(range)))
+                    tightened = true;
             }
         }
         // Even power, v known non-positive: range.lower gives v <= -root(p, L).
@@ -592,8 +593,8 @@ namespace nla {
                 auto cmp = dep.lower_is_open(range) ? llc::LT : llc::LE;
                 u_dependency* d = c().lra.join_deps(dep.get_lower_dep(range),
                                                     c().lra.get_column_upper_bound_witness(v));
-                propagate_lp_bound(v, cmp, -r, d);
-                tightened = true;
+                if (propagate_lp_bound(v, cmp, -r, d))
+                    tightened = true;
             }
         }
         return tightened;
@@ -624,8 +625,8 @@ namespace nla {
                 rational L(dep.lower(range));
                 if (L.root(p, r) && improves_lower(r)) {
                     auto cmp = dep.lower_is_open(range) ? llc::GT : llc::GE;
-                    propagate_lp_bound(v, cmp, r, dep.get_lower_dep(range));
-                    tightened = true;
+                    if (propagate_lp_bound(v, cmp, r, dep.get_lower_dep(range)))
+                        tightened = true;
                 }
             }
             return tightened;
@@ -635,8 +636,8 @@ namespace nla {
             rational U(dep.upper(range));
             if (!U.is_neg() && U.root(p, r) && improves_lower(-r)) {
                 auto cmp = dep.upper_is_open(range) ? llc::GT : llc::GE;
-                propagate_lp_bound(v, cmp, -r, dep.get_upper_dep(range));
-                tightened = true;
+                if (propagate_lp_bound(v, cmp, -r, dep.get_upper_dep(range)))
+                    tightened = true;
             }
         }
         // Even power, v known non-negative: range.lower gives v >= root(p, L).
@@ -647,8 +648,8 @@ namespace nla {
                 auto cmp = dep.lower_is_open(range) ? llc::GT : llc::GE;
                 u_dependency* d = c().lra.join_deps(dep.get_lower_dep(range),
                                                     c().lra.get_column_lower_bound_witness(v));
-                propagate_lp_bound(v, cmp, r, d);
-                tightened = true;
+                if (propagate_lp_bound(v, cmp, r, d))
+                    tightened = true;
             }
         }
         return tightened;
@@ -657,8 +658,16 @@ namespace nla {
     /**
      * Ensure that bounds are integral when the variable is integer.
      */
-    void monomial_bounds::propagate_lp_bound(lpvar v, lp::lconstraint_kind cmp, rational const &q, u_dependency *d) {
+    bool monomial_bounds::propagate_lp_bound(lpvar v, lp::lconstraint_kind cmp, rational const &q, u_dependency *d) {
         SASSERT(cmp != llc::EQ && cmp != llc::NE);
+        // Global cap on derived-bound magnitude. Interval up-propagation can
+        // double the bit-width of bounds at every propagation round (a product
+        // bound is the product of factor bounds, which may themselves be
+        // derived); unchecked this ends in single mpn multiplications so large
+        // that even the -T watchdog cannot preempt them.
+        unsigned const max_bits = c().params().arith_nl_propagate_row_bounds_max_bits();
+        if (max_bits > 0 && q.bitsize() > max_bits)
+            return false;
         if (!c().var_is_int(v))
             c().lra.update_column_type_and_bound(v, cmp, q, d);
         else if (q.is_int()) {
@@ -673,6 +682,7 @@ namespace nla {
             c().lra.update_column_type_and_bound(v, llc::GE, ceil(q), d);
         else
             c().lra.update_column_type_and_bound(v, llc::LE, floor(q), d);
+        return true;
     }
 
     bool monomial_bounds::tighten_lp_bound(dep_interval const &range, lpvar v, unsigned power) {
@@ -748,6 +758,156 @@ namespace nla {
         return propagated;
     }
 
+    namespace {
+        // Minimal consumer for lar_solver::calculate_implied_bounds_for_row:
+        // accepts only bounds that improve a column of interest.
+        struct nl_row_bound_imp {
+            lp::lar_solver&         m_lp;
+            indexed_uint_set const& m_relevant;
+            // When false, only bounds for sides the column lacks entirely are
+            // accepted; when true, improvements of existing bounds also pass.
+            bool                    m_allow_improvements = false;
+            nl_row_bound_imp(lp::lar_solver& l, indexed_uint_set const& r) : m_lp(l), m_relevant(r) {}
+            lp::lar_solver& lp() { return m_lp; }
+            const lp::lar_solver& lp() const { return m_lp; }
+            bool bound_is_interesting(unsigned j, lp::lconstraint_kind kind, const lp::mpq& v) const {
+                if (!m_relevant.contains(j))
+                    return false;
+                switch (kind) {
+                case lp::lconstraint_kind::GE:
+                case lp::lconstraint_kind::GT:
+                    if (!m_lp.column_has_lower_bound(j))
+                        return true;
+                    return m_allow_improvements && v > m_lp.get_lower_bound(j).x;
+                case lp::lconstraint_kind::LE:
+                case lp::lconstraint_kind::LT:
+                    if (!m_lp.column_has_upper_bound(j))
+                        return true;
+                    return m_allow_improvements && v < m_lp.get_upper_bound(j).x;
+                default:
+                    return false;
+                }
+            }
+        };
+    }
+
+    /**
+       \brief Assert row-implied bounds of nonlinear-relevant columns as LP
+       column bounds.
+
+       This is the one-sided generalization of propagate_fixed_rows, and the
+       nla counterpart of theory_arith's implied-bound propagation: solver 2
+       asserts a bound derived from a row (say, x <= 2^32 - 1 out of the row
+       of (< (mod a p) p) once p is fixed at 2^32) directly into its tableau,
+       where it feeds the interval engine, bounds the monomials containing x,
+       and lets a plain farkas conflict refute the query without Grobner,
+       Horner or nlsat. theory_lra only turns implied bounds into literals
+       when a matching atom exists, so without this pass such bounds never
+       reach the LP columns and interval propagation of products starves.
+
+       Only columns occurring in a monomial are touched, mirroring
+       propagate_fixed_rows: the point is enabling nonlinear reasoning, not
+       general bound strengthening.
+    */
+    bool monomial_bounds::propagate_row_implied_bounds(bool incremental) {
+        if (!c().params().arith_nl_propagate_row_bounds())
+            return false;
+        auto& lra = c().lra;
+
+        // At a final check, restrict attention to the monomials that are
+        // violated in the current model: their variables and factors are the
+        // columns whose missing bounds starve interval propagation, and the
+        // rows adjacent to those columns are where the bounds are implied
+        // (e.g. the row of (< (mod a p) p) implies mod <= 2^32 - 1 once p is
+        // fixed at 2^32). During search (incremental) the trigger is instead
+        // a column whose bounds changed since the last propagation - the same
+        // trigger theory_arith uses - and the candidate columns are all
+        // monomial variables and factors.
+        indexed_uint_set nl_vars;
+        indexed_uint_set rows;
+        if (incremental) {
+            for (auto const& m : c().emons()) {
+                nl_vars.insert(m.var());
+                for (lpvar k : m.vars())
+                    nl_vars.insert(k);
+            }
+            for (lpvar j : c().m_columns_with_changed_bounds) {
+                if (j >= lra.column_count())
+                    continue;
+                for (auto const& cell : lra.A_r().m_columns[j])
+                    rows.insert(cell.var());
+            }
+        }
+        else {
+            for (lpvar v : c().m_to_refine) {
+                auto const& m = c().emons()[v];
+                nl_vars.insert(m.var());
+                for (lpvar k : m.vars())
+                    nl_vars.insert(k);
+            }
+            for (lpvar j : nl_vars)
+                for (auto const& cell : lra.A_r().m_columns[j])
+                    rows.insert(cell.var());
+        }
+        if (rows.empty())
+            return false;
+
+        // Two escalation levels. Level 1 only fills in sides the columns lack
+        // altogether - the least invasive repair of starved interval
+        // propagation, and usually all that effectively-linear problems need.
+        // Only when that yields nothing does level 2 also assert improvements
+        // of existing bounds, which drives the full cascade (factor bounds ->
+        // product bounds -> farkas) at the price of perturbing the search.
+        nl_row_bound_imp imp(lra, nl_vars);
+        std_vector<lp::implied_bound> ibounds;
+        bool propagated = false;
+        for (bool allow_improvements : { false, true }) {
+            // The incremental variant never escalates: during search only the
+            // level-1 repairs (missing-side bounds out of fixed-anchored rows)
+            // are quiet enough to assert on every propagation round.
+            if (allow_improvements && (incremental || !c().params().arith_nl_propagate_row_bounds_improve()))
+                break;
+            imp.m_allow_improvements = allow_improvements;
+            ibounds.clear();
+            lp::lp_bound_propagator<nl_row_bound_imp> bp(imp, ibounds);
+            bp.init();
+            for (unsigned i : rows) {
+                // At the default level only rows anchored by a fixed column are
+                // analyzed: a fixed factor (a pow2 constant, a determined
+                // length) is what turns the row into a bound on the remaining
+                // nonlinear column - the linearization signature this pass is
+                // after. Rows without a fixed column mostly contribute noise.
+                if (!allow_improvements) {
+                    bool has_fixed = false;
+                    for (auto const& cell : lra.get_row(i))
+                        if (lra.column_is_fixed(cell.var())) {
+                            has_fixed = true;
+                            break;
+                        }
+                    if (!has_fixed)
+                        continue;
+                }
+                lra.calculate_implied_bounds_for_row(i, bp);
+            }
+
+            for (auto const& ib : ibounds) {
+                lpvar j = ib.m_j;
+                // For term slack columns m_j is a term index, not a column;
+                // those never pass the nl_vars filter, but be defensive anyway.
+                if (j >= lra.column_count() || !nl_vars.contains(j))
+                    continue;
+                u_dependency* d = ib.explain_implied();
+                if (!propagate_lp_bound(j, ib.kind(), ib.m_bound, d))
+                    continue;
+                ++c().lra.settings().stats().m_nla_propagate_row_bounds;
+                propagated = true;
+            }
+            if (propagated)
+                break;
+        }
+        return propagated;
+    }
+
     // ================================================================
     // max_min: incremental LP bound optimization.
     //

src/math/lp/monomial_bounds.h

@@ -22,7 +22,7 @@ namespace nla {
         bool tighten_lp_lower_bound(dep_interval const& range, lpvar v, unsigned p);
         bool tighten_lp_bound(dep_interval &mi, lpvar v, unsigned power, dep_interval &product);
  
-        void propagate_lp_bound(lpvar v, lp::lconstraint_kind cmp, rational const &q, u_dependency *d);
+        bool propagate_lp_bound(lpvar v, lp::lconstraint_kind cmp, rational const &q, u_dependency *d);
 
 
         bool should_propagate_lower(dep_interval const& range, lpvar v, unsigned p);
@@ -91,6 +91,7 @@ namespace nla {
         bool propagate_linear_bounds();
         bool propagate_changed_bounds();
         bool propagate_fixed_rows();
+        bool propagate_row_implied_bounds(bool incremental);
 
         // Maximize (is_lower == false) or minimize (is_lower == true) column j
         // over the LP tableau and, if the resulting bound improves j's current

src/math/lp/nla_core.cpp

@@ -45,9 +45,10 @@ core::core(lp::lar_solver& s, params_ref const& p, reslimit & lim) :
      m_nlsat_delay_bound = lp_settings().nlsat_delay();
      lra.m_find_monics_with_changed_bounds_func = [&](const indexed_uint_set& columns_with_changed_bounds) {
         for (lpvar j : columns_with_changed_bounds) {
+            m_columns_with_changed_bounds.insert(j);
             if (is_monic_var(j))
                 m_monics_with_changed_bounds.insert(j);
-            for (const auto & m: m_emons.get_use_list(j)) 
+            for (const auto & m: m_emons.get_use_list(j))
                 m_monics_with_changed_bounds.insert(m.var());
         }
     };
@@ -648,7 +649,7 @@ void core::init_to_refine() {
     unsigned r = random(), sz = m_emons.number_of_monics();
     for (unsigned k = 0; k < sz; ++k) {
         auto const & m = *(m_emons.begin() + (k + r)% sz);
-        if (!check_monic(m)) 
+        if (!check_monic(m))
             insert_to_refine(m.var());
     }
     
@@ -1185,9 +1186,11 @@ void core::patch_monomial(lpvar j) {
     // We could not patch j, now we try patching the factor variables.
     TRACE(nla_solver, tout << " trying squares\n";);
     // handle perfect squares
-    if ((*m_patched_monic).vars().size() == 2 && (*m_patched_monic).vars()[0] == (*m_patched_monic).vars()[1]) {        
+    if ((*m_patched_monic).vars().size() == 2 && (*m_patched_monic).vars()[0] == (*m_patched_monic).vars()[1]) {
         rational root;
-        if (v.is_perfect_square(root)) {
+        // is_perfect_square multiplies numbers of v's magnitude; on the huge
+        // values that bound propagation can produce it dominates the run time.
+        if (v.bitsize() <= 256 && v.is_perfect_square(root)) {
             m_patched_var = (*m_patched_monic).vars()[0];
             if (!var_breaks_correct_monic(m_patched_var) && (try_to_patch(root) || try_to_patch(-root))) { 
                 TRACE(nla_solver, tout << "patched square\n";);
@@ -1305,14 +1308,24 @@ lbool core::check(unsigned level) {
 
     init_to_refine();
     patch_monomials();
-    set_use_nra_model(false);    
+    set_use_nra_model(false);
     if (m_to_refine.empty())
-        return l_true;    
+        return l_true;
     init_search();
     m_nla_satisfied = false;
 
     lbool ret = l_undef;
-    bool run_grobner = need_run_grobner();
+    // Optionally defer the Grobner basis while bound propagation is still
+    // delivering: solver 2 never reaches its Grobner strategy on
+    // effectively-linear problems because interval propagation reports
+    // progress at every call. The deferral cuts Grobner invocations ~7x and
+    // the seed-tail ~40% on the F* UInt128 family, but it also starves the
+    // Grobner lemmas that alone close Pulse.Lib.ForEvery-1 (a query solver 2
+    // cannot solve at all), so it is opt-in rather than default.
+    bool bounds_active = m_bounds_progress_since_check > 0 &&
+                         params().arith_nl_grobner_defer_on_bounds_progress();
+    m_bounds_progress_since_check = 0;
+    bool run_grobner = need_run_grobner() && !bounds_active;
     bool run_horner = need_run_horner();
     bool run_bounds = params().arith_nl_branching();
 
@@ -1323,8 +1336,21 @@ lbool core::check(unsigned level) {
 
     if (no_effect() && refine_pseudo_linear())
         return l_false;
-       
-    
+
+    // Pre-empt the lemma machinery when the violated monomials carry the
+    // effectively-linear signature. The pass itself is the detector: at its
+    // default level it only asserts bounds for sides a column lacks entirely,
+    // implied by rows anchored on a fixed column (a pow2 constant, a
+    // determined length). When such bounds exist - the situation solver 2
+    // handles by pure bound propagation - asserting them and letting the
+    // simplex continue beats deriving Grobner/Horner lemmas over the same
+    // fixed constants. When the pass asserts nothing, the machinery below
+    // runs exactly as before.
+    if (no_effect() && m_monomial_bounds.propagate_row_implied_bounds(false)) {
+        m_check_feasible = true;
+        return l_false;
+    }
+
     {
         std::function<void(void)> check1 = [&]() { if (no_effect() && run_horner) m_horner.horner_lemmas(); };
         std::function<void(void)> check2 = [&]() { if (no_effect() && run_grobner) m_grobner(); };
@@ -1430,10 +1456,15 @@ lbool core::bounded_nlsat() {
     p.set_uint("max_conflicts", lp_settings().m_max_conflicts);            
     m_nra.updt_params(p);
     lp_settings().stats().m_nra_calls++;
-    if (ret == l_undef) 
-        ++m_nlsat_delay_bound;
+    if (ret == l_undef) {
+        // Exponential backoff: a query that bounded nlsat cannot decide within
+        // its conflict budget tends to stay undecidable on the next model as
+        // well; a linear delay lets the search sink seconds into repeated
+        // fruitless nlsat calls (each one costs up to 100 conflicts).
+        m_nlsat_delay_bound = m_nlsat_delay_bound == 0 ? 4 : std::min(2 * m_nlsat_delay_bound, 1u << 20);
+    }
     else if (m_nlsat_delay_bound > 0)
-        m_nlsat_delay_bound /= 2;        
+        m_nlsat_delay_bound /= 2;
     
     m_nlsat_delay = m_nlsat_delay_bound;
 
@@ -1545,9 +1576,10 @@ bool core::propagate() {
         propagated = true;
     if (m_monomial_bounds.tighten_lp_bounds())
 		propagated = true;
-    if (m_monomial_bounds.propagate_changed_bounds()) 
+    if (m_monomial_bounds.propagate_changed_bounds())
         propagated = true;
     m_monics_with_changed_bounds.reset();
+    m_columns_with_changed_bounds.reset();
     if (propagated)
         m_check_feasible = true;
     return propagated;
@@ -1556,12 +1588,17 @@ bool core::propagate() {
 bool core::incremental_propagate() {
     bool propagated = false;
     clear();
+    if (m_monomial_bounds.propagate_row_implied_bounds(true)) {
+        propagated = true;
+        ++m_bounds_progress_since_check;
+    }
     if (m_monomial_bounds.propagate_changed_bounds())
         propagated = true;
     m_monics_with_changed_bounds.reset();
+    m_columns_with_changed_bounds.reset();
     if (propagated)
         m_check_feasible = true;
-    return propagated;    
+    return propagated;
 }
 
 /**

src/math/lp/nla_core.h

@@ -80,6 +80,12 @@ class core {
     vector<lp::fixed_equality> m_fixed_equalities;
     indexed_uint_set         m_to_refine;
     indexed_uint_set         m_monics_with_changed_bounds;
+    indexed_uint_set         m_columns_with_changed_bounds;
+    // Bound-propagation progress (incremental or pre-check) accumulated since
+    // the last final check; while non-zero, the Grobner basis is deferred,
+    // mirroring solver 2, whose strategy ladder never advances past interval
+    // propagation as long as it keeps deriving bounds.
+    unsigned                 m_bounds_progress_since_check = 0;
     tangents                 m_tangents;
     basics                   m_basics;
     order                    m_order;

src/math/lp/nla_grobner.cpp

@@ -375,6 +375,16 @@ namespace nla {
         eval.var2val() = [&](unsigned j) { return val(j); };
         if (eval(p) == 0)
             return false;
+        // Divisibility and quotient branching is effective for small moduli but
+        // hopeless for huge ones: a residue lemma modulo 2^32 (coefficients of
+        // that scale typically enter the polynomial by substitution of fixed
+        // power-of-two constants) refutes just the current model out of billions
+        // and only churns the search. Skip when any coefficient is that large.
+        unsigned const max_bits = c().params().arith_nl_grobner_quotient_max_bits();
+        if (max_bits > 0)
+            for (auto const& mn : p)
+                if (mn.coeff.bitsize() > max_bits)
+                    return false;
         TRACE(grobner, tout << "propagate_quotients " << p << "\n");
         tracked_uint_set nl_vars;
         rational d(1);
@@ -996,6 +1006,16 @@ namespace nla {
         }
     }
 
+    // A fixed variable is substituted by its value only when the value is small.
+    // Substituting huge constants (e.g. 2^32 from pow2 tables) drives the basis
+    // computation into large-coefficient arithmetic; such variables stay symbolic.
+    bool grobner::fixed_value_is_small(lpvar j) const {
+        unsigned max_bits = c().params().arith_nl_grobner_subs_fixed_max_bits();
+        if (max_bits == 0)
+            return true;
+        return lra.column_lower_bound(j).x.bitsize() <= max_bits;
+    }
+
     const rational& grobner::val_of_fixed_var_with_deps(lpvar j, u_dependency*& dep) {
         auto* d = lra.get_bound_constraint_witnesses_for_column(j);
         if (d)
@@ -1024,7 +1044,7 @@ namespace nla {
                 dep = zero_dep;
                 return r;
             }
-            if (c().params().arith_nl_grobner_subs_fixed() == 1 && c().var_is_fixed(j))
+            if (c().params().arith_nl_grobner_subs_fixed() == 1 && c().var_is_fixed(j) && fixed_value_is_small(j))
                 r *= val_of_fixed_var_with_deps(j, dep);
             else if (m_config.m_expand_terms && c().lra.column_has_term(j))
                 r *= pdd_expr(c().lra.get_term(j), dep);

src/math/lp/nla_grobner.h

@@ -97,6 +97,7 @@ namespace nla {
         bool is_solved(dd::pdd const& p, unsigned& v, dd::pdd& r);
         void add_eq(dd::pdd& p, u_dependency* dep);        
         bool is_pseudo_linear(monic const& m) const;
+        bool fixed_value_is_small(lpvar j) const;
         const rational& val_of_fixed_var_with_deps(lpvar j, u_dependency*& dep);
         dd::pdd pdd_expr(const rational& c, lpvar j, u_dependency*& dep);  
         dd::pdd pdd_expr(lp::lar_term const& t, u_dependency*& dep);

src/params/smt_params_helper.pyg

@@ -87,11 +87,14 @@ def_module_params(module_name='smt',
                           ('arith.nl.grobner_max_simplified', UINT, 10000, 'grobner\'s maximum number of simplifications'),
                           ('arith.nl.grobner_cnfl_to_report', UINT, 1, 'grobner\'s maximum number of conflicts to report'),
                           ('arith.nl.grobner_propagate_quotients', BOOL, True, 'detect conflicts x*y + z = 0 where x doesn\'t divide z'),
+                          ('arith.nl.grobner_quotient_max_bits', UINT, 0, 'skip quotient/mod-residue lemmas when a polynomial coefficient exceeds this bit-size (0 = no limit); huge moduli make divisibility branching unproductive'),
                           ('arith.nl.grobner_gcd_test', BOOL, True, 'detect gcd conflicts for polynomial powers x^k - y = 0'),
                           ('arith.nl.grobner_exp_delay', BOOL, True, 'use exponential delay between grobner basis attempts'),
+                          ('arith.nl.grobner_defer_on_bounds_progress', BOOL, False, 'defer the grobner basis while nonlinear bound propagation is still making progress between final checks; mirrors the legacy solver, which never reaches grobner while interval propagation delivers; reduces seed-tail latency on effectively-linear problems at the price of starving grobner-dependent queries'),
                           ('arith.nl.grobner_adaptive', BOOL, False, 'scale grobner growth knobs (eqs/size/degree/max_simplified) up on productive runs and down on misses'),
                           ('arith.nl.gr_q', UINT, 10, 'grobner\'s quota'),
-                          ('arith.nl.grobner_subs_fixed', UINT, 1, '0 - no subs, 1 - substitute, 2 - substitute fixed zeros only'),   
+                          ('arith.nl.grobner_subs_fixed', UINT, 1, '0 - no subs, 1 - substitute, 2 - substitute fixed zeros only'),
+                          ('arith.nl.grobner_subs_fixed_max_bits', UINT, 0, 'with grobner_subs_fixed=1, substitute a non-zero fixed variable only when the bit-size of its value is at most this bound (0 = no limit); larger fixed values stay symbolic to avoid large-coefficient growth in the basis'),
                           ('arith.nl.grobner_expand_terms', BOOL, True, 'expand terms before computing grobner basis'),
                           ('arith.nl.grobner_perfect_squares', BOOL, True, 'expand perfect squares with Grobner'),
                           ('arith.nl.monomial_sandwich', BOOL, False, 'derive bound on a monomial factor by pairing two LP rows that share the other factor'),
@@ -101,7 +104,12 @@ def_module_params(module_name='smt',
                           ('arith.nl.delay', UINT, 10, 'number of calls to final check before invoking bounded nlsat check'),
                           ('arith.nl.propagate_linear_monomials', BOOL, True, 'propagate linear monomials'),
                           ('arith.nl.optimize_bounds', BOOL, True, 'enable bounds optimization'),
-                          ('arith.nl.propagate_fixed_rows', BOOL, False, 'scan LP rows for fixed variables'), 
+                          ('arith.nl.propagate_fixed_rows', BOOL, False, 'scan LP rows for fixed variables'),
+                          ('arith.nl.propagate_row_bounds', BOOL, True, 'assert row-implied bounds of variables occurring in nonlinear monomials as LP column bounds; lets interval propagation bound products and linearize without running grobner/horner/nlsat'),
+                          ('arith.nl.propagate_row_bounds_max_bits', UINT, 256, 'do not assert a derived bound whose value exceeds this bit-size; caps the multiplicative growth of derived bounds (0 = no limit)'),
+                          ('arith.nl.propagate_row_bounds_improve', BOOL, False, 'when row-implied bound propagation finds no missing-side bounds, also assert improvements of existing bounds; drives the full bound cascade so the F*-style effectively-linear queries refute without grobner/horner/nlsat, at the price of perturbing searches that were healthy'),
+                          ('arith.nl.linear_probe', BOOL, False, 'before the main SMT search, probe the query with a short bounds-only solver (no grobner/horner/nlsat, row-implied bound propagation with improvements); decides effectively-linear nonlinear queries at a fraction of the cost, falls through to the unchanged main search otherwise'),
+                          ('arith.nl.linear_probe_timeout', UINT, 300, 'wall-clock budget of the bounds-only linear probe, in milliseconds'),
                           ('arith.nl.optimize_bounds_lp_max_vars', UINT, 120, 'skip LP-based nonlinear bounds optimization when the number of candidate monomial variables exceeds this threshold (0 = unlimited)'),
                           ('arith.nl.cross_nested', BOOL, True, 'enable cross-nested consistency checking'),
                           ('arith.nl.log', BOOL, False, 'Log lemmas sent to nra solver'),

src/smt/smt_solver.cpp

@@ -28,6 +28,8 @@ Notes:
 #include "params/smt_params_helper.hpp"
 #include "solver/solver_na2as.h"
 #include "solver/mus.h"
+#include "util/cancel_eh.h"
+#include "util/scoped_timer.h"
 
 #include <algorithm>
 
@@ -71,12 +73,17 @@ namespace {
         unsigned             m_core_extend_patterns_max_distance;
         bool                 m_core_extend_nonlocal_patterns;
         obj_map<expr, expr*> m_name2assertion;
+        // bounds-only linear probe (arith.nl.linear_probe)
+        expr_ref_vector         m_probe_core;
+        model_ref               m_probe_model;
+        bool                    m_result_from_probe = false;
 
     public:
         smt_solver(ast_manager & m, params_ref const & p, symbol const & l) :
             solver_na2as(m),
             m_smt_params(p),
             m_context(m, m_smt_params),
+            m_probe_core(m),
             m_cuber(nullptr),
             m_minimizing_core(false),
             m_core_extend_patterns(false),
@@ -163,6 +170,7 @@ namespace {
         }
 
         void assert_expr_core(expr * t) override {
+            reset_probe();
             m_context.assert_expr(t);
         }
         void set_phase(expr* e) override { m_context.set_phase(e); }
@@ -181,10 +189,12 @@ namespace {
         }
 
         void push_core() override {
+            reset_probe();
             m_context.push();
         }
 
         void pop_core(unsigned n) override {
+            reset_probe();
             unsigned cur_sz = m_assumptions.size();
             if (n > 0 && cur_sz > 0) {
                 unsigned lvl = m_scopes.size();
@@ -202,8 +212,85 @@ namespace {
             m_context.pop(n);
         }
 
+        void reset_probe() {
+            m_probe_core.reset();
+            m_probe_model = nullptr;
+            m_result_from_probe = false;
+        }
+
+        // A short bounds-only probe on a throwaway kernel: solver 6 with the
+        // nonlinear lemma machinery (Grobner, Horner, nlsat) disabled, so only
+        // linear reasoning, linearization of fixed-factor monomials and
+        // row-implied bound tightening act. Effectively-linear queries are
+        // decided here at a fraction of the cost of the main search and with
+        // none of its seed variance; anything else fails fast (there is
+        // nothing expensive left to run) and the main search starts unchanged.
+        lbool try_nl_linear_probe(unsigned num_assumptions, expr * const * assumptions) {
+            reset_probe();
+            smt_params_helper ph(get_params());
+            if (!ph.arith_nl_linear_probe())
+                return l_undef;
+            if (m.proofs_enabled())
+                return l_undef;
+            params_ref pp;
+            pp.copy(get_params());
+            pp.set_bool("arith.nl.linear_probe", false);
+            pp.set_uint("arith.solver", 6);
+            pp.set_bool("arith.nl.grobner", false);
+            pp.set_bool("arith.nl.horner", false);
+            pp.set_bool("arith.nl.nra", false);
+            pp.set_bool("arith.nl.nra_check_assignment", false);
+            pp.set_bool("arith.nl.propagate_row_bounds_improve", true);
+
+            // The probe lives in its own ast_manager: preprocessing inside a
+            // shared manager would allocate nodes and shift ast identifiers,
+            // silently changing the tie-breaking of the main search that runs
+            // after a failed probe. With a separate manager the main search is
+            // bit-identical to a run without the probe.
+            // ast_translation's constructor copies the plugin families with
+            // aligned family ids; the target manager must start bare.
+            ast_manager pm(PGM_DISABLED);
+            ast_translation to_probe(m, pm);
+            scoped_ptr<smt_params> fp = alloc(smt_params, pp);
+            smt::kernel probe(pm, *fp, pp);
+            if (m_logic != symbol::null)
+                probe.set_logic(m_logic);
+            ptr_vector<expr> fmls;
+            m_context.get_context().get_asserted_formulas(fmls);
+            for (expr* f : fmls)
+                probe.assert_expr(to_probe(f));
+            expr_ref_vector pas(pm);
+            for (unsigned i = 0; i < num_assumptions; ++i)
+                pas.push_back(to_probe(assumptions[i]));
+            lbool r;
+            {
+                cancel_eh<reslimit> eh(pm.limit());
+                scoped_timer timer(ph.arith_nl_linear_probe_timeout(), &eh);
+                r = probe.check(pas.size(), pas.data());
+            }
+            if (r == l_undef)
+                return l_undef;
+            ast_translation from_probe(pm, m);
+            if (r == l_false) {
+                unsigned sz = probe.get_unsat_core_size();
+                for (unsigned i = 0; i < sz; ++i)
+                    m_probe_core.push_back(from_probe(probe.get_unsat_core_expr(i)));
+            }
+            else {
+                model_ref pmdl;
+                probe.get_model(pmdl);
+                if (pmdl)
+                    m_probe_model = pmdl->translate(from_probe);
+            }
+            m_result_from_probe = true;
+            return r;
+        }
+
         lbool check_sat_core2(unsigned num_assumptions, expr * const * assumptions) override {
             TRACE(solver_na2as, tout << "smt_solver::check_sat_core:\n"; for (unsigned i = 0; i < num_assumptions; ++i) tout << mk_pp(assumptions[i], m) << "\n";);
+            lbool r = try_nl_linear_probe(num_assumptions, assumptions);
+            if (r != l_undef)
+                return r;
             return m_context.check(num_assumptions, assumptions);
         }
 
@@ -373,6 +460,10 @@ namespace {
         };
 
         void get_unsat_core(expr_ref_vector & r) override {
+            if (m_result_from_probe) {
+                r.append(m_probe_core);
+                return;
+            }
 
             unsigned sz = m_context.get_unsat_core_size();
             for (unsigned i = 0; i < sz; ++i) {
@@ -397,7 +488,10 @@ namespace {
         }
 
         void get_model_core(model_ref & m) override {
-            m_context.get_model(m);
+            if (m_result_from_probe)
+                m = m_probe_model;
+            else
+                m_context.get_model(m);
         }
 
         proof * get_proof_core() override {

src/smt/tactic/CMakeLists.txt

@@ -1,12 +1,14 @@
 z3_add_component(smt_tactic
   SOURCES
     ctx_solver_simplify_tactic.cpp
+    nl_linear_probe_tactic.cpp
     smt_tactic_core.cpp
     unit_subsumption_tactic.cpp
   COMPONENT_DEPENDENCIES
     smt
   TACTIC_HEADERS
     ctx_solver_simplify_tactic.h
+    nl_linear_probe_tactic.h
     smt_tactic_core.h
     unit_subsumption_tactic.h
 )

src/smt/tactic/nl_linear_probe_tactic.cpp

@@ -0,0 +1,38 @@
+/*++
+Copyright (c) 2026 Microsoft Corporation
+
+Module Name:
+
+    nl_linear_probe_tactic.cpp
+
+Abstract:
+
+    See nl_linear_probe_tactic.h.
+
+Author:
+
+    Lev Nachmanson (levnach) 2026-08-06
+
+--*/
+#include "smt/tactic/nl_linear_probe_tactic.h"
+#include "smt/tactic/smt_tactic_core.h"
+#include "tactic/tactical.h"
+
+tactic * mk_nl_linear_probe_tactic(ast_manager & m, params_ref const & p) {
+    // The probe: solver 6 restricted to its linear machinery. Grobner,
+    // Horner and nlsat are off; row-implied bound propagation is allowed to
+    // improve existing bounds, which drives the factor-bounds -> product
+    // bounds -> farkas cascade to completion on effectively-linear queries.
+    params_ref probe_p = p;
+    probe_p.set_uint("arith.solver", 6);
+    probe_p.set_bool("arith.nl.grobner", false);
+    probe_p.set_bool("arith.nl.horner", false);
+    probe_p.set_bool("arith.nl.nra", false);
+    probe_p.set_bool("arith.nl.nra_check_assignment", false);
+    probe_p.set_bool("arith.nl.propagate_row_bounds_improve", true);
+
+    unsigned timeout_ms = p.get_uint("probe_timeout", 300);
+
+    return or_else(try_for(using_params(mk_smt_tactic_core(m), probe_p), timeout_ms),
+                   mk_smt_tactic_core(m, p));
+}

src/smt/tactic/nl_linear_probe_tactic.h

@@ -0,0 +1,39 @@
+/*++
+Copyright (c) 2026 Microsoft Corporation
+
+Module Name:
+
+    nl_linear_probe_tactic.h
+
+Abstract:
+
+    A short bounds-only probe for nonlinear arithmetic followed by the
+    regular SMT tactic.
+
+    The probe runs the SMT solver with every nonlinear lemma mechanism
+    disabled (no Grobner, no Horner, no nlsat): only linear reasoning,
+    linearization of monomials with fixed factors, and row-implied bound
+    tightening act. On effectively-linear problems - monomials whose
+    factors are pinned by fixed constants, as in bit-level arithmetic
+    over power-of-two limbs - this decides the query at a fraction of
+    the cost and with none of the seed variance of the lemma machinery;
+    when bound reasoning cannot decide the query the probe fails fast
+    and the unchanged default SMT tactic runs on a fresh solver.
+
+Author:
+
+    Lev Nachmanson (levnach) 2026-08-06
+
+--*/
+#pragma once
+
+#include "util/params.h"
+
+class ast_manager;
+class tactic;
+
+tactic * mk_nl_linear_probe_tactic(ast_manager & m, params_ref const & p = params_ref());
+
+/*
+  ADD_TACTIC("nl-linear-probe", "short bounds-only linear probe for nonlinear arithmetic, falling back to the smt tactic.", "mk_nl_linear_probe_tactic(m, p)")
+*/