Nl2lin - integrate a linear under approximation of a CAD cell by Valentin Promies. (#8982)

* outline of signature for assignment based conflict generation

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* outline of interface contract

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* remove confusing construction

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* add material in nra-solver to interface

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* add marshaling from nlsat lemmas into core solver

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* tidy

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* add call to check-assignment

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* Nl2lin (#7795)

* add linearized projection in nlsat

* implement nlsat check for given assignment

* add some comments

* fixup loop

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* updates

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* fixes

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* debug nl2lin

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

* Nl2lin (#7827)

* fix linear projection

* fix linear projection

* use an explicit cell description in check_assignment

* clean up (#7844)

* Simplify no effect checks in nla_core.cpp

Move up linear nlsat call to replace bounded nlsat.

* t

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

* t

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

* detangle mess

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* remove the too early return

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

* do not set use_nra_model to true

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

* remove a comment

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

* add a hook to add new multiplication definitions in nla_core

* add internalization routine that uses macro-expanded polynomial representation

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* add internalization routine that uses macro-expanded polynomial representation

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* fixup backtranslation to not use roots

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* call setup_assignment_solver instead of setup_solver

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* debug the setup, still not working

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

* updated clang format

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* simplify

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* create polynomials with integer coefficients, use the hook to create new monomials

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

* integrating changes from master related to work with polynomials

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

* add forgotten files

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

* Update nlsat_explain.cpp

Remove a duplicate call

* fix

* move linear cell construction to levelwise

* fix

* fix

* Port throttle and soundness fixes from master

- Fix soundness: pop incomplete lemma from m_lemmas on add_lemma failure
- Gracefully handle root atoms in add_lemma
- Throttle check_assignment with failure counter (decrement on success)
- Add arith.nl.nra_check_assignment parameter

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>

* Add arith.nl.nra_check_assignment_max_fail parameter

Replace hardcoded failure threshold with configurable parameter (default 10).

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>

* Add cha_abort_on_fail parameter to control failure counter decrement

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>

* abort nla check_assignment after a set number of allowed failures

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

* Add missing AST query methods to Java API (#8977)

* add Expr.isGround() to Java API

Expose Z3_is_ground as a public method on Expr. Returns true when the
expression contains no free variables.

* add Expr.isLambda() to Java API

Expose Z3_is_lambda as a public method on Expr. Returns true when the
expression is a lambda quantifier.

* add AST.getDepth() to Java API

Expose Z3_get_depth as a public method on AST. Returns the maximum
number of nodes on any path from root to leaf.

* add ArraySort.getArity() to Java API

Expose Z3_get_array_arity as a public method on ArraySort. Returns
the number of dimensions of a multi-dimensional array sort.

* add DatatypeSort.isRecursive() to Java API

Expose Z3_is_recursive_datatype_sort as a public method on
DatatypeSort. Returns true when the datatype refers to itself.

* add FPExpr.isNumeral() to Java API

Expose Z3_fpa_is_numeral as a public method on FPExpr. Returns true
when the expression is a concrete floating-point value.

* add isGroundExample test to JavaExample

Test Expr.isGround() on constants, variables, and compound
expressions.

* add astDepthExample test to JavaExample

Test AST.getDepth() on leaf nodes and nested expressions to verify
the depth computation.

* add arrayArityExample test to JavaExample

Test ArraySort.getArity() on single-domain and multi-domain array
sorts.

* add recursiveDatatypeExample test to JavaExample

Test DatatypeSort.isRecursive() on a recursive list datatype and a
non-recursive pair datatype.

* add fpNumeralExample test to JavaExample

Test FPExpr.isNumeral() on a floating point constant and a symbolic
variable.

* add isLambdaExample test to JavaExample

Test Expr.isLambda() on a lambda expression and a plain variable.

* change the default number of failures in check_assignment to 7

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

* Fix high and medium priority API coherence issues (Go, Java, C++, TypeScript) (#8983)

* Initial plan

* Add missing API functions to Go, Java, C++, and TypeScript bindings

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

* qf-s-benchmark: debug build + seq tracing + seq-fast/nseq-slow trace analysis (#8988)

* Initial plan

* Update qf-s-benchmark: debug build, seq tracing, trace analysis

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

* disable linear approximation by default to check the merge

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

* set check_assignment to true

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

* fix restore_x by recalulating new column values

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

* fix restore_x by recalulating new column values

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

* fix a memory leak

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

---------

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
Co-authored-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Co-authored-by: ValentinPromies <44966217+ValentinPromies@users.noreply.github.com>
Co-authored-by: Valentin Promies <valentin.promies@rwth-aachen.de>
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Co-authored-by: Angelica Moreira <48168649+angelica-moreira@users.noreply.github.com>
Co-authored-by: Copilot <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

src/math/lp/lar_solver.h

@@ -446,8 +446,11 @@ public:
         cs.restore_x();
         if (backup_sz < current_sz) {
             // New columns were added after backup.
-            // move_non_basic_columns_to_bounds snaps non-basic
+            // Recalculate basic variable values from non-basic ones
-            // columns to their bounds and finds a feasible solution.
+            // to restore the Ax=0 tableau invariant, then snap
+            // non-basic columns to their bounds and find a feasible solution.
+            for (unsigned i = 0; i < A_r().row_count(); i++)
+                set_column_value(r_basis()[i], get_basic_var_value_from_row(i));
             move_non_basic_columns_to_bounds();
         }
         else {

src/math/lp/nla_coi.cpp

@@ -1,4 +1,3 @@
-
 /*++
   Copyright (c) 2025 Microsoft Corporation
 

src/math/lp/nla_coi.h

@@ -1,4 +1,3 @@
-
 /*++
   Copyright (c) 2025 Microsoft Corporation
 
@@ -14,6 +13,9 @@
 
 #pragma once
 
+#include "util/uint_set.h"
+#include "util/vector.h"
+
 namespace nla {
 
     class core;

src/math/lp/nla_core.cpp

@@ -1331,6 +1331,13 @@ lbool core::check(unsigned level) {
             return l_false;
     }
 
+    if (no_effect() && params().arith_nl_nra_check_assignment() && m_check_assignment_fail_cnt < params().arith_nl_nra_check_assignment_max_fail()) {
+        scoped_limits sl(m_reslim);
+        sl.push_child(&m_nra_lim);
+        ret = m_nra.check_assignment();
+        if (ret != l_true)
+            ++m_check_assignment_fail_cnt;
+    }
 
     if (no_effect() && should_run_bounded_nlsat()) 
         ret = bounded_nlsat();

src/math/lp/nla_core.h

@@ -63,6 +63,7 @@ class core {
 
     unsigned m_nlsat_delay = 0;
     unsigned m_nlsat_delay_bound = 0;
+    unsigned m_check_assignment_fail_cnt = 0;
 
     bool should_run_bounded_nlsat();
     lbool bounded_nlsat();
@@ -94,6 +95,8 @@ class core {
     emonics                  m_emons;
     svector<lpvar>           m_add_buffer;
     mutable indexed_uint_set m_active_var_set;
+    // hook installed by theory_lra for creating a multiplication definition
+    std::function<lpvar(unsigned, lpvar const*)> m_add_mul_def_hook;
 
     reslimit                 m_nra_lim;
 
@@ -215,6 +218,8 @@ public:
     void add_idivision(lpvar q, lpvar x, lpvar y) { m_divisions.add_idivision(q, x, y); }
     void add_rdivision(lpvar q, lpvar x, lpvar y) { m_divisions.add_rdivision(q, x, y); }
     void add_bounded_division(lpvar q, lpvar x, lpvar y) { m_divisions.add_bounded_division(q, x, y); }
+    void set_add_mul_def_hook(std::function<lpvar(unsigned, lpvar const*)> const& f) { m_add_mul_def_hook = f; }
+    lpvar add_mul_def(unsigned sz, lpvar const* vs) { SASSERT(m_add_mul_def_hook); lpvar v = m_add_mul_def_hook(sz, vs); add_monic(v, sz, vs); return v; }
 
     void set_relevant(std::function<bool(lpvar)>& is_relevant) { m_relevant = is_relevant; }
     bool is_relevant(lpvar v) const { return !m_relevant || m_relevant(v); }
@@ -478,4 +483,3 @@ inline std::ostream& operator<<(std::ostream& out, pp_factorization const& f) {
 inline std::ostream& operator<<(std::ostream& out, pp_var const& v) { return v.c.print_var(v.v, out); }
 
 } // end of namespace nla
-

src/math/lp/nla_grobner.h

@@ -12,6 +12,7 @@
 #include "math/lp/nla_intervals.h"
 #include "math/lp/nex.h"
 #include "math/lp/cross_nested.h"
+#include "util/params.h"
 #include "util/uint_set.h"
 #include "math/grobner/pdd_solver.h"
 

src/math/lp/nra_solver.cpp

@@ -11,6 +11,7 @@
 #include "math/lp/nra_solver.h"
 #include "math/lp/nla_coi.h"
 #include "nlsat/nlsat_solver.h"
+#include "nlsat/nlsat_assignment.h"
 #include "math/polynomial/polynomial.h"
 #include "math/polynomial/algebraic_numbers.h"
 #include "util/map.h"
@@ -35,6 +36,13 @@ struct solver::imp {
     scoped_ptr<scoped_anum_vector>   m_values; // values provided by LRA solver
     scoped_ptr<scoped_anum> m_tmp1, m_tmp2;
     nla::coi                  m_coi;
+    svector<lp::constraint_index> m_literal2constraint;
+    struct eq {
+        bool operator()(unsigned_vector const &a, unsigned_vector const &b) const {
+            return a == b;
+        }
+    };
+    map<unsigned_vector, unsigned, svector_hash<unsigned_hash>, eq> m_vars2mon;
     nla::core&                m_nla_core;
     
     imp(lp::lar_solver& s, reslimit& lim, params_ref const& p, nla::core& nla_core): 
@@ -92,6 +100,44 @@ struct solver::imp {
         denominators.push_back(den);
     }
 
+    // Create polynomial definition for variable v used in setup_assignment_solver.
+    // Side-effects: updates m_vars2mon when v is a monic variable.
+    void mk_definition_assignment(unsigned v, polynomial_ref_vector &definitions) {
+        auto &pm = m_nlsat->pm();
+        polynomial::polynomial_ref p(pm);
+        if (m_nla_core.emons().is_monic_var(v)) {
+            auto const &m = m_nla_core.emons()[v];
+            auto vars = m.vars();
+            std::sort(vars.begin(), vars.end());
+            m_vars2mon.insert(vars, v);
+            for (auto v2 : vars) {
+                auto pv = definitions.get(v2);
+                if (!p)
+                    p = pv;
+                else
+                    p = pm.mul(p, pv);
+            }
+        }
+        else if (lra.column_has_term(v)) {
+            rational den(1);
+            for (auto const& [w, coeff] : lra.get_term(v))
+                den = lcm(den, denominator(coeff));
+            for (auto const& [w, coeff] : lra.get_term(v)) {
+                auto pw = definitions.get(w);
+                polynomial::polynomial_ref term(pm);
+                term = pm.mul(den * coeff, pw);
+                if (!p)
+                    p = term;
+                else
+                    p = pm.add(p, term);
+            }
+        }
+        else {
+            p = pm.mk_polynomial(lp2nl(v));
+        }
+        definitions.push_back(p);
+    }
+
     void setup_solver_poly() {
         m_coi.init();
         auto &pm = m_nlsat->pm();
@@ -275,6 +321,194 @@ struct solver::imp {
         return r;
     }
 
+    void setup_assignment_solver() {
+        SASSERT(need_check());
+        reset();
+        m_literal2constraint.reset();
+        m_vars2mon.reset();
+        m_coi.init();
+        auto &pm = m_nlsat->pm();
+        polynomial_ref_vector definitions(pm);
+        for (unsigned v = 0; v < lra.number_of_vars(); ++v) {
+            auto j = m_nlsat->mk_var(lra.var_is_int(v));
+            VERIFY(j == v);
+            m_lp2nl.insert(v, j);
+            scoped_anum a(am());
+            am().set(a, m_nla_core.val(v).to_mpq());
+            m_values->push_back(a);
+            mk_definition_assignment(v, definitions);
+        }
+
+        for (auto ci : m_coi.constraints()) {
+            auto &c = lra.constraints()[ci];
+            auto &pm = m_nlsat->pm();
+            auto k = c.kind();
+            auto rhs = c.rhs();
+            auto lhs = c.coeffs();
+            rational den = denominator(rhs);
+            for (auto [coeff, v] : lhs)
+                den = lcm(den, denominator(coeff));
+            polynomial::polynomial_ref p(pm);
+            p = pm.mk_const(-den * rhs);
+
+            for (auto [coeff, v] : lhs) {
+                polynomial_ref poly(pm);
+                poly = pm.mul(den * coeff, definitions.get(v));
+                p = p + poly;
+            }
+            auto lit = add_constraint(p, ci, k);
+            m_literal2constraint.setx(lit.index(), ci, lp::null_ci);
+        }
+    }
+
+    void process_polynomial_check_assignment(polynomial::polynomial const* p, rational& bound, const u_map<lp::lpvar>& nl2lp, lp::lar_term& t) {
+        polynomial::manager& pm = m_nlsat->pm();       
+        for (unsigned i = 0; i < pm.size(p); ++i) {
+            polynomial::monomial* m = pm.get_monomial(p, i);
+            auto& coeff = pm.coeff(p, i);
+                 
+            unsigned num_vars = pm.size(m);
+            // add mon * coeff to t;
+            switch (num_vars) {                            
+            case 0:
+                bound -= coeff;
+                break;
+            case 1: {
+                auto v = nl2lp[pm.get_var(m, 0)];
+                t.add_monomial(coeff, v);
+                break;
+            }
+            default: {
+                svector<lp::lpvar> vars;
+                for (unsigned j = 0; j < num_vars; ++j)
+                    vars.push_back(nl2lp[pm.get_var(m, j)]);
+                std::sort(vars.begin(), vars.end());
+                lp::lpvar v;
+                if (m_vars2mon.contains(vars)) 
+                   v = m_vars2mon[vars];
+                else 
+                   v = m_nla_core.add_mul_def(vars.size(), vars.data());  
+                t.add_monomial(coeff, v);
+                break;
+            }
+            }                      
+        }
+    }
+
+    u_map<lp::lpvar> reverse_lp2nl() {
+        u_map<lp::lpvar> nl2lp;
+        for (auto [j, x] : m_lp2nl)
+            nl2lp.insert(x, j);
+        return nl2lp;
+    }
+    
+    lbool check_assignment() {
+        setup_assignment_solver();
+        lbool r = l_undef;
+        statistics &st = m_nla_core.lp_settings().stats().m_st;
+        nlsat::literal_vector clause;
+        try {
+            nlsat::assignment rvalues(m_nlsat->am());
+            for (auto [j, x] : m_lp2nl) {
+                scoped_anum a(am());
+                am().set(a, m_nla_core.val(j).to_mpq());
+                rvalues.set(x, a);
+            }
+            r = m_nlsat->check(rvalues, clause);
+        } 
+        catch (z3_exception &) {
+            if (m_limit.is_canceled()) {
+                r = l_undef;
+            } 
+            else {
+                m_nlsat->collect_statistics(st);
+                throw;
+            }
+        }
+        m_nlsat->collect_statistics(st);
+        switch (r) {
+        case l_true:
+            m_nla_core.set_use_nra_model(true);
+            lra.init_model();
+            for (lp::constraint_index ci : lra.constraints().indices())
+                if (!check_constraint(ci))
+                    return l_undef;
+            for (auto const& m : m_nla_core.emons())
+                if (!check_monic(m))
+                    return l_undef;
+            m_nla_core.set_use_nra_model(true);
+            break;
+        case l_false:
+            r = add_lemma(clause);
+            break;
+        default:
+            break;
+        }
+        return r;        
+    }
+
+    lbool add_lemma(nlsat::literal_vector const &clause) {
+        u_map<lp::lpvar> nl2lp = reverse_lp2nl();
+        polynomial::manager &pm = m_nlsat->pm();
+        lbool result = l_false;
+        {
+            nla::lemma_builder lemma(m_nla_core, __FUNCTION__);
+            for (nlsat::literal l : clause) {
+                if (m_literal2constraint.get((~l).index(), lp::null_ci) != lp::null_ci) {
+                    auto ci = m_literal2constraint[(~l).index()];
+                    lp::explanation ex;
+                    ex.push_back(ci);
+                    lemma &= ex;
+                    continue;
+                }
+                nlsat::atom *a = m_nlsat->bool_var2atom(l.var());
+                if (a->is_root_atom()) {
+                    result = l_undef;
+                    break;
+                }
+                SASSERT(a->is_ineq_atom());
+                auto &ia = *to_ineq_atom(a);
+                if (ia.size() != 1) {
+                    result = l_undef; // factored polynomials not handled here
+                    break;
+                }
+                polynomial::polynomial const *p = ia.p(0);
+                rational bound(0);
+                lp::lar_term t;
+                process_polynomial_check_assignment(p, bound, nl2lp, t);
+
+                nla::ineq inq(lp::lconstraint_kind::EQ, t, bound);  // initial value overwritten in cases below
+                switch (a->get_kind()) {
+                case nlsat::atom::EQ:
+                    inq = nla::ineq(l.sign() ? lp::lconstraint_kind::NE : lp::lconstraint_kind::EQ, t, bound);
+                    break;
+                case nlsat::atom::LT:
+                    inq = nla::ineq(l.sign() ? lp::lconstraint_kind::GE : lp::lconstraint_kind::LT, t, bound);
+                    break;
+                case nlsat::atom::GT:
+                    inq = nla::ineq(l.sign() ? lp::lconstraint_kind::LE : lp::lconstraint_kind::GT, t, bound);
+                    break;
+                default:
+                    UNREACHABLE();
+                    result = l_undef;
+                    break;
+                }
+                if (result == l_undef)
+                    break;
+                if (m_nla_core.ineq_holds(inq)) {
+                    result = l_undef;
+                    break;
+                }
+                lemma |= inq;
+            }
+            if (result == l_false)
+                this->m_nla_core.m_check_feasible = true;
+        } // lemma_builder destructor runs here
+        if (result == l_undef)
+            m_nla_core.m_lemmas.pop_back(); // discard incomplete lemma
+        return result;
+    }
+
 
     void add_monic_eq_bound(mon_eq const& m) {
         if (!lra.column_has_lower_bound(m.var()) && 
@@ -646,7 +880,6 @@ struct solver::imp {
             if (m_nla_core.emons().is_monic_var(v)) {
                 am().set(a, 1);
                 auto &m = m_nla_core.emon(v);
-
                 for (auto x : m.vars()) 
                     am().mul(a, (*m_values)[x], a);
                 m_values->push_back(a);
@@ -737,6 +970,10 @@ lbool solver::check(dd::solver::equation_vector const& eqs) {
     return m_imp->check(eqs);
 }
 
+lbool solver::check_assignment() {
+    return m_imp->check_assignment();
+}
+
 bool solver::need_check() {
     return m_imp->need_check();
 }

src/math/lp/nra_solver.h

@@ -47,6 +47,11 @@ namespace nra {
         */
         lbool check(dd::solver::equation_vector const& eqs);
 
+        /**
+          \brief Check feasibility modulo current value assignment.
+        */
+        lbool check_assignment();
+
         /*
           \brief determine whether nra check is needed.
         */

src/nlsat/levelwise.cpp

@@ -75,6 +75,8 @@ namespace nlsat {
         mutable std_vector<unsigned> m_deg_in_order_graph; // degree of polynomial in resultant graph
         mutable std_vector<unsigned> m_unique_neighbor;    // UINT_MAX = not set, UINT_MAX-1 = multiple
 
+        bool m_linear_cell = false; // indicates whether cell bounds are forced to be linear
+
         assignment const& sample() const { return m_solver.sample(); }
 
         struct root_function {
@@ -231,7 +233,8 @@ namespace nlsat {
             assignment const&,
             pmanager& pm,
             anum_manager& am,
-            polynomial::cache& cache)
+            polynomial::cache& cache,
+            bool linear)
             : m_solver(solver),
               m_P(ps),
               m_n(max_x),
@@ -240,7 +243,8 @@ namespace nlsat {
               m_cache(cache),
               m_todo(m_cache, true),
               m_level_ps(m_pm),
-              m_psc_tmp(m_pm) {
+              m_psc_tmp(m_pm),
+              m_linear_cell(linear) {
             m_I.reserve(m_n);
             for (unsigned i = 0; i < m_n; ++i)
                 m_I.emplace_back(m_pm);
@@ -1007,6 +1011,66 @@ namespace nlsat {
             }
         }
 
+
+        void add_linear_poly_from_root(anum const& a, bool lower, polynomial_ref& p) {
+            rational r;
+            m_am.to_rational(a, r);
+            p = m_pm.mk_polynomial(m_level);
+            p = denominator(r)*p - numerator(r);
+
+            if (lower) {
+                m_I[m_level].l = p;
+                m_I[m_level].l_index = 1;
+            } else {
+                m_I[m_level].u = p;
+                m_I[m_level].u_index = 1;
+            }
+            m_level_ps.push_back(p);
+            m_poly_has_roots.push_back(true);
+            polynomial_ref w = choose_nonzero_coeff(p, m_level);
+            m_witnesses.push_back(w);
+        }
+
+        // Ensure that the interval bounds will be described by linear polynomials.
+        // If this is not already the case, the working set of polynomials is extended by
+        // new linear polynomials whose roots under-approximate the cell boundary.
+        // Based on: Valentin Promies, Jasper Nalbach, Erika Abraham and Paul Wagner
+        // "More is Less: Adding Polynomials for Faster Explanations in NLSAT" (CADE30, 2025)
+        void add_linear_approximations(anum const& v) {
+            polynomial_ref p_lower(m_pm), p_upper(m_pm);
+            auto& r = m_rel.m_rfunc;
+            if (m_I[m_level].is_section()) {
+                if (!m_am.is_rational(v)) {
+                    NOT_IMPLEMENTED_YET();
+                } 
+                else if (m_pm.total_degree(m_I[m_level].l) > 1) {
+                    add_linear_poly_from_root(v, true, p_lower);
+                    // update root function ordering
+                    r.emplace((r.begin() + m_l_rf), m_am, p_lower, 1, v, m_level_ps.size()-1);
+                }
+                return;
+            }
+
+            // sector: have to consider lower and upper bound
+            if (!m_I[m_level].l_inf() && m_pm.total_degree(m_I[m_level].l) > 1) {
+                scoped_anum between(m_am);
+                m_am.select(r[m_l_rf].val, v, between);
+                add_linear_poly_from_root(between, true, p_lower);
+                // update root function ordering
+                r.emplace((r.begin() + m_l_rf + 1), m_am, p_lower, 1, between, m_level_ps.size()-1);
+                ++m_l_rf;
+                if (is_set(m_u_rf))
+                    ++m_u_rf;
+            }
+            if (!m_I[m_level].u_inf() && m_pm.total_degree(m_I[m_level].u) > 1) {
+                scoped_anum between(m_am);
+                m_am.select(v, r[m_u_rf].val, between);
+                // update root function ordering
+                add_linear_poly_from_root(between, false, p_upper);
+                r.emplace((r.begin() + m_u_rf), m_am, p_upper, 1, between, m_level_ps.size()-1);
+            }
+        }
+
         // Build Θ (root functions) and pick I_level around sample(level).
         // Sets m_l_rf/m_u_rf and m_I[level].
         // Returns whether any roots were found (i.e., whether a relation can be built).
@@ -1022,6 +1086,10 @@ namespace nlsat {
                 return false;
 
             set_interval_from_root_partition(v, mid);
+
+            if (m_linear_cell)
+                add_linear_approximations(v);
+
             compute_side_mask();
             return true;
         }
@@ -1376,8 +1444,9 @@ namespace nlsat {
         assignment const& s,
         pmanager& pm,
         anum_manager& am,
-        polynomial::cache& cache)
+        polynomial::cache& cache,
-        : m_impl(new impl(solver, ps, n, s, pm, am, cache)) {}
+        bool linear)
+        : m_impl(new impl(solver, ps, n, s, pm, am, cache, linear)) {}
 
     levelwise::~levelwise() { delete m_impl; }
 

src/nlsat/levelwise.h

@@ -40,7 +40,7 @@ namespace nlsat {
         impl* m_impl;
     public:
         // Construct with polynomials ps, maximal variable max_x, current sample s, polynomial manager pm, and algebraic-number manager am
-        levelwise(nlsat::solver& solver, polynomial_ref_vector const& ps, var max_x, assignment const& s, pmanager& pm, anum_manager& am, polynomial::cache & cache);
+        levelwise(nlsat::solver& solver, polynomial_ref_vector const& ps, var max_x, assignment const& s, pmanager& pm, anum_manager& am, polynomial::cache & cache, bool linear=false);
         ~levelwise();
 
         levelwise(levelwise const&) = delete;

src/nlsat/nlsat_explain.cpp

@@ -1040,13 +1040,13 @@ namespace nlsat {
            \brief Apply model-based projection operation defined in our paper.
         */
 
-        bool levelwise_single_cell(polynomial_ref_vector & ps, var max_x, polynomial::cache & cache) {
+        bool levelwise_single_cell(polynomial_ref_vector & ps, var max_x, polynomial::cache & cache, bool linear=false) {
             // Store polynomials for debugging unsound lemmas
             m_last_lws_input_polys.reset();
             for (unsigned i = 0; i < ps.size(); i++)
                 m_last_lws_input_polys.push_back(ps.get(i));
             
-            levelwise lws(m_solver, ps, max_x, sample(), m_pm, m_am, cache);
+            levelwise lws(m_solver, ps, max_x, sample(), m_pm, m_am, cache, linear);
             auto cell = lws.single_cell();
             TRACE(lws, for (unsigned i = 0; i < cell.size(); i++)
                                  display(tout << "I[" << i << "]:", m_solver, cell[i]) << "\n";);
@@ -1139,9 +1139,23 @@ namespace nlsat {
                 x = extract_max_polys(ps);
                 cac_add_cell_lits(ps, x, samples);
             }
-            
         }
 
+
+        /**
+         * \brief compute the resultants of p with each polynomial in ps w.r.t. x
+         */
+        void psc_resultants_with(polynomial_ref_vector const& ps, polynomial_ref p, var const x) {
+            polynomial_ref q(m_pm);
+            unsigned sz = ps.size();
+            for (unsigned i = 0; i < sz; i++) {
+                q = ps.get(i);
+                if (q == p) continue;
+                psc(p, q, x);
+            }
+        }
+
+
         bool check_already_added() const {
             for (bool b : m_already_added_literal) {
                 (void)b;
@@ -1698,6 +1712,38 @@ namespace nlsat {
         }
 
 
+        void compute_linear_explanation(unsigned num, literal const * ls, scoped_literal_vector & result) {
+            SASSERT(check_already_added());
+            SASSERT(num > 0);
+            SASSERT(max_var(num, ls) != 0 || m_solver.sample().is_assigned(0));
+            TRACE(nlsat_explain, 
+                  tout << "the infeasible clause:\n"; 
+                  display(tout, m_solver, num, ls) << "\n";
+                  m_solver.display_assignment(tout << "assignment:\n");
+                  );
+
+            m_result = &result;
+            m_lower_stage_polys.reset();
+            collect_polys(num, ls, m_ps);
+            for (unsigned i = 0; i < m_lower_stage_polys.size(); i++) {
+                m_ps.push_back(m_lower_stage_polys.get(i));
+            }
+            if (m_ps.empty())
+                return;
+            
+            // We call levelwise directly without normalize, simplify, elim_vanishing to preserve the original polynomials
+            var max_x = max_var(m_ps);
+            bool levelwise_ok = levelwise_single_cell(m_ps, max_x+1, m_cache, true); // max_x+1 because we have a full sample
+            SASSERT(levelwise_ok);
+            m_solver.record_levelwise_result(levelwise_ok);
+
+            reset_already_added();
+            m_result = nullptr;
+            TRACE(nlsat_explain, display(tout << "[explain] result\n", m_solver, result) << "\n";);
+            CASSERT("nlsat", check_already_added());
+        }
+
+
         void project(var x, unsigned num, literal const * ls, scoped_literal_vector & result) {
             unsigned base = result.size();
             while (true) {
@@ -1876,6 +1922,10 @@ namespace nlsat {
         m_imp->compute_conflict_explanation(n, ls, result);
     }
 
+    void explain::compute_linear_explanation(unsigned n, literal const * ls, scoped_literal_vector & result) {
+        m_imp->compute_linear_explanation(n, ls, result);
+    }
+
     void explain::project(var x, unsigned n, literal const * ls, scoped_literal_vector & result) {
         m_imp->project(x, n, ls, result);
     }

src/nlsat/nlsat_explain.h

@@ -66,6 +66,12 @@ namespace nlsat {
         */
         void compute_conflict_explanation(unsigned n, literal const * ls, scoped_literal_vector & result);
 
+        /**
+           \brief A variant of compute_conflict_explanation, but all resulting literals s_i are linear.
+           This is achieved by adding new polynomials during the projection, thereby under-approximating
+           the computed cell.
+        */
+        void compute_linear_explanation(unsigned n, literal const * ls, scoped_literal_vector & result);
         
         /**
            \brief projection for a given variable.

src/nlsat/nlsat_solver.cpp

@@ -2156,6 +2156,62 @@ namespace nlsat {
             m_assignment.reset();
         }
 
+        lbool check(assignment const& rvalues, literal_vector& clause) {
+            // temporarily set m_assignment to the given one
+            assignment tmp = m_assignment;
+            m_assignment.reset();
+            m_assignment.copy(rvalues);
+
+            // check whether the asserted atoms are satisfied by rvalues
+            literal best_literal = null_literal;
+            lbool satisfied = l_true;
+            for (auto cp : m_clauses) {
+                auto& c = *cp;
+                bool is_false = all_of(c, [&](literal l) { return const_cast<imp*>(this)->value(l) == l_false; });
+                bool is_true = any_of(c, [&](literal l) { return const_cast<imp*>(this)->value(l) == l_true; });
+                if (is_true)
+                    continue;                
+                
+                if (!is_false) {
+                    satisfied = l_undef;
+                    continue;
+                }
+
+                // take best literal from c
+                for (literal l : c) {
+                    if (best_literal == null_literal) {
+                        best_literal = l;
+                    } 
+                    else {
+                        bool_var b_best = best_literal.var();
+                        bool_var b_l = l.var();
+                        if (degree(m_atoms[b_l]) < degree(m_atoms[b_best])) {
+                            best_literal = l;
+                        }
+                        // TODO: there might be better criteria than just the degree in the main variable.
+                    }
+                }
+            }
+
+            if (best_literal == null_literal)
+                return satisfied;
+
+            // assignment does not satisfy the constraints -> create lemma
+            SASSERT(best_literal != null_literal);
+            clause.reset();
+            m_lazy_clause.reset();
+            m_explain.compute_linear_explanation(1, &best_literal, m_lazy_clause);
+
+            for (auto l : m_lazy_clause) {
+                clause.push_back(l);
+            }
+            clause.push_back(~best_literal);
+
+            m_assignment.reset();
+            m_assignment.copy(tmp);
+            return l_false;
+        }
+
         lbool check(literal_vector& assumptions) {
             literal_vector result;
             unsigned sz = assumptions.size();
@@ -4419,6 +4475,10 @@ namespace nlsat {
         return m_imp->check(assumptions);
     }
 
+    lbool solver::check(assignment const& rvalues, literal_vector& clause) {
+        return m_imp->check(rvalues, clause);
+    }
+
     void solver::get_core(vector<assumption, false>& assumptions) {
         return m_imp->get_core(assumptions);
     }

src/nlsat/nlsat_solver.h

@@ -219,6 +219,19 @@ namespace nlsat {
 
         lbool check(literal_vector& assumptions);
 
+        //
+        // check satisfiability of asserted formulas relative to state of the nlsat solver.
+        // produce either,
+        // l_true - a model is available (rvalues can be ignored) or,
+        // l_false - a clause (not core v not cell) excluding a cell around rvalues if core (consisting of atoms
+        // passed to nlsat) is asserted.
+        // l_undef - if the search was interrupted by a resource limit.
+        // clause is a list of literals. Their disjunction is valid.
+        // Different implementations of check are possible. One where cell comprises of linear polynomials could
+        // produce lemmas that are friendly to linear arithmetic solvers.
+        //
+        lbool check(assignment const& rvalues, literal_vector& clause);
+
         // -----------------------
         //
         // Model

src/params/smt_params_helper.pyg

@@ -60,6 +60,8 @@ def_module_params(module_name='smt',
                           ('arith.solver', UINT, 6, 'arithmetic solver: 0 - no solver, 1 - bellman-ford based solver (diff. logic only), 2 - simplex based solver, 3 - floyd-warshall based solver (diff. logic only) and no theory combination 4 - utvpi, 5 - infinitary lra, 6 - lra solver'),
                           ('arith.nl', BOOL, True, '(incomplete) nonlinear arithmetic support based on Groebner basis and interval propagation, relevant only if smt.arith.solver=2'),
                           ('arith.nl.nra', BOOL, True, 'call nra_solver when incremental linearization does not produce a lemma, this option is ignored when arith.nl=false, relevant only if smt.arith.solver=6'),
+                          ('arith.nl.nra_check_assignment', BOOL, True, 'call check_assignment in nra_solver to verify current assignment against nlsat constraints'),
+                          ('arith.nl.nra_check_assignment_max_fail', UINT, 7, 'maximum consecutive check_assignment failures before disabling it'),
                           ('arith.nl.branching', BOOL, True, 'branching on integer variables in non linear clusters'),
                           ('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'),

src/smt/theory_lra.cpp

@@ -155,6 +155,7 @@ class theory_lra::imp {
     ptr_vector<expr>       m_not_handled;
     ptr_vector<app>        m_underspecified;
     ptr_vector<app>        m_bv_terms;
+    ptr_vector<expr>       m_mul_defs; // fresh multiplication definition vars
     vector<ptr_vector<api_bound> > m_use_list;        // bounds where variables are used.
 
     // attributes for incremental version:
@@ -267,9 +268,25 @@ class theory_lra::imp {
             };
             m_nla->set_relevant(is_relevant);
             m_nla->updt_params(ctx().get_params());
+            m_nla->get_core().set_add_mul_def_hook([&](unsigned sz, lpvar const* vs) { return add_mul_def(sz, vs); });
         }
     }
 
+    lpvar add_mul_def(unsigned sz, lpvar const* vs) {
+        bool is_int = true;
+        for (unsigned i = 0; i < sz; ++i) {
+            theory_var tv = lp().local_to_external(vs[i]);
+            is_int &= this->is_int(tv);
+        }
+        sort* srt = is_int ? a.mk_int() : a.mk_real();
+        app_ref c(m.mk_fresh_const("mul!", srt), m);
+        mk_enode(c);
+        theory_var v = mk_var(c);
+        ctx().push_trail(push_back_vector<ptr_vector<expr>>(m_mul_defs));
+        m_mul_defs.push_back(c);
+        return register_theory_var_in_lar_solver(v);
+    }
+
     void found_unsupported(expr* n) {
         ctx().push_trail(push_back_vector<ptr_vector<expr>>(m_not_handled));
         TRACE(arith, tout << "unsupported " << mk_pp(n, m) << "\n");