From 6fb68ac010daef986734ac5a6662a22613d9863b Mon Sep 17 00:00:00 2001 From: Lev Nachmanson <5377127+levnach@users.noreply.github.com> Date: Sun, 15 Mar 2026 06:13:04 -1000 Subject: [PATCH] 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 * outline of interface contract Signed-off-by: Nikolaj Bjorner * remove confusing construction Signed-off-by: Nikolaj Bjorner * add material in nra-solver to interface Signed-off-by: Nikolaj Bjorner * add marshaling from nlsat lemmas into core solver Signed-off-by: Nikolaj Bjorner * tidy Signed-off-by: Nikolaj Bjorner * add call to check-assignment Signed-off-by: Nikolaj Bjorner * Nl2lin (#7795) * add linearized projection in nlsat * implement nlsat check for given assignment * add some comments * fixup loop Signed-off-by: Nikolaj Bjorner * updates Signed-off-by: Nikolaj Bjorner * fixes Signed-off-by: Nikolaj Bjorner * debug nl2lin Signed-off-by: Lev Nachmanson * 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 * t Signed-off-by: Lev Nachmanson * detangle mess Signed-off-by: Nikolaj Bjorner * remove the too early return Signed-off-by: Lev Nachmanson * do not set use_nra_model to true Signed-off-by: Lev Nachmanson * remove a comment Signed-off-by: Lev Nachmanson * 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 * add internalization routine that uses macro-expanded polynomial representation Signed-off-by: Nikolaj Bjorner * fixup backtranslation to not use roots Signed-off-by: Nikolaj Bjorner * call setup_assignment_solver instead of setup_solver Signed-off-by: Nikolaj Bjorner * debug the setup, still not working Signed-off-by: Lev Nachmanson * updated clang format Signed-off-by: Nikolaj Bjorner * simplify Signed-off-by: Nikolaj Bjorner * create polynomials with integer coefficients, use the hook to create new monomials Signed-off-by: Lev Nachmanson * integrating changes from master related to work with polynomials Signed-off-by: Lev Nachmanson * add forgotten files Signed-off-by: Lev Nachmanson * 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 * 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 * 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 * set check_assignment to true Signed-off-by: Lev Nachmanson * fix restore_x by recalulating new column values Signed-off-by: Lev Nachmanson * fix restore_x by recalulating new column values Signed-off-by: Lev Nachmanson * fix a memory leak Signed-off-by: Lev Nachmanson --------- Signed-off-by: Nikolaj Bjorner Signed-off-by: Lev Nachmanson Co-authored-by: Nikolaj Bjorner Co-authored-by: ValentinPromies <44966217+ValentinPromies@users.noreply.github.com> Co-authored-by: Valentin Promies 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 | 7 +- src/math/lp/nla_coi.cpp | 3 +- src/math/lp/nla_coi.h | 6 +- src/math/lp/nla_core.cpp | 11 +- src/math/lp/nla_core.h | 6 +- src/math/lp/nla_grobner.h | 1 + src/math/lp/nla_pp.cpp | 2 +- src/math/lp/nra_solver.cpp | 245 ++++++++++++++++++++++++++++++- src/math/lp/nra_solver.h | 5 + src/nlsat/levelwise.cpp | 77 +++++++++- src/nlsat/levelwise.h | 2 +- src/nlsat/nlsat_explain.cpp | 56 ++++++- src/nlsat/nlsat_explain.h | 6 + src/nlsat/nlsat_solver.cpp | 60 ++++++++ src/nlsat/nlsat_solver.h | 13 ++ src/params/smt_params_helper.pyg | 2 + src/smt/theory_lra.cpp | 17 +++ 17 files changed, 497 insertions(+), 22 deletions(-) diff --git a/src/math/lp/lar_solver.h b/src/math/lp/lar_solver.h index 5c7e7bbb0..a5d49dd33 100644 --- a/src/math/lp/lar_solver.h +++ b/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 - // columns to their bounds and finds a feasible solution. + // Recalculate basic variable values from non-basic ones + // 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 { diff --git a/src/math/lp/nla_coi.cpp b/src/math/lp/nla_coi.cpp index fcab22021..2632ab217 100644 --- a/src/math/lp/nla_coi.cpp +++ b/src/math/lp/nla_coi.cpp @@ -1,4 +1,3 @@ - /*++ Copyright (c) 2025 Microsoft Corporation @@ -85,4 +84,4 @@ namespace nla { } } } -} \ No newline at end of file +} diff --git a/src/math/lp/nla_coi.h b/src/math/lp/nla_coi.h index d05f08fbd..683b30e09 100644 --- a/src/math/lp/nla_coi.h +++ b/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; @@ -40,4 +42,4 @@ namespace nla { indexed_uint_set const &vars() { return m_var_set; } }; -} \ No newline at end of file +} diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp index c7a29e9a7..a78dfc451 100644 --- a/src/math/lp/nla_core.cpp +++ b/src/math/lp/nla_core.cpp @@ -1331,7 +1331,14 @@ 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(); @@ -1582,4 +1589,4 @@ void core::refine_pseudo_linear(monic const& m) { } SASSERT(nlvar != null_lpvar); lemma |= ineq(lp::lar_term(m.var(), rational(-prod), nlvar), llc::EQ, rational(0)); -} \ No newline at end of file +} diff --git a/src/math/lp/nla_core.h b/src/math/lp/nla_core.h index 5ccbc17e0..8055c5e93 100644 --- a/src/math/lp/nla_core.h +++ b/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 m_add_buffer; mutable indexed_uint_set m_active_var_set; + // hook installed by theory_lra for creating a multiplication definition + std::function 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 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& 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 - diff --git a/src/math/lp/nla_grobner.h b/src/math/lp/nla_grobner.h index 19f0e3687..b9ed043d5 100644 --- a/src/math/lp/nla_grobner.h +++ b/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" diff --git a/src/math/lp/nla_pp.cpp b/src/math/lp/nla_pp.cpp index 7d7e8ec7c..c925753c8 100644 --- a/src/math/lp/nla_pp.cpp +++ b/src/math/lp/nla_pp.cpp @@ -432,4 +432,4 @@ std::ostream& core::display_constraint_smt(std::ostream& out, unsigned id, lp::l out << (evaluation ? "true" : "false"); out << "\n"; return out; -} \ No newline at end of file +} diff --git a/src/math/lp/nra_solver.cpp b/src/math/lp/nra_solver.cpp index dae20dc69..96a1c97a3 100644 --- a/src/math/lp/nra_solver.cpp +++ b/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 m_values; // values provided by LRA solver scoped_ptr m_tmp1, m_tmp2; nla::coi m_coi; + svector m_literal2constraint; + struct eq { + bool operator()(unsigned_vector const &a, unsigned_vector const &b) const { + return a == b; + } + }; + map, 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(); @@ -273,7 +319,195 @@ struct solver::imp { break; } 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& 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 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 reverse_lp2nl() { + u_map 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 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) { @@ -643,10 +877,9 @@ struct solver::imp { unsigned w; scoped_anum a(am()); for (unsigned v = m_values->size(); v < sz; ++v) { - if (m_nla_core.emons().is_monic_var(v)) { + 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); @@ -654,7 +887,7 @@ struct solver::imp { else if (lra.column_has_term(v)) { scoped_anum b(am()); am().set(a, 0); - for (auto const &[w, coeff] : lra.get_term(v)) { + for (auto const &[w, coeff] : lra.get_term(v)) { am().set(b, coeff.to_mpq()); am().mul(b, (*m_values)[w], b); am().add(a, b, 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(); } diff --git a/src/math/lp/nra_solver.h b/src/math/lp/nra_solver.h index b009b3c12..1e4e2829f 100644 --- a/src/math/lp/nra_solver.h +++ b/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. */ diff --git a/src/nlsat/levelwise.cpp b/src/nlsat/levelwise.cpp index 7821c8a84..2ff363763 100644 --- a/src/nlsat/levelwise.cpp +++ b/src/nlsat/levelwise.cpp @@ -75,6 +75,8 @@ namespace nlsat { mutable std_vector m_deg_in_order_graph; // degree of polynomial in resultant graph mutable std_vector 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) - : m_impl(new impl(solver, ps, n, s, pm, am, cache)) {} + polynomial::cache& cache, + bool linear) + : m_impl(new impl(solver, ps, n, s, pm, am, cache, linear)) {} levelwise::~levelwise() { delete m_impl; } diff --git a/src/nlsat/levelwise.h b/src/nlsat/levelwise.h index 950bee641..3bb17e591 100644 --- a/src/nlsat/levelwise.h +++ b/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; diff --git a/src/nlsat/nlsat_explain.cpp b/src/nlsat/nlsat_explain.cpp index d5aadf683..1555e2989 100644 --- a/src/nlsat/nlsat_explain.cpp +++ b/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); } diff --git a/src/nlsat/nlsat_explain.h b/src/nlsat/nlsat_explain.h index 3ff4fb982..e33477a80 100644 --- a/src/nlsat/nlsat_explain.h +++ b/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. diff --git a/src/nlsat/nlsat_solver.cpp b/src/nlsat/nlsat_solver.cpp index e5e104a33..6a656b46d 100644 --- a/src/nlsat/nlsat_solver.cpp +++ b/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(this)->value(l) == l_false; }); + bool is_true = any_of(c, [&](literal l) { return const_cast(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& assumptions) { return m_imp->get_core(assumptions); } diff --git a/src/nlsat/nlsat_solver.h b/src/nlsat/nlsat_solver.h index ff970fefa..b6e003473 100644 --- a/src/nlsat/nlsat_solver.h +++ b/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 diff --git a/src/params/smt_params_helper.pyg b/src/params/smt_params_helper.pyg index 451a07964..708d88bb6 100644 --- a/src/params/smt_params_helper.pyg +++ b/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'), diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index 72bf7354a..901785378 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -155,6 +155,7 @@ class theory_lra::imp { ptr_vector m_not_handled; ptr_vector m_underspecified; ptr_vector m_bv_terms; + ptr_vector m_mul_defs; // fresh multiplication definition vars vector > 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>(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>(m_not_handled)); TRACE(arith, tout << "unsupported " << mk_pp(n, m) << "\n");