Improvements to NLA lemmas (#9391)

* Add dual-row shared-factor sandwich for NLA bound propagation

When enabled via arith.nl.monomial_sandwich (default off), monomial_bounds
finds LP term columns whose term has shape  a_m * m + a_v * v  with exactly
two variables — both factors of a binary monomial m = u*v. The term column's
bound bounds (a_m * m + a_v * v); substituting m = u*v gives v * (a_m*u + a_v),
and sign-aware interval division by v plus an affine shift yields a numeric
bound on u. The derived interval is fed to the existing propagate_value path
so the lemma channel and integer rounding logic are shared with the rest of
NLA's forward/backward propagation; no new emit code.

Catches conflicts of the form
  α_v1 * v + α_m * m ≥ k1
  α_v2 * v + α_m * m ≤ k2
that today require nlsat (when no single row alone yields infeasibility but
their conjunction tightly bounds u after factoring v).

Scope: binary monomials only (m.size()==2, no squares); cap of 16 term-columns
scanned per call; one lemma per (u,v) attempt to keep the lemma channel quiet.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

* Add arith.nl.order.binomial_sign flag (default true)

Granular gate for order_lemma_on_binomial_sign — the only order family that
embeds a model-snapshot literal (x ≷ val(x)) in the lemma body. Disabling it
keeps the always-good structural mon-ol family running while removing the
SAT-splitter shape that cascades under model perturbations (e.g., from
arith.nl.monomial_sandwich tightening factor bounds).

Default true preserves master behaviour; the flag is intended as an
experimental knob to measure how much of an observed cascade is specifically
attributable to the binomial-sign splitter vs. the structural cancellation
lemmas in the same module.

See ord-binom-opportunities.md for the full gap analysis and the
deterministic-replacement directions (sandwich, McCormick) that would let
this flag eventually default to false without regressing leaves where
ord-binom currently carries the proof.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

* Add sign-pinned binomial bound for NLA (Opportunity 1 from ord-binom doc)

When enabled via arith.nl.monomial_binomial_sign (default off), monomial_bounds
adds a third pass alongside propagate_down (existing) and propagate_shared_factor
(sandwich). For a binary monomial m = u*v in m_to_refine whose model value mv
disagrees with val(u)*val(v), and where v has a determined sign:

  1. synthesize a one-sided interval for m.var() at mv (no deps; the snapshot
     enters as a literal in the lemma body, not as an antecedent)
  2. divide by v's interval (sign-aware via dep.div<with_deps>) to get a
     deterministic interval for u
  3. emit a propagate_value-style lemma whose body is
        m.var() < mv (or > mv) ∨ u-bound
     conditioned on v's bound witness

Targets the case ord-binom currently handles: factors have determined signs,
m.var() may have no LP bound. The clause is sound modulo the monomial
definition (same condition propagate_down, propagate_shared_factor, and
ord-binom already rely on).

A new throttle kind MONOMIAL_BINOMIAL_SIGN keyed on (m.var, u, v, direction)
prevents cascading: without it, each new val(m.var()) snapshot would re-emit
across model changes the same way ord-binom does.

Validated via smt.arith.validate=true: 0 soundness errors across the
32-leaf test corpus.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

* Add McCormick box-corner tangent points (Opportunity 2 from ord-binom doc)

When enabled via arith.nl.tangents.box_corners (default off, sub-flag of
arith.nl.tangents), tangent_imp::get_points selects m_a, m_b at the corners
of the bound box [x_lo, x_hi] × [y_lo, y_hi] instead of the model-centered
points val(x) ± delta. The selection follows the classical McCormick
under/over envelope:

  - m_below=true (under-approximation):
      m_a = (x_lo, y_lo),  m_b = (x_hi, y_hi)
  - m_below=false (over-approximation):
      m_a = (x_lo, y_hi),  m_b = (x_hi, y_lo)

The existing generate_plane already produces the McCormick linear form
xy ≷ pl.y·x + pl.x·y − pl.x·pl.y at any chosen point pl. push_point is
skipped in box-corner mode: corners are extremes, so doubling the offset
moves out of the box and would invalidate the McCormick property.

Falls back to the existing model-driven point selection when either factor
has an unbounded side or the box is degenerate (single-point in a
dimension).

Soundness — non-strict inequality at corners. The classical model-driven
flow uses pl strictly in the interior of the box, so generate_plane emits
xy > T (strict). At the box corners the tangent meets the surface along
the box's edges (xy = T when x = pl.x or y = pl.y), so the strict
inequality is violated by any model with x at the box boundary. A new
m_pl_strict_interior member, set false on a successful set_box_corners(),
switches generate_plane's emission to ≥/≤ (non-strict). The model-driven
path keeps strict — its push_point + plane_is_correct_cut chain already
guarantees pl is interior.

Validated via smt.arith.validate=true: 0 validate_conflict() failures
across the 32-leaf test corpus with box_corners=true.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

---------

Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

src/math/lp/monomial_bounds.cpp

@@ -312,6 +312,12 @@ namespace nla {
             }
             dep.mul<dep_intervals::with_deps>(product, vi, product);
         }
+        if (do_propagate_down && c().params().arith_nl_monomial_sandwich() &&
+            propagate_shared_factor(m))
+            return true;
+        if (c().params().arith_nl_monomial_binomial_sign() &&
+            propagate_binomial_sign(m))
+            return true;
         return do_propagate_up && propagate_value(product, m.var());
     }
 
@@ -501,11 +507,196 @@ namespace nla {
     }
     
     lpvar monomial_bounds::non_fixed_var(monic const& m) {
-        for (lpvar v : m) 
+        for (lpvar v : m)
             if (!c().var_is_fixed(v))
                 return v;
         return null_lpvar;
     }
 
+    /**
+     * Dual-row shared-factor sandwich. For a binary monomial m = u*v, find LP
+     * term columns whose term has shape  a_m * m + a_v * v  (exactly two
+     * variables, both factors of m). The term column's bound is a sound
+     * interval for (a_m * m + a_v * v). Substituting m = u*v yields
+     * v * (a_m * u + a_v); dividing by the interval on v (sign-determined)
+     * gives an interval on (a_m * u + a_v), and an affine shift gives an
+     * interval on u. The derived interval is fed to the existing
+     * propagate_value path so the lemma channel and integer rounding are
+     * shared with the rest of the propagation pipeline.
+     */
+    bool monomial_bounds::propagate_shared_factor(monic const& m) {
+        if (m.size() != 2)
+            return false;
+        lpvar f0 = m.vars()[0], f1 = m.vars()[1];
+        if (f0 == f1)
+            return false;
+
+        unsigned const fanout_limit = c().params().arith_nl_monomial_sandwich_max_fanout();
+
+        auto try_pair = [&](lpvar u, lpvar v) -> bool {
+            // Skip if u participates in too many monomials: tightening such a
+            // factor cascades through ord-binom / monotonicity on every monic
+            // that contains it.
+            if (fanout_limit > 0) {
+                unsigned fanout = 0;
+                for (auto const& m1 : c().emons().get_use_list(u)) {
+                    (void)m1;
+                    if (++fanout > fanout_limit)
+                        return false;
+                }
+            }
+            scoped_dep_interval vi(dep);
+            var2interval(v, vi);
+            if (!dep.separated_from_zero(vi))
+                return false;
+
+            auto& lra = c().lra;
+            unsigned const ROW_CAP = 16;
+            unsigned scanned = 0;
+
+            for (auto const& cell : lra.A_r().m_columns[m.var()]) {
+                if (++scanned > ROW_CAP)
+                    break;
+                unsigned basic = lra.get_base_column_in_row(cell.var());
+                if (basic == m.var() || basic == v || basic == u)
+                    continue;
+                if (!lra.column_has_term(basic))
+                    continue;
+                auto const& term = lra.get_term(basic);
+                if (term.size() != 2 ||
+                    !term.contains(m.var()) || !term.contains(v))
+                    continue;
+
+                rational const& a_m = term.get_coeff(m.var());
+                rational const& a_v = term.get_coeff(v);
+                if (a_m.is_zero())
+                    continue;
+
+                // Term value = a_m*m + a_v*v; bound on basic bounds the term.
+                // Substituting m = u*v: term = v * (a_m*u + a_v).
+                scoped_dep_interval bi(dep);
+                var2interval(basic, bi);
+
+                scoped_dep_interval inner(dep);
+                dep.div<dep_intervals::with_deps>(bi, vi, inner);
+
+                scoped_dep_interval shift(dep);
+                dep.set_value(shift, -a_v);
+                scoped_dep_interval scaled(dep);
+                dep.add<dep_intervals::with_deps>(inner, shift, scaled);
+
+                scoped_dep_interval u_int(dep);
+                dep.mul<dep_intervals::with_deps>(rational::one() / a_m, scaled, u_int);
+
+                TRACE(nla_solver, tout << "sandwich shared-factor basic=" << basic
+                      << " m=" << m.var() << " v=" << v << " u=" << u
+                      << " a_m=" << a_m << " a_v=" << a_v << "\n";);
+
+                if (propagate_value(u_int, u))
+                    return true;  // one lemma per call to keep the channel quiet
+            }
+            return false;
+        };
+
+        return try_pair(f1, f0) || try_pair(f0, f1);
+    }
+
+    /**
+     * Sign-pinned binomial bound. For a binary monomial m = u*v in m_to_refine,
+     * use the current LP value mv = val(m.var()) as a one-sided anchor on the
+     * monomial value variable, and derive a deterministic interval for u via
+     * sign-aware division by v.
+     *
+     * Direction is chosen by the disagreement: if val(m.var()) > val(u)*val(v)
+     * the LP placed the monomial above the factor product, so we condition on
+     * "m.var() >= mv"; otherwise on "m.var() <= mv". The resulting clause is
+     * structurally analogous to a propagate_value lemma plus one extra
+     * snapshot literal on m.var(): under the asserted bounds on v, the clause
+     * reduces to a 2-disjunct (snapshot literal | factor bound).
+     *
+     * Targets the case ord-binom currently handles: factors have determined
+     * signs, m.var() may have no LP bound at all. The clause is sound modulo
+     * the monomial definition (the same condition propagate_down,
+     * propagate_shared_factor and ord-binom rely on).
+     */
+    bool monomial_bounds::propagate_binomial_sign(monic const& m) {
+        if (m.size() != 2)
+            return false;
+        lpvar f0 = m.vars()[0], f1 = m.vars()[1];
+        if (f0 == f1)
+            return false;
+
+        rational const mv = c().val(m.var());
+        rational const fp = c().val(f0) * c().val(f1);
+        if (mv == fp)
+            return false;
+        bool const below = mv > fp;            // LP placed m.var() too high
+        llc const anchor_cmp = below ? llc::LT : llc::GT;
+
+        auto try_anchor = [&](lpvar u, lpvar v) -> bool {
+            // Throttle once per (m.var(), u, v, direction) tuple. Without it
+            // each new val(m.var()) snapshot would re-emit and the search
+            // would cascade across model changes the same way ord-binom does.
+            if (c().throttle().insert_new(
+                    nla_throttle::MONOMIAL_BINOMIAL_SIGN,
+                    m.var(), u, v, below))
+                return false;
+
+            scoped_dep_interval vi(dep);
+            var2interval(v, vi);
+            if (!dep.separated_from_zero(vi))
+                return false;
+
+            // Synthesize a one-sided interval for m.var() at mv. No deps;
+            // the snapshot literal goes into the lemma body directly.
+            scoped_dep_interval mi_anchor(dep);
+            if (below) {
+                dep.set_lower(mi_anchor, mv);
+                dep.set_lower_is_inf(mi_anchor, false);
+                dep.set_lower_is_open(mi_anchor, false);
+                dep.set_upper_is_inf(mi_anchor, true);
+            } else {
+                dep.set_upper(mi_anchor, mv);
+                dep.set_upper_is_inf(mi_anchor, false);
+                dep.set_upper_is_open(mi_anchor, false);
+                dep.set_lower_is_inf(mi_anchor, true);
+            }
+
+            scoped_dep_interval u_int(dep);
+            dep.div<dep_intervals::with_deps>(mi_anchor, vi, u_int);
+
+            bool emitted = false;
+            if (should_propagate_lower(u_int, u, 1)) {
+                auto const& lower = dep.lower(u_int);
+                if (!is_too_big(lower)) {
+                    auto cmp = dep.lower_is_open(u_int) ? llc::GT : llc::GE;
+                    lp::explanation ex;
+                    dep.get_lower_dep(u_int, ex);
+                    lemma_builder lemma(c(), "binomial sign anchor");
+                    lemma &= ex;
+                    lemma |= ineq(m.var(), anchor_cmp, mv);
+                    lemma |= ineq(u, cmp, lower);
+                    emitted = true;
+                }
+            }
+            if (should_propagate_upper(u_int, u, 1)) {
+                auto const& upper = dep.upper(u_int);
+                if (!is_too_big(upper)) {
+                    auto cmp = dep.upper_is_open(u_int) ? llc::LT : llc::LE;
+                    lp::explanation ex;
+                    dep.get_upper_dep(u_int, ex);
+                    lemma_builder lemma(c(), "binomial sign anchor");
+                    lemma &= ex;
+                    lemma |= ineq(m.var(), anchor_cmp, mv);
+                    lemma |= ineq(u, cmp, upper);
+                    emitted = true;
+                }
+            }
+            return emitted;
+        };
+
+        return try_anchor(f1, f0) || try_anchor(f0, f1);
+    }
+
 }
 

src/math/lp/monomial_bounds.h

@@ -33,6 +33,8 @@ namespace nla {
         u_dependency* explain_fixed(monic const& m, rational const& k);
         lp::explanation get_explanation(u_dependency* dep);
         bool propagate_down(monic const& m, dep_interval& mi, lpvar v, unsigned power, dep_interval& product);
+        bool propagate_shared_factor(monic const& m);
+        bool propagate_binomial_sign(monic const& m);
         void analyze_monomial(monic const& m, unsigned& num_free, lpvar& free_v, unsigned& power) const;
         bool is_free(lpvar v) const;
         bool is_zero(lpvar v) const;

src/math/lp/nla_order_lemmas.cpp

@@ -81,9 +81,11 @@ void order::order_lemma_on_binomial(const monic& ac) {
   
 */
 void order::order_lemma_on_binomial_sign(const monic& xy, lpvar x, lpvar y, int sign) {
+    if (!c().params().arith_nl_order_binomial_sign())
+        return;
     if (!c().var_is_int(x) && val(x).is_big())
         return;
-    
+
 
     SASSERT(!_().mon_has_zero(xy.vars()));
     int sy = rat_sign(val(y));

src/math/lp/nla_tangent_lemmas.cpp

@@ -18,6 +18,12 @@ class tangent_imp {
     rational      m_correct_v;
     // "below" means that the incorrect value is less than the correct one, that is m_v < m_correct_v
     bool          m_below;
+    // pl is in the strict interior of the bound box (model-driven points
+    // get_initial_points + push_point); McCormick at the box corners
+    // requires non-strict inequality because the tangent meets the surface
+    // along the box's edges (xy = pl.y*x + pl.x*y - pl.x*pl.y at x = pl.x
+    // or y = pl.y).
+    bool          m_pl_strict_interior = true;
     rational      m_v; // the monomial value 
     lpvar         m_j; // the monic variable
     const monic&  m_m;
@@ -89,7 +95,10 @@ private:
         t.add_monomial(- m_y.rat_sign()*pl.x, m_jy);
         t.add_monomial(- m_x.rat_sign()*pl.y, m_jx);
         t.add_var(m_j);
-        lemma |= ineq(t, m_below? llc::GT : llc::LT, - pl.x*pl.y);
+        llc cmp = m_below
+            ? (m_pl_strict_interior ? llc::GT : llc::GE)
+            : (m_pl_strict_interior ? llc::LT : llc::LE);
+        lemma |= ineq(t, cmp, - pl.x*pl.y);
         explain(lemma);
     }
 
@@ -164,14 +173,61 @@ private:
         return a.x * m_xy.y + a.y * m_xy.x - a.x * a.y;
     }
 
+    // McCormick at box corners: choose m_a, m_b at the corners of
+    // [x_lo, x_hi] x [y_lo, y_hi] that bound xy from the side dictated by
+    // m_below. Returns false if either factor has an unbounded side, the
+    // box is degenerate, or the current LP value of a factor coincides with
+    // a chosen corner — generate_plane's negate_relation requires
+    // val(j) != corner_coord (SASSERT in debug; trivially-true literal in
+    // release). The caller falls back to the model-driven point selection in
+    // these cases.
+    bool set_box_corners() {
+        if (!c().has_lower_bound(m_jx) || !c().has_upper_bound(m_jx))
+            return false;
+        if (!c().has_lower_bound(m_jy) || !c().has_upper_bound(m_jy))
+            return false;
+        rational const& x_lo = c().get_lower_bound(m_jx);
+        rational const& x_hi = c().get_upper_bound(m_jx);
+        rational const& y_lo = c().get_lower_bound(m_jy);
+        rational const& y_hi = c().get_upper_bound(m_jy);
+        if (x_lo == x_hi || y_lo == y_hi)
+            return false;
+        // negate_relation requires the model value to be strictly separated
+        // from the corner coordinate it's compared to. If LP currently sits
+        // exactly at a box edge, fall back.
+        rational const& vx = c().val(m_jx);
+        rational const& vy = c().val(m_jy);
+        if (vx == x_lo || vx == x_hi || vy == y_lo || vy == y_hi)
+            return false;
+        if (m_below) {
+            // Under-approximation: tangents at (x_lo, y_lo) and (x_hi, y_hi)
+            // bound xy from below across the box.
+            m_a = point(x_lo, y_lo);
+            m_b = point(x_hi, y_hi);
+        } else {
+            // Over-approximation: anti-diagonal corners.
+            m_a = point(x_lo, y_hi);
+            m_b = point(x_hi, y_lo);
+        }
+        m_pl_strict_interior = false;
+        return true;
+    }
+
     void get_points() {
+        if (c().params().arith_nl_tangents_box_corners() && set_box_corners()) {
+            // Box corners are extremes; pushing further moves out of the box
+            // and would invalidate the McCormick property.
+            TRACE(nla_solver, tout << "xy = " << m_xy << ", box-corner points: ";
+                  print_tangent_domain(tout) << std::endl;);
+            return;
+        }
         get_initial_points();
         TRACE(nla_solver, tout << "xy = " << m_xy << ", correct val = " << m_correct_v;
               print_tangent_domain(tout << "\ntang points:") << std::endl;);
-        push_point(m_a);        
+        push_point(m_a);
         push_point(m_b);
         TRACE(nla_solver,
-              tout << "pushed a = " << m_a << std::endl 
+              tout << "pushed a = " << m_a << std::endl
               << "pushed b = " << m_b << std::endl
               << "tang_plane(a) = " << tang_plane(m_a) << " , val = " << m_a << ", "
               << "tang_plane(b) = " << tang_plane(m_b) << " , val = " << m_b << std::endl;);

src/math/lp/nla_throttle.h

@@ -18,9 +18,10 @@ class nla_throttle {
 public:
     enum throttle_kind {
         ORDER_LEMMA,            // order lemma (9 params)
-        BINOMIAL_SIGN_LEMMA,    // binomial sign (6 params) 
+        BINOMIAL_SIGN_LEMMA,    // binomial sign (6 params)
         MONOTONE_LEMMA,         // monotonicity (2 params)
-        TANGENT_LEMMA           // tangent lemma (5 params: monic_var, x_var, y_var, below, plane_type)
+        TANGENT_LEMMA,          // tangent lemma (5 params: monic_var, x_var, y_var, below, plane_type)
+        MONOMIAL_BINOMIAL_SIGN  // monomial binomial sign anchor (4 params: monic_var, u, v, below)
     };
 
 private:

src/params/smt_params_helper.pyg

@@ -67,8 +67,10 @@ def_module_params(module_name='smt',
                           ('arith.nl.expensive_patching', BOOL, False, 'use the expensive of monomials'),
                           ('arith.nl.rounds', UINT, 1024, 'threshold for number of (nested) final checks for non linear arithmetic, relevant only if smt.arith.solver=2'),
                           ('arith.nl.order', BOOL, True, 'run order lemmas'),
+                          ('arith.nl.order.binomial_sign', BOOL, True, 'run order_lemma_on_binomial_sign; disabling it keeps the structural order-lemma splitting'),
                           ('arith.nl.expp', BOOL, False, 'expensive patching'),
                           ('arith.nl.tangents', BOOL, True, 'run tangent lemmas'),
+                          ('arith.nl.tangents.box_corners', BOOL, False, 'choose tangent-plane points at the bound-box corners instead of the model-centered val(x) +/- delta; produces the McCormick under/over envelope and is deterministic and snapshot-independent'),
                           ('arith.nl.horner', BOOL, True, 'run horner\'s heuristic'),
                           ('arith.nl.horner_subs_fixed', UINT, 2, '0 - no subs, 1 - substitute, 2 - substitute fixed zeros only'),
                           ('arith.nl.horner_frequency', UINT, 4, 'horner\'s call frequency'),
@@ -87,6 +89,9 @@ def_module_params(module_name='smt',
                           ('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_expand_terms', BOOL, True, 'expand terms before computing grobner basis'),
+                          ('arith.nl.monomial_sandwich', BOOL, False, 'derive bound on a monomial factor by pairing two LP rows that share the other factor'),
+                          ('arith.nl.monomial_sandwich.max_fanout', UINT, 0, 'skip monomial sandwich when the conclusion factor appears in more than this many monomials (0 = no limit)'),
+                          ('arith.nl.monomial_binomial_sign', BOOL, False, 'derive bound on a binomial-monomial factor anchored on the current LP value of the monomial; replaces order_lemma_on_binomial_sign with a deterministic factor bound conditioned on a one-sided snapshot of the monomial value'),
                           ('arith.nl.reduce_pseudo_linear', BOOL, True, 'create incremental linearization axioms for pseudo-linear monomials'),
                           ('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'),