From 46284c434a83ad419e729a2d1dc9e745e39b618d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 11 Jul 2025 18:36:28 +0200 Subject: [PATCH 01/42] outline of signature for assignment based conflict generation Signed-off-by: Nikolaj Bjorner --- src/nlsat/nlsat_solver.cpp | 8 ++++++++ src/nlsat/nlsat_solver.h | 11 +++++++++++ 2 files changed, 19 insertions(+) diff --git a/src/nlsat/nlsat_solver.cpp b/src/nlsat/nlsat_solver.cpp index 97cac90fc..00fc58962 100644 --- a/src/nlsat/nlsat_solver.cpp +++ b/src/nlsat/nlsat_solver.cpp @@ -2034,6 +2034,10 @@ namespace nlsat { m_assignment.reset(); } + lbool check(literal_vector& assumptions, assignment const& rvalues, polynomial_ref_vector& core) { + return l_undef; + } + lbool check(literal_vector& assumptions) { literal_vector result; unsigned sz = assumptions.size(); @@ -4104,6 +4108,10 @@ namespace nlsat { return m_imp->check(assumptions); } + lbool solver::check(literal_vector& assumptions, assignment const& rvalues, polynomial_ref_vector& core) { + return m_imp->check(assumptions, rvalues, core); + } + 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 ae403fc83..0d0a0d3d4 100644 --- a/src/nlsat/nlsat_solver.h +++ b/src/nlsat/nlsat_solver.h @@ -218,6 +218,17 @@ namespace nlsat { lbool check(literal_vector& assumptions); + // check satisfiability of asserted formulas relative to assumptions. + // produce either, + // l_true - a model is availabe (rvalues can be ignored) or, + // l_false - update the list of assumptions (possibly reset it to empty), and a set of polynomials in core, + // such that the conjunction of the assumptions and the polynomials in core is unsatisfiable. + // l_undef - if the search was interrupted by a resource limit. + // We associate literals with the polynomials in the core based on their sign with respect to rvalues. + // If p(rvalues) > 0, then the literal is p <= 0, p(rvalues) < 0, then p(rvalues) >= 0, and p(rvalues) = 0, then p != 0. + // + lbool check(literal_vector& assumptions, assignment const& rvalues, polynomial_ref_vector& core); + // ----------------------- // // Model From 6bcee13158f9f14821c187c6c0c96cf62e51c4a5 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 11 Jul 2025 18:44:41 +0200 Subject: [PATCH 02/42] outline of interface contract Signed-off-by: Nikolaj Bjorner --- src/nlsat/nlsat_solver.h | 10 +++++++--- 1 file changed, 7 insertions(+), 3 deletions(-) diff --git a/src/nlsat/nlsat_solver.h b/src/nlsat/nlsat_solver.h index 0d0a0d3d4..b27691753 100644 --- a/src/nlsat/nlsat_solver.h +++ b/src/nlsat/nlsat_solver.h @@ -218,14 +218,18 @@ namespace nlsat { lbool check(literal_vector& assumptions); + // // check satisfiability of asserted formulas relative to assumptions. // produce either, - // l_true - a model is availabe (rvalues can be ignored) or, + // l_true - a model is available (rvalues can be ignored) or, // l_false - update the list of assumptions (possibly reset it to empty), and a set of polynomials in core, // such that the conjunction of the assumptions and the polynomials in core is unsatisfiable. // l_undef - if the search was interrupted by a resource limit. - // We associate literals with the polynomials in the core based on their sign with respect to rvalues. - // If p(rvalues) > 0, then the literal is p <= 0, p(rvalues) < 0, then p(rvalues) >= 0, and p(rvalues) = 0, then p != 0. + // Core is a list of polynomials. We associate literals as follows: + // For ~ in { >, <, = } If p(rvalues) ~ 0, then lit is p ~ 0. Their negations are used in the conflict clause. + // (this constrains the kind of literals for the conflict clause and may be revisited). + // Different implementations of check are possible. One where core comprises of linear polynomials could + // produce lemmas that are friendly to linear arithmetic solvers. // lbool check(literal_vector& assumptions, assignment const& rvalues, polynomial_ref_vector& core); From 5f25eb5aa2209ec7a7033dda1d33ea2ac321e428 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 11 Jul 2025 19:18:35 +0200 Subject: [PATCH 03/42] remove confusing construction Signed-off-by: Nikolaj Bjorner --- src/nlsat/nlsat_solver.h | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/src/nlsat/nlsat_solver.h b/src/nlsat/nlsat_solver.h index b27691753..ddff95255 100644 --- a/src/nlsat/nlsat_solver.h +++ b/src/nlsat/nlsat_solver.h @@ -225,9 +225,7 @@ namespace nlsat { // l_false - update the list of assumptions (possibly reset it to empty), and a set of polynomials in core, // such that the conjunction of the assumptions and the polynomials in core is unsatisfiable. // l_undef - if the search was interrupted by a resource limit. - // Core is a list of polynomials. We associate literals as follows: - // For ~ in { >, <, = } If p(rvalues) ~ 0, then lit is p ~ 0. Their negations are used in the conflict clause. - // (this constrains the kind of literals for the conflict clause and may be revisited). + // Core is a list of polynomials. We associate literals as follows: TBD // Different implementations of check are possible. One where core comprises of linear polynomials could // produce lemmas that are friendly to linear arithmetic solvers. // From c3488fcfa9b2c542300ece4d3030a3de023cc2a0 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 11 Jul 2025 20:02:28 +0200 Subject: [PATCH 04/42] add material in nra-solver to interface Signed-off-by: Nikolaj Bjorner --- src/math/lp/nra_solver.cpp | 158 +++++++++++++++++++++++++++++-------- src/math/lp/nra_solver.h | 5 ++ src/nlsat/nlsat_solver.cpp | 6 +- src/nlsat/nlsat_solver.h | 8 +- 4 files changed, 139 insertions(+), 38 deletions(-) diff --git a/src/math/lp/nra_solver.cpp b/src/math/lp/nra_solver.cpp index bc498f9e4..419504502 100644 --- a/src/math/lp/nra_solver.cpp +++ b/src/math/lp/nra_solver.cpp @@ -10,6 +10,7 @@ #include "math/lp/lar_solver.h" #include "math/lp/nra_solver.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" @@ -133,27 +134,15 @@ struct solver::imp { m_lp2nl.reset(); } - /** - \brief one-shot nlsat check. - A one shot checker is the least functionality that can - enable non-linear reasoning. - In addition to checking satisfiability we would also need - to identify equalities in the model that should be assumed - with the remaining solver. - - TBD: use partial model from lra_solver to prime the state of nlsat_solver. - TBD: explore more incremental ways of applying nlsat (using assumptions) - */ - lbool check() { + void setup_solver() { SASSERT(need_check()); reset(); - vector core; init_cone_of_influence(); // add linear inequalities from lra_solver for (auto ci : m_constraint_set) add_constraint(ci); - + // add polynomial definitions. for (auto const& m : m_mon_set) add_monic_eq(m_nla_core.emons()[m]); @@ -169,7 +158,7 @@ struct solver::imp { static unsigned id = 0; std::stringstream strm; -#ifndef SINGLE_THREAD +#ifndef SINGLE_THREAD std::thread::id this_id = std::this_thread::get_id(); strm << "nla_" << this_id << "." << (++id) << ".smt2"; #else @@ -180,7 +169,39 @@ struct solver::imp { out << "(check-sat)\n"; out.close(); } + } + void validate_constraints() { + for (lp::constraint_index ci : lra.constraints().indices()) + if (!check_constraint(ci)) { + IF_VERBOSE(0, verbose_stream() << "constraint " << ci << " violated\n"; + lra.constraints().display(verbose_stream())); + UNREACHABLE(); + return; + } + for (auto const& m : m_nla_core.emons()) { + if (!check_monic(m)) { + IF_VERBOSE(0, verbose_stream() << "monic " << m << " violated\n"; + lra.constraints().display(verbose_stream())); + UNREACHABLE(); + return; + } + } + } + + /** + \brief one-shot nlsat check. + A one shot checker is the least functionality that can + enable non-linear reasoning. + In addition to checking satisfiability we would also need + to identify equalities in the model that should be assumed + with the remaining solver. + + TBD: use partial model from lra_solver to prime the state of nlsat_solver. + TBD: explore more incremental ways of applying nlsat (using assumptions) + */ + lbool check() { + setup_solver(); lbool r = l_undef; statistics& st = m_nla_core.lp_settings().stats().m_st; try { @@ -204,23 +225,10 @@ struct solver::imp { 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)) { - IF_VERBOSE(0, verbose_stream() << "constraint " << ci << " violated\n"; - lra.constraints().display(verbose_stream())); - UNREACHABLE(); - return l_undef; - } - for (auto const& m : m_nla_core.emons()) { - if (!check_monic(m)) { - IF_VERBOSE(0, verbose_stream() << "monic " << m << " violated\n"; - lra.constraints().display(verbose_stream())); - UNREACHABLE(); - return l_undef; - } - } + validate_constraints(); break; case l_false: { + vector core; lp::explanation ex; m_nlsat->get_core(core); for (auto c : core) { @@ -237,7 +245,91 @@ struct solver::imp { break; } return r; - } + } + + lbool check_assignment() { + setup_solver(); + lbool r = l_undef; + statistics& st = m_nla_core.lp_settings().stats().m_st; + nlsat::atom_vector clause; + try { + polynomial::manager& pm = m_nlsat->pm(); + 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); + TRACE(nra, + m_nlsat->display(tout << r << "\n"); + display(tout); + for (auto [j, x] : m_lp2nl) tout << "j" << j << " := x" << x << "\n";); + switch (r) { + case l_true: + m_nla_core.set_use_nra_model(true); + lra.init_model(); + validate_constraints(); + break; + case l_false: { + vector core; + lp::explanation ex; + m_nlsat->get_core(core); + for (auto c : core) { + unsigned idx = static_cast(static_cast(c) - this); + ex.push_back(idx); + TRACE(nra, lra.display_constraint(tout << "ex: " << idx << ": ", idx) << "\n";); + } + for (auto a : clause) { + // a cannot be a root object. + SASSERT(!a->is_root_atom()); + SASSERT(a->is_ineq_atom()); + auto& ia = *to_ineq_atom(a); + VERIFY(ia.size() == 1); // deal with factored polynomials later + // a is an inequality atom, i.e., p > 0, p < 0, or p = 0. + polynomial::polynomial* p = ia.p(0); + + #if 0 + // convert poloynomial into monomials etc. + #endif + switch (a->get_kind()) { + case nlsat::atom::EQ: { + NOT_IMPLEMENTED_YET(); + break; + } + case nlsat::atom::LT: { + NOT_IMPLEMENTED_YET(); + break; + } + case nlsat::atom::GT: { + NOT_IMPLEMENTED_YET(); + break; + } + default: + UNREACHABLE(); + } + } + + nla::lemma_builder lemma(m_nla_core, __FUNCTION__); + lemma &= ex; + m_nla_core.set_use_nra_model(true); + break; + } + case l_undef: + break; + } + return r; + } void add_monic_eq_bound(mon_eq const& m) { @@ -655,6 +747,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 90f022ba6..f3b3bf69c 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 moduo current value assignment. + */ + lbool check_assignment(); + /* \brief determine whether nra check is needed. */ diff --git a/src/nlsat/nlsat_solver.cpp b/src/nlsat/nlsat_solver.cpp index 00fc58962..ed4e50c38 100644 --- a/src/nlsat/nlsat_solver.cpp +++ b/src/nlsat/nlsat_solver.cpp @@ -2034,7 +2034,7 @@ namespace nlsat { m_assignment.reset(); } - lbool check(literal_vector& assumptions, assignment const& rvalues, polynomial_ref_vector& core) { + lbool check(assignment const& rvalues, atom_vector& core) { return l_undef; } @@ -4108,8 +4108,8 @@ namespace nlsat { return m_imp->check(assumptions); } - lbool solver::check(literal_vector& assumptions, assignment const& rvalues, polynomial_ref_vector& core) { - return m_imp->check(assumptions, rvalues, core); + lbool solver::check(assignment const& rvalues, atom_vector& clause) { + return m_imp->check(rvalues, clause); } void solver::get_core(vector& assumptions) { diff --git a/src/nlsat/nlsat_solver.h b/src/nlsat/nlsat_solver.h index ddff95255..f9f46d494 100644 --- a/src/nlsat/nlsat_solver.h +++ b/src/nlsat/nlsat_solver.h @@ -219,17 +219,17 @@ namespace nlsat { lbool check(literal_vector& assumptions); // - // check satisfiability of asserted formulas relative to 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 - update the list of assumptions (possibly reset it to empty), and a set of polynomials in core, + // l_false - the conjunction of literals from get_core, and negations of atoms in clause, // such that the conjunction of the assumptions and the polynomials in core is unsatisfiable. // l_undef - if the search was interrupted by a resource limit. - // Core is a list of polynomials. We associate literals as follows: TBD + // clause is a list of atoms. Their negations conjoined with core literals are unsatisfiable. // Different implementations of check are possible. One where core comprises of linear polynomials could // produce lemmas that are friendly to linear arithmetic solvers. // - lbool check(literal_vector& assumptions, assignment const& rvalues, polynomial_ref_vector& core); + lbool check(assignment const& rvalues, atom_vector& clause); // ----------------------- // From 10cb358f9fd00452f25dd24638a1e165fcfec57b Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 11 Jul 2025 22:29:33 +0200 Subject: [PATCH 05/42] add marshaling from nlsat lemmas into core solver Signed-off-by: Nikolaj Bjorner --- src/math/lp/nra_solver.cpp | 110 ++++++++++++++++++++++++------------- 1 file changed, 73 insertions(+), 37 deletions(-) diff --git a/src/math/lp/nra_solver.cpp b/src/math/lp/nra_solver.cpp index 419504502..cad04e9b9 100644 --- a/src/math/lp/nra_solver.cpp +++ b/src/math/lp/nra_solver.cpp @@ -228,14 +228,8 @@ struct solver::imp { validate_constraints(); break; case l_false: { - vector core; lp::explanation ex; - m_nlsat->get_core(core); - for (auto c : core) { - unsigned idx = static_cast(static_cast(c) - this); - ex.push_back(idx); - TRACE(nra, lra.display_constraint(tout << "ex: " << idx << ": ", idx) << "\n";); - } + constraint_core2ex(ex); nla::lemma_builder lemma(m_nla_core, __FUNCTION__); lemma &= ex; m_nla_core.set_use_nra_model(true); @@ -252,8 +246,8 @@ struct solver::imp { lbool r = l_undef; statistics& st = m_nla_core.lp_settings().stats().m_st; nlsat::atom_vector clause; + polynomial::manager& pm = m_nlsat->pm(); try { - polynomial::manager& pm = m_nlsat->pm(); nlsat::assignment rvalues(m_nlsat->am()); for (auto [j, x] : m_lp2nl) { scoped_anum a(am()); @@ -262,10 +256,12 @@ struct solver::imp { } r = m_nlsat->check(rvalues, clause); - } catch (z3_exception&) { + } + catch (z3_exception&) { if (m_limit.is_canceled()) { r = l_undef; - } else { + } + else { m_nlsat->collect_statistics(st); throw; } @@ -282,14 +278,11 @@ struct solver::imp { validate_constraints(); break; case l_false: { - vector core; lp::explanation ex; - m_nlsat->get_core(core); - for (auto c : core) { - unsigned idx = static_cast(static_cast(c) - this); - ex.push_back(idx); - TRACE(nra, lra.display_constraint(tout << "ex: " << idx << ": ", idx) << "\n";); - } + constraint_core2ex(ex); + u_map nl2lp; + for (auto [j, x] : m_lp2nl) + nl2lp.insert(x, j); for (auto a : clause) { // a cannot be a root object. SASSERT(!a->is_root_atom()); @@ -297,31 +290,64 @@ struct solver::imp { auto& ia = *to_ineq_atom(a); VERIFY(ia.size() == 1); // deal with factored polynomials later // a is an inequality atom, i.e., p > 0, p < 0, or p = 0. - polynomial::polynomial* p = ia.p(0); - - #if 0 - // convert poloynomial into monomials etc. - #endif + polynomial::polynomial const* p = ia.p(0); + unsigned num_mon = pm.size(p); + rational bound(0); + lp::lar_term t; + + nla::lemma_builder lemma(m_nla_core, __FUNCTION__); + lemma &= ex; + for (unsigned i = 0; i < num_mon; ++i) { + polynomial::monomial* m = pm.get_monomial(p, i); + auto& coeff = pm.coeff(p, i); + unsigned num_vars = pm.size(m); + lp::lpvar v = lp::null_lpvar; + // add mon * coeff to t; + switch (num_vars) { + case 0: + bound -= coeff; + break; + case 1: + 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)]); + auto mon = m_nla_core.emons().find_canonical(vars); + if (mon) + v = mon->var(); + else { + return l_undef; + // this one is for Lev Nachmanson: lar_solver relies on internal variables + // to have terms from outside. The solver doesn't get to create + // its own monomials. + // v = ... + // It is not a use case if the nlsat solver only provides linear + // polynomials so punt for now. + m_nla_core.add_monic(v, vars.size(), vars.data()); + } + t.add_monomial(coeff, v); + break; + } + } + } + switch (a->get_kind()) { - case nlsat::atom::EQ: { - NOT_IMPLEMENTED_YET(); - break; - } - case nlsat::atom::LT: { - NOT_IMPLEMENTED_YET(); - break; - } - case nlsat::atom::GT: { - NOT_IMPLEMENTED_YET(); - break; - } + case nlsat::atom::EQ: + lemma |= nla::ineq(lp::lconstraint_kind::EQ, t, bound); + break; + case nlsat::atom::LT: + lemma |= nla::ineq(lp::lconstraint_kind::LT, t, bound); + break; + case nlsat::atom::GT: + lemma |= nla::ineq(lp::lconstraint_kind::GT, t, bound); + break; default: UNREACHABLE(); } } - - nla::lemma_builder lemma(m_nla_core, __FUNCTION__); - lemma &= ex; m_nla_core.set_use_nra_model(true); break; } @@ -331,6 +357,16 @@ struct solver::imp { return r; } + void constraint_core2ex(lp::explanation& ex) { + vector core; + m_nlsat->get_core(core); + for (auto c : core) { + unsigned idx = static_cast(static_cast(c) - this); + ex.push_back(idx); + TRACE(nra, lra.display_constraint(tout << "ex: " << idx << ": ", idx) << "\n";); + } + } + void add_monic_eq_bound(mon_eq const& m) { if (!lra.column_has_lower_bound(m.var()) && From d2ada6a77263d73db1ef20f9baf1665698765b3b Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 11 Jul 2025 22:40:55 +0200 Subject: [PATCH 06/42] tidy Signed-off-by: Nikolaj Bjorner --- src/math/lp/nra_solver.cpp | 19 +++++++++++++------ 1 file changed, 13 insertions(+), 6 deletions(-) diff --git a/src/math/lp/nra_solver.cpp b/src/math/lp/nra_solver.cpp index cad04e9b9..3817bf70b 100644 --- a/src/math/lp/nra_solver.cpp +++ b/src/math/lp/nra_solver.cpp @@ -189,6 +189,16 @@ struct solver::imp { } } + bool check_constraints() { + for (lp::constraint_index ci : lra.constraints().indices()) + if (!check_constraint(ci)) + return false; + for (auto const& m : m_nla_core.emons()) + if (!check_monic(m)) + return false; + return true; + } + /** \brief one-shot nlsat check. A one shot checker is the least functionality that can @@ -319,6 +329,7 @@ struct solver::imp { if (mon) v = mon->var(); else { + NOT_IMPLEMENTED_YET(); return l_undef; // this one is for Lev Nachmanson: lar_solver relies on internal variables // to have terms from outside. The solver doesn't get to create @@ -527,12 +538,8 @@ struct solver::imp { 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; + if (!check_constraints()) + return l_undef; break; case l_false: { lp::explanation ex; From a38af61d777659e56afc97d9a8df2181e4a721bb Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 20 Aug 2025 07:32:50 -0700 Subject: [PATCH 07/42] add call to check-assignment Signed-off-by: Nikolaj Bjorner --- src/math/lp/nla_core.cpp | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp index 5a74f882f..7795af30f 100644 --- a/src/math/lp/nla_core.cpp +++ b/src/math/lp/nla_core.cpp @@ -1538,6 +1538,13 @@ lbool core::check() { if (no_effect()) m_divisions.check(); + bool use_nra_linearization = true; + + if (no_effect() && use_nra_linearization) { + scoped_limits sl(m_reslim); + sl.push_child(&m_nra_lim); + ret = m_nra.check_assignment(); + } if (no_effect()) { std::function check1 = [&]() { m_order.order_lemma(); From 4b4e8cbc6ed7c77e2bb06778bf6cae3eb8a40811 Mon Sep 17 00:00:00 2001 From: ValentinPromies <44966217+ValentinPromies@users.noreply.github.com> Date: Wed, 20 Aug 2025 16:36:35 +0200 Subject: [PATCH 08/42] Nl2lin (#7795) * add linearized projection in nlsat * implement nlsat check for given assignment * add some comments --- src/nlsat/nlsat_explain.cpp | 212 +++++++++++++++++++++++++++++++++++- src/nlsat/nlsat_explain.h | 1 + src/nlsat/nlsat_solver.cpp | 61 ++++++++++- 3 files changed, 272 insertions(+), 2 deletions(-) diff --git a/src/nlsat/nlsat_explain.cpp b/src/nlsat/nlsat_explain.cpp index 92a0428a2..19c6316d5 100644 --- a/src/nlsat/nlsat_explain.cpp +++ b/src/nlsat/nlsat_explain.cpp @@ -45,6 +45,7 @@ namespace nlsat { bool m_minimize_cores; bool m_factor; bool m_signed_project; + bool m_linear_project; bool m_cell_sample; @@ -155,6 +156,7 @@ namespace nlsat { m_full_dimensional = false; m_minimize_cores = false; m_signed_project = false; + m_linear_project = false; } std::ostream& display(std::ostream & out, polynomial_ref const & p) const { @@ -1262,8 +1264,212 @@ namespace nlsat { } } + + /** + * \brief add cell literals for the linearized projection and categorize the polynomials in ps + * - ps_below will contain all polynomials from ps which have a root below m_assignment w.r.t. x + * - ps_above will contain all polynomials from ps which have a root above m_assignment w.r.t. x + * - ps_equal will contain at least one polynomial from ps which have a root equal to m_assignment + * - In addition, they may contain additional linear polynomials added as cell boundaries + * - The back elements of ps_below, ps_above, ps_equal are the polynomials used for the cell literals + */ + void add_cell_lits_linear(polynomial_ref_vector const& ps, + var const x, + polynomial_ref_vector& ps_below, + polynomial_ref_vector& ps_above, + polynomial_ref_vector& ps_equal) { + ps_below.reset(); + ps_above.reset(); + ps_equal.reset(); + + SASSERT(m_assignment.is_assigned(x)); + anum const & x_val = m_assignment.value(x); + + bool lower_inf = true, upper_inf = true; + scoped_anum lower(m_am), upper(m_am); + polynomial_ref p_lower(m_pm), p_upper(m_pm); + unsigned i_lower = UINT_MAX, i_upper = UINT_MAX; + + scoped_anum_vector & roots = m_roots_tmp; + polynomial_ref p(m_pm); + + unsigned sz = ps.size(); + for (unsigned k = 0; k < sz; k++) { + p = ps.get(k); + if (max_var(p) != x) + continue; + roots.reset(); + + // Temporarily unassign x, s.t. isolate_roots does not assume p as constant. + m_am.isolate_roots(p, undef_var_assignment(m_assignment, x), roots); + unsigned num_roots = roots.size(); + if (num_roots == 0) continue; + + // find p's smallest root above the sample + unsigned i = 0; + int s = 1; + for (; i < num_roots; ++i) { + s = m_am.compare(x_val, roots[i]); + if (s <= 0) break; + } + + if (s == 0) { + // roots[i] == x_val + ps_equal.push_back(p); + p_lower = p; + i_lower = i+1; + break; // TODO: choose the best among multiple section polynomials? + } else if (s < 0) { + // x_val < roots[i] + ps_above.push_back(p); + if (upper_inf || m_am.lt(roots[i], upper)) { + upper_inf = false; + m_am.set(upper, roots[i]); + p_upper = p; + i_upper = i + 1; + } + } + // in any case, roots[i-1] might provide a lower bound if it exists + if (i > 0) { + // roots[i-1] < x_val + ps_below.push_back(p); + if (lower_inf || m_am.lt(lower, roots[i-1])) { + lower_inf = false; + m_am.set(lower, roots[i-1]); + p_lower = p; + i_lower = i; + } + } + } + + // add linear cell bounds + + if (!ps_equal.empty()) { + if (!m_am.is_rational(x_val)) { + // TODO: FAIL + NOT_IMPLEMENTED_YET(); + } else if (m_pm.total_degree(p_lower) > 1) { + rational bound; + m_am.to_rational(x_val, bound); + p_lower = m_pm.mk_polynomial(x); + p_lower = p_lower - bound; + } + add_root_literal(atom::ROOT_EQ, x, 1, p_lower); + // make sure bounding poly is at the back of the vector + ps_equal.push_back(p_lower); + return; + } + if (!lower_inf) { + bool approximate = (m_pm.total_degree(p_lower) > 1); + if (approximate) { + scoped_anum between(m_am); + m_am.select(lower, x_val, between); + rational new_bound; + m_am.to_rational(between, new_bound); + p_lower = m_pm.mk_polynomial(x); + p_lower = p_lower - new_bound; + } + add_root_literal((approximate || m_full_dimensional) ? atom::ROOT_GE : atom::ROOT_GT, x, 1, p_lower); + // make sure bounding poly is at the back of the vector + ps_below.push_back(p_lower); + } + if (!upper_inf) { + bool approximate = (m_pm.total_degree(p_upper) > 1); + if (approximate) { + scoped_anum between(m_am); + m_am.select(x_val, upper, between); + rational new_bound; + m_am.to_rational(between, new_bound); + p_upper = m_pm.mk_polynomial(x); + p_upper = p_upper - new_bound; + } + add_root_literal((approximate || m_full_dimensional) ? atom::ROOT_LE : atom::ROOT_LT, x, 1, p_upper); + // make sure bounding poly is at the back of the vector + ps_below.push_back(p_upper); + } + } + + + /** + * \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); + } + } + + + /** + * Linearized projection based on: + * Valentin Promies, Jasper Nalbach, Erika Abraham and Paul Wagner + * "More is Less: Adding Polynomials for Faster Explanations in NLSAT" + * in CADE30, 2025 + */ + void project_linear(polynomial_ref_vector & ps, var max_x) { + if (ps.empty()) + return; + m_todo.reset(); + for (poly* p : ps) { + m_todo.insert(p); + } + + polynomial_ref_vector ps_below_sample(m_pm); + polynomial_ref_vector ps_above_sample(m_pm); + polynomial_ref_vector ps_equal_sample(m_pm); + var x = m_todo.extract_max_polys(ps); + if (x == max_x) { + // top level projection like original + // we could also do a covering-style projection, sparing some resultants + add_lcs(ps, x); + psc_discriminant(ps, x); + psc_resultant(ps, x); + x = m_todo.extract_max_polys(ps); + } + + while(!m_todo.empty()) { + add_cell_lits_linear(ps, x, ps_below_sample, ps_above_sample, ps_equal_sample); + if (all_univ(ps, x) && m_todo.empty()) { + m_todo.reset(); + break; + } + add_lcs(ps, x); + psc_discriminant(ps, x); + polynomial_ref lb(m_pm); + polynomial_ref ub(m_pm); + + if (!ps_equal_sample.empty()) { + // section + lb = ps_equal_sample.back(); + psc_resultants_with(ps, lb, x); + } else { + if (!ps_below_sample.empty()) { + lb = ps_below_sample.back(); + psc_resultants_with(ps_below_sample, lb, x); + } + if (!ps_above_sample.empty()) { + ub = ps_above_sample.back(); + psc_resultants_with(ps_above_sample, ub, x); + if (!ps_below_sample.empty()) { + // also need resultant between bounds + psc(lb, ub, x); + } + } + } + x = m_todo.extract_max_polys(ps); + } + } + + void project(polynomial_ref_vector & ps, var max_x) { - if (m_cell_sample) { + if (m_linear_project) { + project_linear(ps, max_x); + } + else if (m_cell_sample) { project_cdcac(ps, max_x); } else { @@ -2126,6 +2332,10 @@ namespace nlsat { m_imp->m_signed_project = f; } + void explain::set_linear_project(bool f) { + m_imp->m_linear_project = f; + } + void explain::main_operator(unsigned n, literal const * ls, scoped_literal_vector & result) { (*m_imp)(n, ls, result); } diff --git a/src/nlsat/nlsat_explain.h b/src/nlsat/nlsat_explain.h index 6e1cf091b..316a1367e 100644 --- a/src/nlsat/nlsat_explain.h +++ b/src/nlsat/nlsat_explain.h @@ -45,6 +45,7 @@ namespace nlsat { void set_minimize_cores(bool f); void set_factor(bool f); void set_signed_project(bool f); + void set_linear_project(bool f); /** \brief Given a set of literals ls[0], ... ls[n-1] s.t. diff --git a/src/nlsat/nlsat_solver.cpp b/src/nlsat/nlsat_solver.cpp index ed4e50c38..34109578c 100644 --- a/src/nlsat/nlsat_solver.cpp +++ b/src/nlsat/nlsat_solver.cpp @@ -2035,7 +2035,66 @@ namespace nlsat { } lbool check(assignment const& rvalues, atom_vector& core) { - return l_undef; + // 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; + unsigned sz = m_clauses.size(); + lbool satisfied = l_true; + for (unsigned i = 0; i < sz; i++) { + bool c_satisfied = false; + clause const & c = *(m_clauses[i]); + for (literal l : c) { + if (const_cast(this)->value(l) != l_false) { + c_satisfied = true; + break; + } + } + if (c_satisfied) 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 (satisfied == l_true) { + // nothing to do + return l_true; + } + if (satisfied == l_undef) { + // nothing to do? + return l_undef; + } + + // assignment does not satisfy the constraints -> create lemma + SASSERT(best_literal != null_literal); + m_lazy_clause.reset(); + m_explain.set_linear_project(true); + m_explain.main_operator(1, &best_literal, m_lazy_clause); + m_explain.set_linear_project(false); // TODO: there should be a better way to control this. + m_lazy_clause.push_back(~best_literal); + + core.clear(); + for (literal l : m_lazy_clause) { + core.push_back(m_atoms[l.var()]); + } + + m_assignment.reset(); + m_assignment.copy(tmp); + return l_false; } lbool check(literal_vector& assumptions) { From 964dd2a71ae398149b4bcba27ce41318af735a64 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 20 Aug 2025 07:46:53 -0700 Subject: [PATCH 09/42] fixup loop Signed-off-by: Nikolaj Bjorner --- src/nlsat/nlsat_explain.cpp | 12 ++++++++---- src/nlsat/nlsat_solver.cpp | 31 ++++++++++++++----------------- 2 files changed, 22 insertions(+), 21 deletions(-) diff --git a/src/nlsat/nlsat_explain.cpp b/src/nlsat/nlsat_explain.cpp index 19c6316d5..55c5f5315 100644 --- a/src/nlsat/nlsat_explain.cpp +++ b/src/nlsat/nlsat_explain.cpp @@ -1303,7 +1303,8 @@ namespace nlsat { // Temporarily unassign x, s.t. isolate_roots does not assume p as constant. m_am.isolate_roots(p, undef_var_assignment(m_assignment, x), roots); unsigned num_roots = roots.size(); - if (num_roots == 0) continue; + if (num_roots == 0) + continue; // find p's smallest root above the sample unsigned i = 0; @@ -1319,7 +1320,8 @@ namespace nlsat { p_lower = p; i_lower = i+1; break; // TODO: choose the best among multiple section polynomials? - } else if (s < 0) { + } + else if (s < 0) { // x_val < roots[i] ps_above.push_back(p); if (upper_inf || m_am.lt(roots[i], upper)) { @@ -1348,7 +1350,8 @@ namespace nlsat { if (!m_am.is_rational(x_val)) { // TODO: FAIL NOT_IMPLEMENTED_YET(); - } else if (m_pm.total_degree(p_lower) > 1) { + } + else if (m_pm.total_degree(p_lower) > 1) { rational bound; m_am.to_rational(x_val, bound); p_lower = m_pm.mk_polynomial(x); @@ -1446,7 +1449,8 @@ namespace nlsat { // section lb = ps_equal_sample.back(); psc_resultants_with(ps, lb, x); - } else { + } + else { if (!ps_below_sample.empty()) { lb = ps_below_sample.back(); psc_resultants_with(ps_below_sample, lb, x); diff --git a/src/nlsat/nlsat_solver.cpp b/src/nlsat/nlsat_solver.cpp index 34109578c..8631fa0b8 100644 --- a/src/nlsat/nlsat_solver.cpp +++ b/src/nlsat/nlsat_solver.cpp @@ -2044,22 +2044,24 @@ namespace nlsat { literal best_literal = null_literal; unsigned sz = m_clauses.size(); lbool satisfied = l_true; - for (unsigned i = 0; i < sz; i++) { - bool c_satisfied = false; - clause const & c = *(m_clauses[i]); - for (literal l : c) { - if (const_cast(this)->value(l) != l_false) { - c_satisfied = true; - break; - } + 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; } - if (c_satisfied) continue; // take best literal from c for (literal l : c) { if (best_literal == null_literal) { best_literal = l; - } else { + } + 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])) { @@ -2070,14 +2072,9 @@ namespace nlsat { } } - if (satisfied == l_true) { - // nothing to do - return l_true; - } - if (satisfied == l_undef) { - // nothing to do? + if (best_literal == null_literal) + return satisfied; return l_undef; - } // assignment does not satisfy the constraints -> create lemma SASSERT(best_literal != null_literal); From d15c0e396e37fc7b001be8a6705664d3a3170e25 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 20 Aug 2025 07:53:43 -0700 Subject: [PATCH 10/42] updates Signed-off-by: Nikolaj Bjorner --- src/nlsat/nlsat_explain.cpp | 30 +++++++++++++----------------- src/nlsat/nlsat_explain.h | 2 ++ src/nlsat/nlsat_solver.cpp | 5 +---- 3 files changed, 16 insertions(+), 21 deletions(-) diff --git a/src/nlsat/nlsat_explain.cpp b/src/nlsat/nlsat_explain.cpp index 55c5f5315..234109939 100644 --- a/src/nlsat/nlsat_explain.cpp +++ b/src/nlsat/nlsat_explain.cpp @@ -45,8 +45,8 @@ namespace nlsat { bool m_minimize_cores; bool m_factor; bool m_signed_project; - bool m_linear_project; bool m_cell_sample; + bool m_linear_project = false; struct todo_set { @@ -156,7 +156,6 @@ namespace nlsat { m_full_dimensional = false; m_minimize_cores = false; m_signed_project = false; - m_linear_project = false; } std::ostream& display(std::ostream & out, polynomial_ref const & p) const { @@ -1413,7 +1412,7 @@ namespace nlsat { * "More is Less: Adding Polynomials for Faster Explanations in NLSAT" * in CADE30, 2025 */ - void project_linear(polynomial_ref_vector & ps, var max_x) { + void linear_project(polynomial_ref_vector & ps, var max_x) { if (ps.empty()) return; m_todo.reset(); @@ -1434,7 +1433,7 @@ namespace nlsat { x = m_todo.extract_max_polys(ps); } - while(!m_todo.empty()) { + while (!m_todo.empty()) { add_cell_lits_linear(ps, x, ps_below_sample, ps_above_sample, ps_equal_sample); if (all_univ(ps, x) && m_todo.empty()) { m_todo.reset(); @@ -1470,15 +1469,12 @@ namespace nlsat { void project(polynomial_ref_vector & ps, var max_x) { - if (m_linear_project) { - project_linear(ps, max_x); - } - else if (m_cell_sample) { - project_cdcac(ps, max_x); - } - else { - project_original(ps, max_x); - } + if (m_linear_project) + linear_project(ps, max_x); + else if (m_cell_sample) + project_cdcac(ps, max_x); + else + project_original(ps, max_x); } bool check_already_added() const { @@ -2336,14 +2332,14 @@ namespace nlsat { m_imp->m_signed_project = f; } - void explain::set_linear_project(bool f) { - m_imp->m_linear_project = f; - } - void explain::main_operator(unsigned n, literal const * ls, scoped_literal_vector & result) { (*m_imp)(n, ls, result); } + void explain::linear_project(unsigned n, literal const* ls, scoped_literal_vector& result) { + m_imp->linear_project(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 316a1367e..de9502c9b 100644 --- a/src/nlsat/nlsat_explain.h +++ b/src/nlsat/nlsat_explain.h @@ -66,6 +66,8 @@ namespace nlsat { */ void main_operator(unsigned n, literal const * ls, scoped_literal_vector & result); + void linear_project(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 8631fa0b8..a6f11256a 100644 --- a/src/nlsat/nlsat_solver.cpp +++ b/src/nlsat/nlsat_solver.cpp @@ -2074,14 +2074,11 @@ namespace nlsat { if (best_literal == null_literal) return satisfied; - return l_undef; // assignment does not satisfy the constraints -> create lemma SASSERT(best_literal != null_literal); m_lazy_clause.reset(); - m_explain.set_linear_project(true); - m_explain.main_operator(1, &best_literal, m_lazy_clause); - m_explain.set_linear_project(false); // TODO: there should be a better way to control this. + m_explain.linear_project(1, &best_literal, m_lazy_clause); m_lazy_clause.push_back(~best_literal); core.clear(); From 5d08ebdffdc92988811114987f6c6ce25d6b3dfa Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 20 Aug 2025 08:02:31 -0700 Subject: [PATCH 11/42] fixes Signed-off-by: Nikolaj Bjorner --- src/math/lp/nla_core.cpp | 1 + src/math/lp/nra_solver.cpp | 2 ++ src/nlsat/nlsat_explain.cpp | 8 ++++---- src/nlsat/nlsat_explain.h | 2 -- src/nlsat/nlsat_solver.cpp | 4 +++- 5 files changed, 10 insertions(+), 7 deletions(-) diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp index 7795af30f..040f754ef 100644 --- a/src/math/lp/nla_core.cpp +++ b/src/math/lp/nla_core.cpp @@ -1544,6 +1544,7 @@ lbool core::check() { scoped_limits sl(m_reslim); sl.push_child(&m_nra_lim); ret = m_nra.check_assignment(); + IF_VERBOSE(1, verbose_stream() << "nra check_assignment returned " << ret << "\n";); } if (no_effect()) { diff --git a/src/math/lp/nra_solver.cpp b/src/math/lp/nra_solver.cpp index 3817bf70b..f25cd97e4 100644 --- a/src/math/lp/nra_solver.cpp +++ b/src/math/lp/nra_solver.cpp @@ -358,6 +358,8 @@ struct solver::imp { default: UNREACHABLE(); } + + IF_VERBOSE(1, verbose_stream() << "linear lemma: " << lemma << "\n"); } m_nla_core.set_use_nra_model(true); break; diff --git a/src/nlsat/nlsat_explain.cpp b/src/nlsat/nlsat_explain.cpp index 234109939..c7fa51825 100644 --- a/src/nlsat/nlsat_explain.cpp +++ b/src/nlsat/nlsat_explain.cpp @@ -2316,6 +2316,10 @@ namespace nlsat { m_imp->m_simplify_cores = f; } + void explain::set_linear_project(bool f) { + m_imp->m_linear_project = f; + } + void explain::set_full_dimensional(bool f) { m_imp->m_full_dimensional = f; } @@ -2336,10 +2340,6 @@ namespace nlsat { (*m_imp)(n, ls, result); } - void explain::linear_project(unsigned n, literal const* ls, scoped_literal_vector& result) { - m_imp->linear_project(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 de9502c9b..316a1367e 100644 --- a/src/nlsat/nlsat_explain.h +++ b/src/nlsat/nlsat_explain.h @@ -66,8 +66,6 @@ namespace nlsat { */ void main_operator(unsigned n, literal const * ls, scoped_literal_vector & result); - void linear_project(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 a6f11256a..0961f4ee0 100644 --- a/src/nlsat/nlsat_solver.cpp +++ b/src/nlsat/nlsat_solver.cpp @@ -2078,7 +2078,9 @@ namespace nlsat { // assignment does not satisfy the constraints -> create lemma SASSERT(best_literal != null_literal); m_lazy_clause.reset(); - m_explain.linear_project(1, &best_literal, m_lazy_clause); + m_explain.set_linear_project(true); + m_explain.main_operator(1, &best_literal, m_lazy_clause); + m_explain.set_linear_project(false); m_lazy_clause.push_back(~best_literal); core.clear(); From 6ef8a0b7bb798720cc44f7fe4c6e9a737c59f147 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Wed, 20 Aug 2025 15:59:11 -0700 Subject: [PATCH 12/42] debug nl2lin Signed-off-by: Lev Nachmanson --- src/math/lp/nla_core.cpp | 9 ++++++++- src/math/lp/nla_core.h | 10 +++++----- src/math/lp/nra_solver.cpp | 16 +++++++++++----- 3 files changed, 24 insertions(+), 11 deletions(-) diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp index 040f754ef..6975c972a 100644 --- a/src/math/lp/nla_core.cpp +++ b/src/math/lp/nla_core.cpp @@ -1,4 +1,4 @@ - /*++ +/*++ Copyright (c) 2017 Microsoft Corporation Module Name: @@ -88,6 +88,13 @@ lpvar core::map_to_root(lpvar j) const { return m_evars.find(j).var(); } +// Reduce a single variable to its root and provide the reduction sign. +lpvar core::reduce_var_to_rooted(lpvar j, rational & sign) const { + auto root = m_evars.find(j); + sign = rational(root.sign() ? -1 : 1); + return root.var(); +} + svector core::sorted_rvars(const factor& f) const { if (f.is_var()) { svector r; r.push_back(map_to_root(f.var())); diff --git a/src/math/lp/nla_core.h b/src/math/lp/nla_core.h index e06faafff..684b58d01 100644 --- a/src/math/lp/nla_core.h +++ b/src/math/lp/nla_core.h @@ -281,8 +281,12 @@ public: svector reduce_monic_to_rooted(const svector & vars, rational & sign) const; - monic_coeff canonize_monic(monic const& m) const; + // Reduce a single variable to its canonical root under current equalities + // and return the convertion sign as either 1 or -1 + lpvar reduce_var_to_rooted(lpvar v, rational & sign) const; + monic_coeff canonize_monic(monic const& m) const; + int vars_sign(const svector& v); bool has_upper_bound(lpvar j) const; bool has_lower_bound(lpvar j) const; @@ -357,10 +361,6 @@ public: template bool vars_are_roots(const T& v) const; - void register_monic_in_tables(unsigned i_mon); - - void register_monics_in_tables(); - void clear(); void init_search(); diff --git a/src/math/lp/nra_solver.cpp b/src/math/lp/nra_solver.cpp index f25cd97e4..9e221e6ea 100644 --- a/src/math/lp/nra_solver.cpp +++ b/src/math/lp/nra_solver.cpp @@ -280,6 +280,7 @@ struct solver::imp { TRACE(nra, m_nlsat->display(tout << r << "\n"); display(tout); + tout << "m_lp2nl:\n"; for (auto [j, x] : m_lp2nl) tout << "j" << j << " := x" << x << "\n";); switch (r) { case l_true: @@ -317,14 +318,19 @@ struct solver::imp { case 0: bound -= coeff; break; - case 1: - v = nl2lp[pm.get_var(m, 0)]; - t.add_monomial(coeff, v); + case 1: { + v = nl2lp[pm.get_var(m, 0)]; + rational s; + v = m_nla_core.reduce_var_to_rooted(v, s); + t.add_monomial(s * coeff, v); + } break; default: { svector vars; for (unsigned j = 0; j < num_vars; ++j) vars.push_back(nl2lp[pm.get_var(m, j)]); + rational s(1); + vars = m_nla_core.reduce_monic_to_rooted(vars, s); auto mon = m_nla_core.emons().find_canonical(vars); if (mon) v = mon->var(); @@ -339,12 +345,12 @@ struct solver::imp { // polynomials so punt for now. m_nla_core.add_monic(v, vars.size(), vars.data()); } - t.add_monomial(coeff, v); + t.add_monomial(s * coeff, v); break; } } } - + TRACE(nra, this->lra.print_term(t, tout << "t:") << std::endl;); switch (a->get_kind()) { case nlsat::atom::EQ: lemma |= nla::ineq(lp::lconstraint_kind::EQ, t, bound); From 187f013224906c0e7e32c5bd7a2567a05f1aaf14 Mon Sep 17 00:00:00 2001 From: ValentinPromies <44966217+ValentinPromies@users.noreply.github.com> Date: Thu, 28 Aug 2025 17:17:37 +0200 Subject: [PATCH 13/42] Nl2lin (#7827) * fix linear projection * fix linear projection * use an explicit cell description in check_assignment --- src/math/lp/nra_solver.cpp | 44 ++++++++++++++++++++----------------- src/nlsat/nlsat_explain.cpp | 22 +++++++++---------- src/nlsat/nlsat_solver.cpp | 20 ++++++++++------- src/nlsat/nlsat_solver.h | 3 ++- 4 files changed, 48 insertions(+), 41 deletions(-) diff --git a/src/math/lp/nra_solver.cpp b/src/math/lp/nra_solver.cpp index 9e221e6ea..b4f0cbe70 100644 --- a/src/math/lp/nra_solver.cpp +++ b/src/math/lp/nra_solver.cpp @@ -256,6 +256,7 @@ struct solver::imp { lbool r = l_undef; statistics& st = m_nla_core.lp_settings().stats().m_st; nlsat::atom_vector clause; + nlsat::literal_vector cell; polynomial::manager& pm = m_nlsat->pm(); try { nlsat::assignment rvalues(m_nlsat->am()); @@ -264,8 +265,7 @@ struct solver::imp { am().set(a, m_nla_core.val(j).to_mpq()); rvalues.set(x, a); } - r = m_nlsat->check(rvalues, clause); - + r = m_nlsat->check(rvalues, clause, cell); } catch (z3_exception&) { if (m_limit.is_canceled()) { @@ -294,8 +294,11 @@ struct solver::imp { u_map nl2lp; for (auto [j, x] : m_lp2nl) nl2lp.insert(x, j); - for (auto a : clause) { - // a cannot be a root object. + + nla::lemma_builder lemma(m_nla_core, __FUNCTION__); + lemma &= ex; + + auto translate_atom = [&](nlsat::atom* a, bool negated){ SASSERT(!a->is_root_atom()); SASSERT(a->is_ineq_atom()); auto& ia = *to_ineq_atom(a); @@ -305,9 +308,6 @@ struct solver::imp { unsigned num_mon = pm.size(p); rational bound(0); lp::lar_term t; - - nla::lemma_builder lemma(m_nla_core, __FUNCTION__); - lemma &= ex; for (unsigned i = 0; i < num_mon; ++i) { polynomial::monomial* m = pm.get_monomial(p, i); auto& coeff = pm.coeff(p, i); @@ -336,7 +336,6 @@ struct solver::imp { v = mon->var(); else { NOT_IMPLEMENTED_YET(); - return l_undef; // this one is for Lev Nachmanson: lar_solver relies on internal variables // to have terms from outside. The solver doesn't get to create // its own monomials. @@ -349,24 +348,29 @@ struct solver::imp { break; } } - } - TRACE(nra, this->lra.print_term(t, tout << "t:") << std::endl;); + } switch (a->get_kind()) { - case nlsat::atom::EQ: - lemma |= nla::ineq(lp::lconstraint_kind::EQ, t, bound); - break; - case nlsat::atom::LT: - lemma |= nla::ineq(lp::lconstraint_kind::LT, t, bound); - break; - case nlsat::atom::GT: - lemma |= nla::ineq(lp::lconstraint_kind::GT, t, bound); - break; + case nlsat::atom::EQ: + return nla::ineq(negated ? lp::lconstraint_kind::NE : lp::lconstraint_kind::EQ, t, bound); + case nlsat::atom::LT: + return nla::ineq(negated ? lp::lconstraint_kind::GE : lp::lconstraint_kind::LT, t, bound); + case nlsat::atom::GT: + return nla::ineq(negated ? lp::lconstraint_kind::LE : lp::lconstraint_kind::GT, t, bound); default: UNREACHABLE(); } + }; - IF_VERBOSE(1, verbose_stream() << "linear lemma: " << lemma << "\n"); + + for (auto a : clause) { + lemma |= translate_atom(a, true); } + + for (nlsat::literal l : cell) { + lemma |= translate_atom( m_nlsat->bool_var2atom(l.var()), l.sign()); + } + + IF_VERBOSE(1, verbose_stream() << "linear lemma: " << lemma << "\n"); m_nla_core.set_use_nra_model(true); break; } diff --git a/src/nlsat/nlsat_explain.cpp b/src/nlsat/nlsat_explain.cpp index c7fa51825..13ad4f41c 100644 --- a/src/nlsat/nlsat_explain.cpp +++ b/src/nlsat/nlsat_explain.cpp @@ -1287,7 +1287,6 @@ namespace nlsat { bool lower_inf = true, upper_inf = true; scoped_anum lower(m_am), upper(m_am); polynomial_ref p_lower(m_pm), p_upper(m_pm); - unsigned i_lower = UINT_MAX, i_upper = UINT_MAX; scoped_anum_vector & roots = m_roots_tmp; polynomial_ref p(m_pm); @@ -1317,7 +1316,6 @@ namespace nlsat { // roots[i] == x_val ps_equal.push_back(p); p_lower = p; - i_lower = i+1; break; // TODO: choose the best among multiple section polynomials? } else if (s < 0) { @@ -1327,7 +1325,6 @@ namespace nlsat { upper_inf = false; m_am.set(upper, roots[i]); p_upper = p; - i_upper = i + 1; } } // in any case, roots[i-1] might provide a lower bound if it exists @@ -1338,7 +1335,6 @@ namespace nlsat { lower_inf = false; m_am.set(lower, roots[i-1]); p_lower = p; - i_lower = i; } } } @@ -1354,7 +1350,7 @@ namespace nlsat { rational bound; m_am.to_rational(x_val, bound); p_lower = m_pm.mk_polynomial(x); - p_lower = p_lower - bound; + p_lower = denominator(bound)*p_lower - numerator(bound); } add_root_literal(atom::ROOT_EQ, x, 1, p_lower); // make sure bounding poly is at the back of the vector @@ -1369,9 +1365,9 @@ namespace nlsat { rational new_bound; m_am.to_rational(between, new_bound); p_lower = m_pm.mk_polynomial(x); - p_lower = p_lower - new_bound; + p_lower = denominator(new_bound)*p_lower - numerator(new_bound); } - add_root_literal((approximate || m_full_dimensional) ? atom::ROOT_GE : atom::ROOT_GT, x, 1, p_lower); + add_root_literal((/*approximate ||*/ m_full_dimensional) ? atom::ROOT_GE : atom::ROOT_GT, x, 1, p_lower); // make sure bounding poly is at the back of the vector ps_below.push_back(p_lower); } @@ -1383,11 +1379,11 @@ namespace nlsat { rational new_bound; m_am.to_rational(between, new_bound); p_upper = m_pm.mk_polynomial(x); - p_upper = p_upper - new_bound; + p_upper = denominator(new_bound)*p_upper - numerator(new_bound); } - add_root_literal((approximate || m_full_dimensional) ? atom::ROOT_LE : atom::ROOT_LT, x, 1, p_upper); + add_root_literal((/*approximate ||*/ m_full_dimensional) ? atom::ROOT_LE : atom::ROOT_LT, x, 1, p_upper); // make sure bounding poly is at the back of the vector - ps_below.push_back(p_upper); + ps_above.push_back(p_upper); } } @@ -1424,7 +1420,7 @@ namespace nlsat { polynomial_ref_vector ps_above_sample(m_pm); polynomial_ref_vector ps_equal_sample(m_pm); var x = m_todo.extract_max_polys(ps); - if (x == max_x) { + if (!m_assignment.is_assigned(x)) { // top level projection like original // we could also do a covering-style projection, sparing some resultants add_lcs(ps, x); @@ -1433,7 +1429,7 @@ namespace nlsat { x = m_todo.extract_max_polys(ps); } - while (!m_todo.empty()) { + while (true) { add_cell_lits_linear(ps, x, ps_below_sample, ps_above_sample, ps_equal_sample); if (all_univ(ps, x) && m_todo.empty()) { m_todo.reset(); @@ -1463,6 +1459,8 @@ namespace nlsat { } } } + if (m_todo.empty()) + break; x = m_todo.extract_max_polys(ps); } } diff --git a/src/nlsat/nlsat_solver.cpp b/src/nlsat/nlsat_solver.cpp index 0961f4ee0..70a203f70 100644 --- a/src/nlsat/nlsat_solver.cpp +++ b/src/nlsat/nlsat_solver.cpp @@ -2034,7 +2034,7 @@ namespace nlsat { m_assignment.reset(); } - lbool check(assignment const& rvalues, atom_vector& core) { + lbool check(assignment const& rvalues, atom_vector& core, literal_vector& cell) { // temporarily set m_assignment to the given one assignment tmp = m_assignment; m_assignment.reset(); @@ -2042,7 +2042,6 @@ namespace nlsat { // check whether the asserted atoms are satisfied by rvalues literal best_literal = null_literal; - unsigned sz = m_clauses.size(); lbool satisfied = l_true; for (auto cp : m_clauses) { auto& c = *cp; @@ -2077,17 +2076,22 @@ namespace nlsat { // assignment does not satisfy the constraints -> create lemma SASSERT(best_literal != null_literal); + cell.reset(); m_lazy_clause.reset(); m_explain.set_linear_project(true); m_explain.main_operator(1, &best_literal, m_lazy_clause); m_explain.set_linear_project(false); - m_lazy_clause.push_back(~best_literal); - core.clear(); - for (literal l : m_lazy_clause) { - core.push_back(m_atoms[l.var()]); + for (auto l : m_lazy_clause) { + cell.push_back(l); } + m_lemma_assumptions = nullptr; + + core.clear(); + SASSERT(!best_literal.sign()); + core.push_back(m_atoms[best_literal.var()]); + m_assignment.reset(); m_assignment.copy(tmp); return l_false; @@ -4163,8 +4167,8 @@ namespace nlsat { return m_imp->check(assumptions); } - lbool solver::check(assignment const& rvalues, atom_vector& clause) { - return m_imp->check(rvalues, clause); + lbool solver::check(assignment const& rvalues, atom_vector& clause, literal_vector& cell) { + return m_imp->check(rvalues, clause, cell); } void solver::get_core(vector& assumptions) { diff --git a/src/nlsat/nlsat_solver.h b/src/nlsat/nlsat_solver.h index f9f46d494..00138ae9b 100644 --- a/src/nlsat/nlsat_solver.h +++ b/src/nlsat/nlsat_solver.h @@ -228,8 +228,9 @@ namespace nlsat { // clause is a list of atoms. Their negations conjoined with core literals are unsatisfiable. // Different implementations of check are possible. One where core comprises of linear polynomials could // produce lemmas that are friendly to linear arithmetic solvers. + // TODO: update // - lbool check(assignment const& rvalues, atom_vector& clause); + lbool check(assignment const& rvalues, atom_vector& clause, literal_vector& cell); // ----------------------- // From 4fec28710730fa709006923952f2a4b08e893c83 Mon Sep 17 00:00:00 2001 From: ValentinPromies <44966217+ValentinPromies@users.noreply.github.com> Date: Wed, 3 Sep 2025 18:52:51 +0200 Subject: [PATCH 14/42] clean up (#7844) --- src/math/lp/nra_solver.cpp | 31 +++++++++++-------------------- src/nlsat/nlsat_solver.cpp | 17 ++++++----------- src/nlsat/nlsat_solver.h | 11 +++++------ 3 files changed, 22 insertions(+), 37 deletions(-) diff --git a/src/math/lp/nra_solver.cpp b/src/math/lp/nra_solver.cpp index b4f0cbe70..3328547d6 100644 --- a/src/math/lp/nra_solver.cpp +++ b/src/math/lp/nra_solver.cpp @@ -255,8 +255,7 @@ struct solver::imp { setup_solver(); lbool r = l_undef; statistics& st = m_nla_core.lp_settings().stats().m_st; - nlsat::atom_vector clause; - nlsat::literal_vector cell; + nlsat::literal_vector clause; polynomial::manager& pm = m_nlsat->pm(); try { nlsat::assignment rvalues(m_nlsat->am()); @@ -265,7 +264,7 @@ struct solver::imp { am().set(a, m_nla_core.val(j).to_mpq()); rvalues.set(x, a); } - r = m_nlsat->check(rvalues, clause, cell); + r = m_nlsat->check(rvalues, clause); } catch (z3_exception&) { if (m_limit.is_canceled()) { @@ -289,16 +288,13 @@ struct solver::imp { validate_constraints(); break; case l_false: { - lp::explanation ex; - constraint_core2ex(ex); u_map nl2lp; for (auto [j, x] : m_lp2nl) nl2lp.insert(x, j); nla::lemma_builder lemma(m_nla_core, __FUNCTION__); - lemma &= ex; - - auto translate_atom = [&](nlsat::atom* a, bool negated){ + for (nlsat::literal l : clause) { + nlsat::atom* a = m_nlsat->bool_var2atom(l.var()); SASSERT(!a->is_root_atom()); SASSERT(a->is_ineq_atom()); auto& ia = *to_ineq_atom(a); @@ -351,23 +347,18 @@ struct solver::imp { } switch (a->get_kind()) { case nlsat::atom::EQ: - return nla::ineq(negated ? lp::lconstraint_kind::NE : lp::lconstraint_kind::EQ, t, bound); + lemma |= nla::ineq(l.sign() ? lp::lconstraint_kind::NE : lp::lconstraint_kind::EQ, t, bound); + break; case nlsat::atom::LT: - return nla::ineq(negated ? lp::lconstraint_kind::GE : lp::lconstraint_kind::LT, t, bound); + lemma |= nla::ineq(l.sign() ? lp::lconstraint_kind::GE : lp::lconstraint_kind::LT, t, bound); + break; case nlsat::atom::GT: - return nla::ineq(negated ? lp::lconstraint_kind::LE : lp::lconstraint_kind::GT, t, bound); + lemma |= nla::ineq(l.sign() ? lp::lconstraint_kind::LE : lp::lconstraint_kind::GT, t, bound); + break; default: UNREACHABLE(); + return l_undef; } - }; - - - for (auto a : clause) { - lemma |= translate_atom(a, true); - } - - for (nlsat::literal l : cell) { - lemma |= translate_atom( m_nlsat->bool_var2atom(l.var()), l.sign()); } IF_VERBOSE(1, verbose_stream() << "linear lemma: " << lemma << "\n"); diff --git a/src/nlsat/nlsat_solver.cpp b/src/nlsat/nlsat_solver.cpp index 70a203f70..aaa3c0857 100644 --- a/src/nlsat/nlsat_solver.cpp +++ b/src/nlsat/nlsat_solver.cpp @@ -2034,7 +2034,7 @@ namespace nlsat { m_assignment.reset(); } - lbool check(assignment const& rvalues, atom_vector& core, literal_vector& cell) { + lbool check(assignment const& rvalues, literal_vector& clause) { // temporarily set m_assignment to the given one assignment tmp = m_assignment; m_assignment.reset(); @@ -2076,21 +2076,16 @@ namespace nlsat { // assignment does not satisfy the constraints -> create lemma SASSERT(best_literal != null_literal); - cell.reset(); + clause.reset(); m_lazy_clause.reset(); m_explain.set_linear_project(true); m_explain.main_operator(1, &best_literal, m_lazy_clause); m_explain.set_linear_project(false); for (auto l : m_lazy_clause) { - cell.push_back(l); + clause.push_back(l); } - - m_lemma_assumptions = nullptr; - - core.clear(); - SASSERT(!best_literal.sign()); - core.push_back(m_atoms[best_literal.var()]); + clause.push_back(~best_literal); m_assignment.reset(); m_assignment.copy(tmp); @@ -4167,8 +4162,8 @@ namespace nlsat { return m_imp->check(assumptions); } - lbool solver::check(assignment const& rvalues, atom_vector& clause, literal_vector& cell) { - return m_imp->check(rvalues, clause, cell); + lbool solver::check(assignment const& rvalues, literal_vector& clause) { + return m_imp->check(rvalues, clause); } void solver::get_core(vector& assumptions) { diff --git a/src/nlsat/nlsat_solver.h b/src/nlsat/nlsat_solver.h index 00138ae9b..3d984c8cd 100644 --- a/src/nlsat/nlsat_solver.h +++ b/src/nlsat/nlsat_solver.h @@ -222,15 +222,14 @@ namespace nlsat { // 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 - the conjunction of literals from get_core, and negations of atoms in clause, - // such that the conjunction of the assumptions and the polynomials in core is unsatisfiable. + // 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 atoms. Their negations conjoined with core literals are unsatisfiable. - // Different implementations of check are possible. One where core comprises of linear polynomials could + // 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. - // TODO: update // - lbool check(assignment const& rvalues, atom_vector& clause, literal_vector& cell); + lbool check(assignment const& rvalues, literal_vector& clause); // ----------------------- // From cf53f2c866ed0dd184c77cc1a1ce15803d02a341 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 12 Sep 2025 13:56:13 -0700 Subject: [PATCH 15/42] Simplify no effect checks in nla_core.cpp Move up linear nlsat call to replace bounded nlsat. --- src/math/lp/nla_core.cpp | 18 +++++++++--------- 1 file changed, 9 insertions(+), 9 deletions(-) diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp index 6975c972a..13eb8a473 100644 --- a/src/math/lp/nla_core.cpp +++ b/src/math/lp/nla_core.cpp @@ -1532,8 +1532,13 @@ lbool core::check() { return l_false; } - - if (no_effect() && should_run_bounded_nlsat()) + if (no_effect()) { + scoped_limits sl(m_reslim); + sl.push_child(&m_nra_lim); + ret = m_nra.check_assignment(); + IF_VERBOSE(1, verbose_stream() << "nra check_assignment returned " << ret << "\n";); + } + else if (no_effect() && should_run_bounded_nlsat()) ret = bounded_nlsat(); if (no_effect()) @@ -1545,14 +1550,9 @@ lbool core::check() { if (no_effect()) m_divisions.check(); - bool use_nra_linearization = true; - if (no_effect() && use_nra_linearization) { - scoped_limits sl(m_reslim); - sl.push_child(&m_nra_lim); - ret = m_nra.check_assignment(); - IF_VERBOSE(1, verbose_stream() << "nra check_assignment returned " << ret << "\n";); - } + + if (no_effect()) { std::function check1 = [&]() { m_order.order_lemma(); From 444a9b1c4f6f92388dff7cacee374d890ac53bc5 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Fri, 19 Sep 2025 17:24:00 -0700 Subject: [PATCH 16/42] t Signed-off-by: Lev Nachmanson --- src/math/lp/nla_core.cpp | 5 +- src/math/lp/nra_solver.cpp | 158 +++++++++++++++++++++++-------------- 2 files changed, 101 insertions(+), 62 deletions(-) diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp index 13eb8a473..4d40e5b59 100644 --- a/src/math/lp/nla_core.cpp +++ b/src/math/lp/nla_core.cpp @@ -1055,6 +1055,7 @@ lemma_builder::lemma_builder(core& c, const char* name):name(name), c(c) { lemma_builder& lemma_builder::operator|=(ineq const& ineq) { if (!c.explain_ineq(*this, ineq.term(), ineq.cmp(), ineq.rs())) { CTRACE(nla_solver, c.ineq_holds(ineq), c.print_ineq(ineq, tout) << "\n";); + CTRACE(nra, c.ineq_holds(ineq), c.print_ineq(ineq, tout) << "\n";); SASSERT(c.m_use_nra_model || !c.ineq_holds(ineq)); current().push_back(ineq); } @@ -1550,10 +1551,6 @@ lbool core::check() { if (no_effect()) m_divisions.check(); - - - - if (no_effect()) { std::function check1 = [&]() { m_order.order_lemma(); }; diff --git a/src/math/lp/nra_solver.cpp b/src/math/lp/nra_solver.cpp index 3328547d6..e195e3058 100644 --- a/src/math/lp/nra_solver.cpp +++ b/src/math/lp/nra_solver.cpp @@ -16,6 +16,7 @@ #include "util/map.h" #include "util/uint_set.h" #include "math/lp/nla_core.h" +#include "math/lp/monic.h" #include "params/smt_params_helper.hpp" @@ -251,6 +252,73 @@ struct solver::imp { return r; } + void process_polynomial_check_assignment(unsigned num_mon, 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 < num_mon; ++i) { + polynomial::monomial* m = pm.get_monomial(p, i); + TRACE(nra, tout << "monomial: "; pm.display(tout, m); tout << "\n";); + auto& coeff = pm.coeff(p, i); + TRACE(nra, tout << "coeff:"; pm.m().display(tout, coeff);); + + unsigned num_vars = pm.size(m); + lp::lpvar v = lp::null_lpvar; + // add mon * coeff to t; + switch (num_vars) { + case 0: + bound -= coeff; + break; + case 1: { + unsigned mon_var = pm.get_var(m, 0); + auto v = nl2lp[mon_var]; + TRACE(nra, tout << "nl2lp[" << mon_var << "]:" << v << std::endl;); + rational s; + SASSERT(v != (unsigned)-1); + v = m_nla_core.reduce_var_to_rooted(v, s); + t.add_monomial(s * coeff, v); + } + break; + default: { + svector vars; + for (unsigned j = 0; j < num_vars; ++j) + vars.push_back(nl2lp[pm.get_var(m, j)]); + rational s; + vars = m_nla_core.reduce_monic_to_rooted(vars, s); + auto mon = m_nla_core.emons().find_canonical(vars); + TRACE(nra, tout << "canonical mon: "; if (mon) tout << *mon; else tout << "null"; tout << "\n";); + + if (mon) + v = mon->var(); + else { + NOT_IMPLEMENTED_YET(); + // this one is for Lev Nachmanson: lar_solver relies on internal variables + // to have terms from outside. The solver doesn't get to create + // its own monomials. + // v = ... + // It is not a use case if the nlsat solver only provides linear + // polynomials so punt for now. + m_nla_core.add_monic(v, vars.size(), vars.data()); + } + TRACE(nra, + tout << "process_polynomial_check_assignment:"; + tout << " vars="; + for (auto _w : vars) tout << _w << ' '; + tout << " s=" << s + << " mon=" << (mon ? static_cast(mon->var()) : -1) + << " v=" << v << "\n";); + t.add_monomial(s * 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_solver(); lbool r = l_undef; @@ -288,79 +356,53 @@ struct solver::imp { validate_constraints(); break; case l_false: { - u_map nl2lp; - for (auto [j, x] : m_lp2nl) - nl2lp.insert(x, j); - + u_map nl2lp = reverse_lp2nl(); nla::lemma_builder lemma(m_nla_core, __FUNCTION__); for (nlsat::literal l : clause) { nlsat::atom* a = m_nlsat->bool_var2atom(l.var()); + TRACE(nra, tout << "atom: "; m_nlsat->display(tout, *a); tout << "\n";); SASSERT(!a->is_root_atom()); SASSERT(a->is_ineq_atom()); auto& ia = *to_ineq_atom(a); VERIFY(ia.size() == 1); // deal with factored polynomials later // a is an inequality atom, i.e., p > 0, p < 0, or p = 0. polynomial::polynomial const* p = ia.p(0); + TRACE(nra, tout << "polynomial: "; pm.display(tout, p); tout << "\n";); unsigned num_mon = pm.size(p); rational bound(0); lp::lar_term t; - for (unsigned i = 0; i < num_mon; ++i) { - polynomial::monomial* m = pm.get_monomial(p, i); - auto& coeff = pm.coeff(p, i); - unsigned num_vars = pm.size(m); - lp::lpvar v = lp::null_lpvar; - // add mon * coeff to t; - switch (num_vars) { - case 0: - bound -= coeff; - break; - case 1: { - v = nl2lp[pm.get_var(m, 0)]; - rational s; - v = m_nla_core.reduce_var_to_rooted(v, s); - t.add_monomial(s * coeff, v); - } - break; - default: { - svector vars; - for (unsigned j = 0; j < num_vars; ++j) - vars.push_back(nl2lp[pm.get_var(m, j)]); - rational s(1); - vars = m_nla_core.reduce_monic_to_rooted(vars, s); - auto mon = m_nla_core.emons().find_canonical(vars); - if (mon) - v = mon->var(); - else { - NOT_IMPLEMENTED_YET(); - // this one is for Lev Nachmanson: lar_solver relies on internal variables - // to have terms from outside. The solver doesn't get to create - // its own monomials. - // v = ... - // It is not a use case if the nlsat solver only provides linear - // polynomials so punt for now. - m_nla_core.add_monic(v, vars.size(), vars.data()); - } - t.add_monomial(s * coeff, v); - break; - } - } - } + process_polynomial_check_assignment(num_mon, p, bound, nl2lp, t); + switch (a->get_kind()) { - case nlsat::atom::EQ: - lemma |= nla::ineq(l.sign() ? lp::lconstraint_kind::NE : lp::lconstraint_kind::EQ, t, bound); - break; - case nlsat::atom::LT: - lemma |= nla::ineq(l.sign() ? lp::lconstraint_kind::GE : lp::lconstraint_kind::LT, t, bound); - break; - case nlsat::atom::GT: - lemma |= nla::ineq(l.sign() ? lp::lconstraint_kind::LE : lp::lconstraint_kind::GT, t, bound); - break; - default: - UNREACHABLE(); - return l_undef; + case nlsat::atom::EQ: + { + nla::ineq inq(l.sign() ? lp::lconstraint_kind::NE : lp::lconstraint_kind::EQ, t, bound); + if (m_nla_core.ineq_holds(inq)) + return l_undef; + lemma |= inq; + } + break; + case nlsat::atom::LT: + { + nla::ineq inq(l.sign() ? lp::lconstraint_kind::GE : lp::lconstraint_kind::LT, t, bound); + if (m_nla_core.ineq_holds(inq)) + return l_undef; + lemma |= inq; + } + break; + case nlsat::atom::GT: + { + nla::ineq inq(l.sign() ? lp::lconstraint_kind::LE : lp::lconstraint_kind::GT, t, bound); + if (m_nla_core.ineq_holds(inq)) + return l_undef; + lemma |= inq; + } + break; + default: + UNREACHABLE(); + return l_undef; } } - IF_VERBOSE(1, verbose_stream() << "linear lemma: " << lemma << "\n"); m_nla_core.set_use_nra_model(true); break; From 3c38ee2690ad86e26ec82a5954eae0e0184f0eb1 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Fri, 19 Sep 2025 17:28:10 -0700 Subject: [PATCH 17/42] t Signed-off-by: Lev Nachmanson --- src/math/lp/nra_solver.cpp | 44 ++++++++++++++++++-------------------- 1 file changed, 21 insertions(+), 23 deletions(-) diff --git a/src/math/lp/nra_solver.cpp b/src/math/lp/nra_solver.cpp index e195e3058..d96968917 100644 --- a/src/math/lp/nra_solver.cpp +++ b/src/math/lp/nra_solver.cpp @@ -374,30 +374,28 @@ struct solver::imp { process_polynomial_check_assignment(num_mon, p, bound, nl2lp, t); switch (a->get_kind()) { - case nlsat::atom::EQ: - { - nla::ineq inq(l.sign() ? lp::lconstraint_kind::NE : lp::lconstraint_kind::EQ, t, bound); - if (m_nla_core.ineq_holds(inq)) - return l_undef; - lemma |= inq; + { + // Introduce a single ineq variable and assign it per case; common handling after switch. + 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(); + return l_undef; } - break; - case nlsat::atom::LT: - { - nla::ineq inq(l.sign() ? lp::lconstraint_kind::GE : lp::lconstraint_kind::LT, t, bound); - if (m_nla_core.ineq_holds(inq)) - return l_undef; - lemma |= inq; - } - break; - case nlsat::atom::GT: - { - nla::ineq inq(l.sign() ? lp::lconstraint_kind::LE : lp::lconstraint_kind::GT, t, bound); - if (m_nla_core.ineq_holds(inq)) - return l_undef; - lemma |= inq; - } - break; + if (m_nla_core.ineq_holds(inq)) + return l_undef; + lemma |= inq; + } + break; default: UNREACHABLE(); return l_undef; From 1582e4616e485c7ee41aee05a0b50bfcb0936876 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 23 Sep 2025 12:45:46 +0300 Subject: [PATCH 18/42] detangle mess Signed-off-by: Nikolaj Bjorner --- .clang-format | 84 ++++++++++++++++++++++++ src/math/lp/.clang-format | 5 -- src/math/lp/nra_solver.cpp | 127 ++++++++++++++++++------------------- 3 files changed, 145 insertions(+), 71 deletions(-) create mode 100644 .clang-format delete mode 100644 src/math/lp/.clang-format diff --git a/.clang-format b/.clang-format new file mode 100644 index 000000000..c4bbbf1e1 --- /dev/null +++ b/.clang-format @@ -0,0 +1,84 @@ + +# Z3 Theorem Prover clang-format configuration +# Based on analysis of existing codebase style patterns + +BasedOnStyle: LLVM + +# Indentation +IndentWidth: 4 +TabWidth: 4 +UseTab: Never + +# Column width +ColumnLimit: 120 + +# Braces +Cpp11BracedListStyle: true + +# Classes and structs +BreakConstructorInitializers: BeforeColon +ConstructorInitializerIndentWidth: 4 +AccessModifierOffset: -4 + +# Function definitions +AlwaysBreakAfterReturnType: None +AllowShortFunctionsOnASingleLine: Empty +AllowShortIfStatementsOnASingleLine: false +AllowShortLoopsOnASingleLine: false +# Ensure function-opening brace is attached to the signature +BreakBeforeBraces: Custom +# Explicitly ensure function brace is not placed on a new line +BraceWrapping: + AfterFunction: false + AfterClass: false + AfterControlStatement: false + AfterNamespace: false + AfterStruct: false +# Spacing +SpaceAfterCStyleCast: false +SpaceAfterLogicalNot: false +SpaceBeforeParens: ControlStatements +SpaceInEmptyParentheses: false +SpacesInCStyleCastParentheses: false +SpacesInParentheses: false +SpacesInSquareBrackets: false +IndentCaseLabels: false + +# Alignment +AlignConsecutiveAssignments: false +AlignConsecutiveDeclarations: false +AlignOperands: true +AlignTrailingComments: true + +# Line breaks +AllowAllParametersOfDeclarationOnNextLine: true +BinPackArguments: true +BinPackParameters: true +BreakBeforeBinaryOperators: None +BreakBeforeTernaryOperators: true + +# Includes +SortIncludes: false # Z3 has specific include ordering conventions + +# Namespaces +NamespaceIndentation: All + +# Comments and documentation +ReflowComments: true +SpacesBeforeTrailingComments: 2 + +# Language standards +Standard: c++20 + +# Penalties (for line breaking decisions) +PenaltyBreakAssignment: 2 +PenaltyBreakBeforeFirstCallParameter: 19 +PenaltyBreakComment: 300 +PenaltyBreakFirstLessLess: 120 +PenaltyBreakString: 1000 +PenaltyExcessCharacter: 1000000 +PenaltyReturnTypeOnItsOwnLine: 60 + +# Misc +KeepEmptyLinesAtTheStartOfBlocks: false +MaxEmptyLinesToKeep: 1 \ No newline at end of file diff --git a/src/math/lp/.clang-format b/src/math/lp/.clang-format deleted file mode 100644 index e9420012c..000000000 --- a/src/math/lp/.clang-format +++ /dev/null @@ -1,5 +0,0 @@ -BasedOnStyle: Google -IndentWidth: 4 -ColumnLimit: 0 -NamespaceIndentation: All -BreakBeforeBraces: Attach \ No newline at end of file diff --git a/src/math/lp/nra_solver.cpp b/src/math/lp/nra_solver.cpp index d96968917..5ba367837 100644 --- a/src/math/lp/nra_solver.cpp +++ b/src/math/lp/nra_solver.cpp @@ -320,21 +320,22 @@ struct solver::imp { } lbool check_assignment() { + IF_VERBOSE(1, verbose_stream() << "nra::solver::check_assignment\n";); setup_solver(); lbool r = l_undef; - statistics& st = m_nla_core.lp_settings().stats().m_st; + statistics &st = m_nla_core.lp_settings().stats().m_st; nlsat::literal_vector clause; - polynomial::manager& pm = m_nlsat->pm(); + polynomial::manager &pm = m_nlsat->pm(); 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); + rvalues.set(x, a); } r = m_nlsat->check(rvalues, clause); } - catch (z3_exception&) { + catch (z3_exception &) { if (m_limit.is_canceled()) { r = l_undef; } @@ -344,71 +345,65 @@ struct solver::imp { } } m_nlsat->collect_statistics(st); - TRACE(nra, - m_nlsat->display(tout << r << "\n"); - display(tout); - tout << "m_lp2nl:\n"; + TRACE(nra, m_nlsat->display(tout << r << "\n"); display(tout); tout << "m_lp2nl:\n"; for (auto [j, x] : m_lp2nl) tout << "j" << j << " := x" << x << "\n";); switch (r) { - case l_true: - m_nla_core.set_use_nra_model(true); - lra.init_model(); - validate_constraints(); - break; - case l_false: { - u_map nl2lp = reverse_lp2nl(); - nla::lemma_builder lemma(m_nla_core, __FUNCTION__); - for (nlsat::literal l : clause) { - nlsat::atom* a = m_nlsat->bool_var2atom(l.var()); - TRACE(nra, tout << "atom: "; m_nlsat->display(tout, *a); tout << "\n";); - SASSERT(!a->is_root_atom()); - SASSERT(a->is_ineq_atom()); - auto& ia = *to_ineq_atom(a); - VERIFY(ia.size() == 1); // deal with factored polynomials later - // a is an inequality atom, i.e., p > 0, p < 0, or p = 0. - polynomial::polynomial const* p = ia.p(0); - TRACE(nra, tout << "polynomial: "; pm.display(tout, p); tout << "\n";); - unsigned num_mon = pm.size(p); - rational bound(0); - lp::lar_term t; - process_polynomial_check_assignment(num_mon, p, bound, nl2lp, t); - - switch (a->get_kind()) { - { - // Introduce a single ineq variable and assign it per case; common handling after switch. - 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(); - return l_undef; - } - if (m_nla_core.ineq_holds(inq)) - return l_undef; - lemma |= inq; - } - break; - default: - UNREACHABLE(); - return l_undef; - } - } - IF_VERBOSE(1, verbose_stream() << "linear lemma: " << lemma << "\n"); - m_nla_core.set_use_nra_model(true); - break; - } - case l_undef: - break; + case l_true: + m_nla_core.set_use_nra_model(true); + lra.init_model(); + validate_constraints(); + m_nla_core.set_use_nra_model(true); + break; + case l_false: + return add_lemma(clause); + default: + break; + } + return r; + } + + lbool add_lemma(nlsat::literal_vector const &clause) { + u_map nl2lp = reverse_lp2nl(); + polynomial::manager &pm = m_nlsat->pm(); + nla::lemma_builder lemma(m_nla_core, __FUNCTION__); + for (nlsat::literal l : clause) { + nlsat::atom *a = m_nlsat->bool_var2atom(l.var()); + TRACE(nra, tout << "atom: "; m_nlsat->display(tout, *a); tout << "\n";); + SASSERT(!a->is_root_atom()); + SASSERT(a->is_ineq_atom()); + auto &ia = *to_ineq_atom(a); + VERIFY(ia.size() == 1); // deal with factored polynomials later + // a is an inequality atom, i.e., p > 0, p < 0, or p = 0. + polynomial::polynomial const *p = ia.p(0); + TRACE(nra, tout << "polynomial: "; pm.display(tout, p); tout << "\n";); + unsigned num_mon = pm.size(p); + rational bound(0); + lp::lar_term t; + process_polynomial_check_assignment(num_mon, p, bound, nl2lp, t); + + // Introduce a single ineq variable and assign it per case; common handling after switch. + 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(); + return l_undef; + } + // NSB review: what is this??? + if (m_nla_core.ineq_holds(inq)) + return l_undef; + lemma |= inq; + IF_VERBOSE(1, verbose_stream() << "linear lemma: " << lemma << "\n"); + return l_false; } - return r; } void constraint_core2ex(lp::explanation& ex) { From cc957011f2f10b134d005f38a41f6082b1642b52 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Mon, 29 Sep 2025 13:12:15 -0700 Subject: [PATCH 19/42] remove the too early return Signed-off-by: Lev Nachmanson --- src/math/lp/nra_solver.cpp | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) diff --git a/src/math/lp/nra_solver.cpp b/src/math/lp/nra_solver.cpp index 5ba367837..b368fdfec 100644 --- a/src/math/lp/nra_solver.cpp +++ b/src/math/lp/nra_solver.cpp @@ -355,7 +355,8 @@ struct solver::imp { m_nla_core.set_use_nra_model(true); break; case l_false: - return add_lemma(clause); + r = add_lemma(clause); + break; default: break; } @@ -397,13 +398,14 @@ struct solver::imp { UNREACHABLE(); return l_undef; } - // NSB review: what is this??? + // Ignore a lemma which is satisfied if (m_nla_core.ineq_holds(inq)) return l_undef; lemma |= inq; - IF_VERBOSE(1, verbose_stream() << "linear lemma: " << lemma << "\n"); - return l_false; } + IF_VERBOSE(1, verbose_stream() << "linear lemma: " << lemma << "\n"); + m_nla_core.set_use_nra_model(true); + return l_false; } void constraint_core2ex(lp::explanation& ex) { From 5de0b8a87fbae6a717ec909b3a39278c0e950e15 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Mon, 29 Sep 2025 13:20:46 -0700 Subject: [PATCH 20/42] do not set use_nra_model to true Signed-off-by: Lev Nachmanson --- src/math/lp/nra_solver.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/math/lp/nra_solver.cpp b/src/math/lp/nra_solver.cpp index b368fdfec..85a55cd6b 100644 --- a/src/math/lp/nra_solver.cpp +++ b/src/math/lp/nra_solver.cpp @@ -404,7 +404,7 @@ struct solver::imp { lemma |= inq; } IF_VERBOSE(1, verbose_stream() << "linear lemma: " << lemma << "\n"); - m_nla_core.set_use_nra_model(true); + //m_nla_core.set_use_nra_model(true); return l_false; } From d79d43355f7ee5d1111cf4b26636966f3e5afd08 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Mon, 29 Sep 2025 13:23:20 -0700 Subject: [PATCH 21/42] remove a comment Signed-off-by: Lev Nachmanson --- src/math/lp/nra_solver.cpp | 1 - 1 file changed, 1 deletion(-) diff --git a/src/math/lp/nra_solver.cpp b/src/math/lp/nra_solver.cpp index 85a55cd6b..dfa767d50 100644 --- a/src/math/lp/nra_solver.cpp +++ b/src/math/lp/nra_solver.cpp @@ -404,7 +404,6 @@ struct solver::imp { lemma |= inq; } IF_VERBOSE(1, verbose_stream() << "linear lemma: " << lemma << "\n"); - //m_nla_core.set_use_nra_model(true); return l_false; } From 1adfa948238cce81ead3ea123315060412eb1758 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Tue, 30 Sep 2025 16:47:49 -0700 Subject: [PATCH 22/42] add a hook to add new multiplication definitions in nla_core --- src/math/lp/nla_core.cpp | 5 ++++- src/math/lp/nla_core.h | 4 ++++ src/math/lp/nra_solver.cpp | 21 ++++++++------------- src/smt/theory_lra.cpp | 18 ++++++++++++++++++ 4 files changed, 34 insertions(+), 14 deletions(-) diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp index 4d40e5b59..e68f96e82 100644 --- a/src/math/lp/nla_core.cpp +++ b/src/math/lp/nla_core.cpp @@ -1577,7 +1577,10 @@ lbool core::check() { lp_settings().stats().m_nra_calls++; } - if (ret == l_undef && !no_effect() && m_reslim.inc()) + if (ret == l_undef) + return l_undef; + + if (!no_effect() && m_reslim.inc()) ret = l_false; lp_settings().stats().m_nla_lemmas += m_lemmas.size(); diff --git a/src/math/lp/nla_core.h b/src/math/lp/nla_core.h index 684b58d01..048461ddc 100644 --- a/src/math/lp/nla_core.h +++ b/src/math/lp/nla_core.h @@ -94,6 +94,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; @@ -208,6 +210,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); } diff --git a/src/math/lp/nra_solver.cpp b/src/math/lp/nra_solver.cpp index dfa767d50..a86bea20a 100644 --- a/src/math/lp/nra_solver.cpp +++ b/src/math/lp/nra_solver.cpp @@ -289,17 +289,9 @@ struct solver::imp { if (mon) v = mon->var(); else { - NOT_IMPLEMENTED_YET(); - // this one is for Lev Nachmanson: lar_solver relies on internal variables - // to have terms from outside. The solver doesn't get to create - // its own monomials. - // v = ... - // It is not a use case if the nlsat solver only provides linear - // polynomials so punt for now. - m_nla_core.add_monic(v, vars.size(), vars.data()); + v = m_nla_core.add_mul_def(vars.size(), vars.data()); } TRACE(nra, - tout << "process_polynomial_check_assignment:"; tout << " vars="; for (auto _w : vars) tout << _w << ' '; tout << " s=" << s @@ -323,9 +315,8 @@ struct solver::imp { IF_VERBOSE(1, verbose_stream() << "nra::solver::check_assignment\n";); setup_solver(); lbool r = l_undef; - statistics &st = m_nla_core.lp_settings().stats().m_st; - nlsat::literal_vector clause; - polynomial::manager &pm = m_nlsat->pm(); + 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) { @@ -373,7 +364,10 @@ struct solver::imp { SASSERT(!a->is_root_atom()); SASSERT(a->is_ineq_atom()); auto &ia = *to_ineq_atom(a); - VERIFY(ia.size() == 1); // deal with factored polynomials later + if (ia.size() != 1) { + return l_undef; // levnach: not sure what to do here + } + // VERIFY(ia.size() == 1); // deal with factored polynomials later // a is an inequality atom, i.e., p > 0, p < 0, or p = 0. polynomial::polynomial const *p = ia.p(0); TRACE(nra, tout << "polynomial: "; pm.display(tout, p); tout << "\n";); @@ -404,6 +398,7 @@ struct solver::imp { lemma |= inq; } IF_VERBOSE(1, verbose_stream() << "linear lemma: " << lemma << "\n"); + this->m_nla_core.m_check_feasible = true; return l_false; } diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index f3d9a5169..3dbdb1f97 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: @@ -269,10 +270,27 @@ class theory_lra::imp { return ctx().is_relevant(th.get_enode(u)); }; m_nla->set_relevant(is_relevant); + // install hook for creating multiplication definitions from nra_solver + 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) { // under 10 lines + 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"); From 3e47d1099d051e16834a33948750130b4c90bcfb Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 2 Oct 2025 08:36:39 -0700 Subject: [PATCH 23/42] add internalization routine that uses macro-expanded polynomial representation Signed-off-by: Nikolaj Bjorner --- src/math/lp/nra_solver.cpp | 85 +++++++++++++++++++++++++++++++++++++- 1 file changed, 83 insertions(+), 2 deletions(-) diff --git a/src/math/lp/nra_solver.cpp b/src/math/lp/nra_solver.cpp index a86bea20a..fa0261db7 100644 --- a/src/math/lp/nra_solver.cpp +++ b/src/math/lp/nra_solver.cpp @@ -154,6 +154,10 @@ struct solver::imp { TRACE(nra, m_nlsat->display(tout)); + log_nl(); + } + + void log_nl() { smt_params_helper p(m_params); if (p.arith_nl_log()) { static unsigned id = 0; @@ -172,6 +176,78 @@ struct solver::imp { } } + // + // This setup + svector m_literal2constraint; + void setup_assignment_solver() { + SASSERT(need_check()); + reset(); + m_literal2constraint.reset(); + + init_cone_of_influence(); + 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->set(j, a); + if (m_nla_core.emons().is_monic_var(v)) { + auto const &m = m_nla_core.emons()[v]; + polynomial::polynomial_ref p(pm); + for (auto v : m.vars()) { + auto pv = definitions.get(v); + if (!p) + p = pv; + else + p = pm.mul(p, pv); + } + definitions.push_back(p); + } + else if (lra.column_has_term(v)) { + polynomial::polynomial_ref p(pm); + for (auto const& [w, coeff] : lra.get_term(v)) { + auto pw = definitions.get(w); + if (!p) + p = pm.mul(coeff, pw); + else + p = pm.add(p, pm.mul(coeff, pw)); + } + definitions.push_back(p); + } + else + definitions.push_back(pm.mk_polynomial(j)); + } + + // we rely on that all information encoded into the tableau is present as a constraint. + for (auto ci : m_constraint_set) { + auto &c = lra.constraints()[ci]; + auto &pm = m_nlsat->pm(); + auto k = c.kind(); + auto rhs = c.rhs(); + auto lhs = c.coeffs(); + auto sz = lhs.size(); + + 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); + } + + log_nl(); + } + void validate_constraints() { for (lp::constraint_index ci : lra.constraints().indices()) if (!check_constraint(ci)) { @@ -452,8 +528,8 @@ struct solver::imp { } void add_constraint(unsigned idx) { - auto& c = lra.constraints()[idx]; - auto& pm = m_nlsat->pm(); + auto &c = lra.constraints()[idx]; + auto &pm = m_nlsat->pm(); auto k = c.kind(); auto rhs = c.rhs(); auto lhs = c.coeffs(); @@ -470,6 +546,10 @@ struct solver::imp { } rhs *= den; polynomial::polynomial_ref p(pm.mk_linear(sz, coeffs.data(), vars.data(), -rhs), pm); + add_constraint(p, idx, k); + } + + nlsat::literal add_constraint(polynomial::polynomial* p, unsigned idx, lp::lconstraint_kind k) { polynomial::polynomial* ps[1] = { p }; bool is_even[1] = { false }; nlsat::literal lit; @@ -494,6 +574,7 @@ struct solver::imp { UNREACHABLE(); // unreachable } m_nlsat->mk_clause(1, &lit, a); + return lit; } bool check_monic(mon_eq const& m) { From fe8f721600149be014305a27955cd4689d0c0df1 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 2 Oct 2025 08:37:14 -0700 Subject: [PATCH 24/42] add internalization routine that uses macro-expanded polynomial representation Signed-off-by: Nikolaj Bjorner --- src/math/lp/nra_solver.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/math/lp/nra_solver.cpp b/src/math/lp/nra_solver.cpp index fa0261db7..6c6bbd11c 100644 --- a/src/math/lp/nra_solver.cpp +++ b/src/math/lp/nra_solver.cpp @@ -177,7 +177,7 @@ struct solver::imp { } // - // This setup + // This setup is for check_assignment which is better suitated for working with input polynomials diretly. svector m_literal2constraint; void setup_assignment_solver() { SASSERT(need_check()); From ba378ed341530b6c98ed3e7b911e58bc072e583f Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 2 Oct 2025 08:55:27 -0700 Subject: [PATCH 25/42] fixup backtranslation to not use roots Signed-off-by: Nikolaj Bjorner --- src/math/lp/nra_solver.cpp | 67 ++++++++++++++++++++------------------ 1 file changed, 36 insertions(+), 31 deletions(-) diff --git a/src/math/lp/nra_solver.cpp b/src/math/lp/nra_solver.cpp index 6c6bbd11c..0de16d2d0 100644 --- a/src/math/lp/nra_solver.cpp +++ b/src/math/lp/nra_solver.cpp @@ -178,11 +178,22 @@ struct solver::imp { // // This setup is for check_assignment which is better suitated for working with input polynomials diretly. + // First slice the set of constraints to remove clusters that are satisfied by the current assignment. + // Then initialize each variable as either a polynomial variable or as a definition for a term or monomial. + // Finally process all constraints and use the definitions to represent these into the nlsat solver. + // svector m_literal2constraint; + struct eq { + bool operator()(unsigned_vector const &a, unsigned_vector const &b) const { + return a == b; + } + }; + map, eq> m_vars2mon; void setup_assignment_solver() { SASSERT(need_check()); reset(); m_literal2constraint.reset(); + m_vars2mon.reset(); init_cone_of_influence(); auto &pm = m_nlsat->pm(); @@ -190,14 +201,17 @@ struct solver::imp { 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); + m_lp2nl.insert(v, j); // we don't really need this. It is going to be the identify map. scoped_anum a(am()); am().set(a, m_nla_core.val(v).to_mpq()); m_values->set(j, a); 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); polynomial::polynomial_ref p(pm); - for (auto v : m.vars()) { + for (auto v : vars) { auto pv = definitions.get(v); if (!p) p = pv; @@ -328,9 +342,9 @@ struct solver::imp { return r; } - void process_polynomial_check_assignment(unsigned num_mon, 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 < num_mon; ++i) { + 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); TRACE(nra, tout << "monomial: "; pm.display(tout, m); tout << "\n";); auto& coeff = pm.coeff(p, i); @@ -344,36 +358,20 @@ struct solver::imp { bound -= coeff; break; case 1: { - unsigned mon_var = pm.get_var(m, 0); - auto v = nl2lp[mon_var]; - TRACE(nra, tout << "nl2lp[" << mon_var << "]:" << v << std::endl;); - rational s; - SASSERT(v != (unsigned)-1); - v = m_nla_core.reduce_var_to_rooted(v, s); - t.add_monomial(s * coeff, v); - } + auto v = nl2lp[pm.get_var(m, 0)]; + t.add_monomial(coeff, v); break; + } default: { + IF_VERBOSE(0, verbose_stream() << "Valentin! we don't really expect non-linear literals here\n"); svector vars; for (unsigned j = 0; j < num_vars; ++j) vars.push_back(nl2lp[pm.get_var(m, j)]); - rational s; - vars = m_nla_core.reduce_monic_to_rooted(vars, s); - auto mon = m_nla_core.emons().find_canonical(vars); - TRACE(nra, tout << "canonical mon: "; if (mon) tout << *mon; else tout << "null"; tout << "\n";); - - if (mon) - v = mon->var(); - else { - v = m_nla_core.add_mul_def(vars.size(), vars.data()); - } - TRACE(nra, - tout << " vars="; - for (auto _w : vars) tout << _w << ' '; - tout << " s=" << s - << " mon=" << (mon ? static_cast(mon->var()) : -1) - << " v=" << v << "\n";); - t.add_monomial(s * coeff, v); + std::sort(vars.begin(), vars.end()); + SASSERT(m_vars2mon.contains(vars)); + auto v = m_vars2mon[vars]; + TRACE(nra, tout << " vars=" << vars << "\n"); + t.add_monomial(coeff, v); break; } } @@ -435,6 +433,13 @@ struct solver::imp { polynomial::manager &pm = m_nlsat->pm(); 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()); TRACE(nra, tout << "atom: "; m_nlsat->display(tout, *a); tout << "\n";); SASSERT(!a->is_root_atom()); @@ -450,7 +455,7 @@ struct solver::imp { unsigned num_mon = pm.size(p); rational bound(0); lp::lar_term t; - process_polynomial_check_assignment(num_mon, p, bound, nl2lp, t); + process_polynomial_check_assignment(p, bound, nl2lp, t); // Introduce a single ineq variable and assign it per case; common handling after switch. nla::ineq inq(lp::lconstraint_kind::EQ, t, bound); // initial value overwritten in cases below From 874e8b3cfaca03a303a4c75cbb9430a849e18092 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 2 Oct 2025 08:58:15 -0700 Subject: [PATCH 26/42] call setup_assignment_solver instead of setup_solver Signed-off-by: Nikolaj Bjorner --- src/math/lp/nra_solver.cpp | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/math/lp/nra_solver.cpp b/src/math/lp/nra_solver.cpp index 0de16d2d0..0e7cae23a 100644 --- a/src/math/lp/nra_solver.cpp +++ b/src/math/lp/nra_solver.cpp @@ -387,10 +387,10 @@ struct solver::imp { lbool check_assignment() { IF_VERBOSE(1, verbose_stream() << "nra::solver::check_assignment\n";); - setup_solver(); + setup_assignment_solver(); lbool r = l_undef; - statistics &st = m_nla_core.lp_settings().stats().m_st; - nlsat::literal_vector clause; + 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) { From 84a9b38ec8065c5a16baf10b7856fb94cd98f472 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Thu, 2 Oct 2025 17:25:48 -0700 Subject: [PATCH 27/42] debug the setup, still not working Signed-off-by: Lev Nachmanson --- src/math/lp/nra_solver.cpp | 73 +++++++++++++++++++------------------- 1 file changed, 36 insertions(+), 37 deletions(-) diff --git a/src/math/lp/nra_solver.cpp b/src/math/lp/nra_solver.cpp index 0e7cae23a..63ebc133a 100644 --- a/src/math/lp/nra_solver.cpp +++ b/src/math/lp/nra_solver.cpp @@ -188,7 +188,40 @@ struct solver::imp { return a == b; } }; + + + map, eq> m_vars2mon; + // Create polynomial definition for variable v used in setup_assignment_solver. + // Side-effects: updates m_vars2mon when v is a monic variable. + polynomial::polynomial_ref mk_definition(unsigned v, polynomial_ref_vector const& 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)) { + for (auto const& [w, coeff] : lra.get_term(v)) { + auto pw = definitions.get(w); + if (!p) + p = pm.mul(coeff, pw); + else + p = pm.add(p, pm.mul(coeff, pw)); + } + } else { + p = pm.mk_polynomial(v); // nlsat var index equals v (verified above when created) + } + return p; + } void setup_assignment_solver() { SASSERT(need_check()); reset(); @@ -204,35 +237,8 @@ struct solver::imp { m_lp2nl.insert(v, j); // we don't really need this. It is going to be the identify map. scoped_anum a(am()); am().set(a, m_nla_core.val(v).to_mpq()); - m_values->set(j, a); - 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); - polynomial::polynomial_ref p(pm); - for (auto v : vars) { - auto pv = definitions.get(v); - if (!p) - p = pv; - else - p = pm.mul(p, pv); - } - definitions.push_back(p); - } - else if (lra.column_has_term(v)) { - polynomial::polynomial_ref p(pm); - for (auto const& [w, coeff] : lra.get_term(v)) { - auto pw = definitions.get(w); - if (!p) - p = pm.mul(coeff, pw); - else - p = pm.add(p, pm.mul(coeff, pw)); - } - definitions.push_back(p); - } - else - definitions.push_back(pm.mk_polynomial(j)); + m_values->push_back(a); + definitions.push_back(mk_definition(v, definitions)); } // we rely on that all information encoded into the tableau is present as a constraint. @@ -242,8 +248,6 @@ struct solver::imp { auto k = c.kind(); auto rhs = c.rhs(); auto lhs = c.coeffs(); - auto sz = lhs.size(); - rational den = denominator(rhs); for (auto [coeff, v] : lhs) den = lcm(den, denominator(coeff)); @@ -318,10 +322,7 @@ struct solver::imp { } } m_nlsat->collect_statistics(st); - TRACE(nra, - m_nlsat->display(tout << r << "\n"); - display(tout); - for (auto [j, x] : m_lp2nl) tout << "j" << j << " := x" << x << "\n";); + TRACE(nra, m_nlsat->display(tout << r << "\n");); switch (r) { case l_true: m_nla_core.set_use_nra_model(true); @@ -351,7 +352,6 @@ struct solver::imp { TRACE(nra, tout << "coeff:"; pm.m().display(tout, coeff);); unsigned num_vars = pm.size(m); - lp::lpvar v = lp::null_lpvar; // add mon * coeff to t; switch (num_vars) { case 0: @@ -452,7 +452,6 @@ struct solver::imp { // a is an inequality atom, i.e., p > 0, p < 0, or p = 0. polynomial::polynomial const *p = ia.p(0); TRACE(nra, tout << "polynomial: "; pm.display(tout, p); tout << "\n";); - unsigned num_mon = pm.size(p); rational bound(0); lp::lar_term t; process_polynomial_check_assignment(p, bound, nl2lp, t); From 85869b575b283f188aad32faacbc588d9290d2ac Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 2 Oct 2025 20:15:40 -0700 Subject: [PATCH 28/42] updated clang format Signed-off-by: Nikolaj Bjorner --- .clang-format | 10 +++++++++- 1 file changed, 9 insertions(+), 1 deletion(-) diff --git a/.clang-format b/.clang-format index c4bbbf1e1..1d7d35dc5 100644 --- a/.clang-format +++ b/.clang-format @@ -9,6 +9,7 @@ IndentWidth: 4 TabWidth: 4 UseTab: Never + # Column width ColumnLimit: 120 @@ -34,6 +35,8 @@ BraceWrapping: AfterControlStatement: false AfterNamespace: false AfterStruct: false + BeforeElse : true + AfterCaseLabel: false # Spacing SpaceAfterCStyleCast: false SpaceAfterLogicalNot: false @@ -42,7 +45,6 @@ SpaceInEmptyParentheses: false SpacesInCStyleCastParentheses: false SpacesInParentheses: false SpacesInSquareBrackets: false -IndentCaseLabels: false # Alignment AlignConsecutiveAssignments: false @@ -56,6 +58,7 @@ BinPackArguments: true BinPackParameters: true BreakBeforeBinaryOperators: None BreakBeforeTernaryOperators: true +# BreakBeforeElse: true # Includes SortIncludes: false # Z3 has specific include ordering conventions @@ -63,6 +66,11 @@ SortIncludes: false # Z3 has specific include ordering conventions # Namespaces NamespaceIndentation: All +# Switch statements +IndentCaseLabels: false +AllowShortCaseLabelsOnASingleLine: true +IndentCaseBlocks: false + # Comments and documentation ReflowComments: true SpacesBeforeTrailingComments: 2 From f8942dfdee59e766d4268c4e3cb70a1bd98abf3d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 2 Oct 2025 20:17:29 -0700 Subject: [PATCH 29/42] simplify Signed-off-by: Nikolaj Bjorner --- src/math/lp/nra_solver.cpp | 17 ++++++++++------- 1 file changed, 10 insertions(+), 7 deletions(-) diff --git a/src/math/lp/nra_solver.cpp b/src/math/lp/nra_solver.cpp index 63ebc133a..8f653f6c1 100644 --- a/src/math/lp/nra_solver.cpp +++ b/src/math/lp/nra_solver.cpp @@ -194,7 +194,7 @@ struct solver::imp { map, eq> m_vars2mon; // Create polynomial definition for variable v used in setup_assignment_solver. // Side-effects: updates m_vars2mon when v is a monic variable. - polynomial::polynomial_ref mk_definition(unsigned v, polynomial_ref_vector const& definitions) { + void mk_definition(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)) { @@ -209,19 +209,22 @@ struct solver::imp { else p = pm.mul(p, pv); } - } else if (lra.column_has_term(v)) { - for (auto const& [w, coeff] : lra.get_term(v)) { + } + else if (lra.column_has_term(v)) { + for (auto const &[w, coeff] : lra.get_term(v)) { auto pw = definitions.get(w); if (!p) p = pm.mul(coeff, pw); else p = pm.add(p, pm.mul(coeff, pw)); } - } else { - p = pm.mk_polynomial(v); // nlsat var index equals v (verified above when created) } - return p; + else { + p = pm.mk_polynomial(v); // nlsat var index equals v (verified above when created) + } + definitions.push_back(p); } + void setup_assignment_solver() { SASSERT(need_check()); reset(); @@ -238,7 +241,7 @@ struct solver::imp { scoped_anum a(am()); am().set(a, m_nla_core.val(v).to_mpq()); m_values->push_back(a); - definitions.push_back(mk_definition(v, definitions)); + mk_definition(v, definitions); } // we rely on that all information encoded into the tableau is present as a constraint. From 6cbc6f4f84d73e7fbe06d0969d72b16efbf019bc Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Mon, 6 Oct 2025 11:53:06 -0700 Subject: [PATCH 30/42] create polynomials with integer coefficients, use the hook to create new monomials Signed-off-by: Lev Nachmanson --- src/math/lp/nra_solver.cpp | 31 ++++++++++++++++++------------- src/smt/theory_lra.cpp | 2 +- 2 files changed, 19 insertions(+), 14 deletions(-) diff --git a/src/math/lp/nra_solver.cpp b/src/math/lp/nra_solver.cpp index 8f653f6c1..45ea7d3a8 100644 --- a/src/math/lp/nra_solver.cpp +++ b/src/math/lp/nra_solver.cpp @@ -194,7 +194,7 @@ struct solver::imp { map, eq> m_vars2mon; // 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(unsigned v, polynomial_ref_vector& definitions) { + void mk_definition(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)) { @@ -209,22 +209,25 @@ struct solver::imp { else p = pm.mul(p, pv); } - } - else if (lra.column_has_term(v)) { - for (auto const &[w, coeff] : lra.get_term(v)) { + } + else if (lra.column_has_term(v)) { + // Scale coefficients by a common denominator so that they become integers. + 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); if (!p) - p = pm.mul(coeff, pw); + p = pm.mul(den*coeff, pw); else - p = pm.add(p, pm.mul(coeff, pw)); + p = pm.add(p, pm.mul(den*coeff, pw)); } - } - else { - p = pm.mk_polynomial(v); // nlsat var index equals v (verified above when created) + } + else { + p = pm.mk_polynomial(v); // nlsat var index equals v (verified above when created) } definitions.push_back(p); } - void setup_assignment_solver() { SASSERT(need_check()); reset(); @@ -366,13 +369,15 @@ struct solver::imp { break; } default: { - IF_VERBOSE(0, verbose_stream() << "Valentin! we don't really expect non-linear literals here\n"); 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()); - SASSERT(m_vars2mon.contains(vars)); - auto v = m_vars2mon[vars]; + lp::lpvar v; + if (m_vars2mon.contains(vars)) + v = m_vars2mon[vars]; + else + v = m_nla_core.add_mul_def(vars.size(), vars.data()); TRACE(nra, tout << " vars=" << vars << "\n"); t.add_monomial(coeff, v); break; diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index 3dbdb1f97..327ca0c75 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -276,7 +276,7 @@ class theory_lra::imp { } } - lpvar add_mul_def(unsigned sz, lpvar const* vs) { // under 10 lines + 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]); From ddba2cc38176d264861be58bf45b32aef68b9c59 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Mon, 24 Nov 2025 13:00:43 -1000 Subject: [PATCH 31/42] integrating changes from master related to work with polynomials Signed-off-by: Lev Nachmanson --- src/math/lp/CMakeLists.txt | 2 + src/math/lp/nla_core.cpp | 320 ++++----------------- src/math/lp/nla_core.h | 27 +- src/math/lp/nla_grobner.cpp | 4 + src/math/lp/nla_grobner.h | 2 + src/math/lp/nla_solver.cpp | 6 +- src/math/lp/nla_solver.h | 1 + src/math/lp/nra_solver.cpp | 554 +++++++++++++++++++----------------- src/math/lp/nra_solver.h | 4 +- 9 files changed, 390 insertions(+), 530 deletions(-) diff --git a/src/math/lp/CMakeLists.txt b/src/math/lp/CMakeLists.txt index 96f51731f..729b47782 100644 --- a/src/math/lp/CMakeLists.txt +++ b/src/math/lp/CMakeLists.txt @@ -24,6 +24,7 @@ z3_add_component(lp monomial_bounds.cpp nex_creator.cpp nla_basics_lemmas.cpp + nla_coi.cpp nla_common.cpp nla_core.cpp nla_divisions.cpp @@ -32,6 +33,7 @@ z3_add_component(lp nla_monotone_lemmas.cpp nla_order_lemmas.cpp nla_powers.cpp + nla_pp.cpp nla_solver.cpp nla_tangent_lemmas.cpp nla_throttle.cpp diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp index e68f96e82..8078b2645 100644 --- a/src/math/lp/nla_core.cpp +++ b/src/math/lp/nla_core.cpp @@ -1,4 +1,4 @@ -/*++ + /*++ Copyright (c) 2017 Microsoft Corporation Module Name: @@ -17,6 +17,7 @@ Author: #include "math/grobner/pdd_solver.h" #include "math/dd/pdd_interval.h" #include "math/dd/pdd_eval.h" + using namespace nla; typedef lp::lar_term term; @@ -38,7 +39,7 @@ core::core(lp::lar_solver& s, params_ref const& p, reslimit & lim) : m_grobner(this), m_emons(m_evars), m_use_nra_model(false), - m_nra(s, m_nra_lim, *this), + m_nra(s, m_nra_lim, *this, p), m_throttle(lra.trail(), lra.settings().stats()) { m_nlsat_delay_bound = lp_settings().nlsat_delay(); @@ -51,6 +52,10 @@ core::core(lp::lar_solver& s, params_ref const& p, reslimit & lim) : } }; } + +void core::updt_params(params_ref const& p) { + // grobner updt_params is a no-op on this branch +} bool core::compare_holds(const rational& ls, llc cmp, const rational& rs) const { switch(cmp) { @@ -88,13 +93,6 @@ lpvar core::map_to_root(lpvar j) const { return m_evars.find(j).var(); } -// Reduce a single variable to its root and provide the reduction sign. -lpvar core::reduce_var_to_rooted(lpvar j, rational & sign) const { - auto root = m_evars.find(j); - sign = rational(root.sign() ? -1 : 1); - return root.var(); -} - svector core::sorted_rvars(const factor& f) const { if (f.is_var()) { svector r; r.push_back(map_to_root(f.var())); @@ -179,108 +177,6 @@ bool core::check_monic(const monic& m) const { } -template -std::ostream& core::print_product(const T & m, std::ostream& out) const { - bool first = true; - for (lpvar v : m) { - if (!first) out << "*"; else first = false; - if (lp_settings().print_external_var_name()) - out << "(" << lra.get_variable_name(v) << "=" << val(v) << ")"; - else - out << "(j" << v << " = " << val(v) << ")"; - - } - return out; -} -template -std::string core::product_indices_str(const T & m) const { - std::stringstream out; - bool first = true; - for (lpvar v : m) { - if (!first) - out << "*"; - else - first = false; - out << "j" << v;; - } - return out.str(); -} - -std::ostream & core::print_factor(const factor& f, std::ostream& out) const { - if (f.sign()) - out << "- "; - if (f.is_var()) { - out << "VAR, " << pp(f.var()); - } else { - out << "MON, v" << m_emons[f.var()] << " = "; - print_product(m_emons[f.var()].rvars(), out); - } - out << "\n"; - return out; -} - -std::ostream & core::print_factor_with_vars(const factor& f, std::ostream& out) const { - if (f.is_var()) { - out << pp(f.var()); - } - else { - out << " MON = " << pp_mon_with_vars(*this, m_emons[f.var()]); - } - return out; -} - -std::ostream& core::print_monic(const monic& m, std::ostream& out) const { - if (lp_settings().print_external_var_name()) - out << "([" << m.var() << "] = " << lra.get_variable_name(m.var()) << " = " << val(m.var()) << " = "; - else - out << "(j" << m.var() << " = " << val(m.var()) << " = "; - print_product(m.vars(), out) << ")\n"; - return out; -} - - -std::ostream& core::print_bfc(const factorization& m, std::ostream& out) const { - SASSERT(m.size() == 2); - out << "( x = " << pp(m[0]) << "* y = " << pp(m[1]) << ")"; - return out; -} - -std::ostream& core::print_monic_with_vars(lpvar v, std::ostream& out) const { - return print_monic_with_vars(m_emons[v], out); -} -template -std::ostream& core::print_product_with_vars(const T& m, std::ostream& out) const { - print_product(m, out) << "\n"; - for (unsigned k = 0; k < m.size(); k++) { - print_var(m[k], out); - } - return out; -} - -std::ostream& core::print_monic_with_vars(const monic& m, std::ostream& out) const { - out << "[" << pp(m.var()) << "]\n"; - out << "vars:"; print_product_with_vars(m.vars(), out) << "\n"; - if (m.vars() == m.rvars()) - out << "same rvars, and m.rsign = " << m.rsign() << " of course\n"; - else { - out << "rvars:"; print_product_with_vars(m.rvars(), out) << "\n"; - out << "rsign:" << m.rsign() << "\n"; - } - return out; -} - -std::ostream& core::print_explanation(const lp::explanation& exp, std::ostream& out) const { - out << "expl: "; - unsigned i = 0; - for (auto p : exp) { - out << "(" << p.ci() << ")"; - lra.constraints().display(out, [this](lpvar j) { return var_str(j);}, p.ci()); - if (++i < exp.size()) - out << " "; - } - return out; -} - bool core::explain_upper_bound(const lp::lar_term& t, const rational& rs, lp::explanation& e) const { rational b(0); // the bound for (lp::lar_term::ival p : t) { @@ -558,69 +454,6 @@ bool core::var_is_free(lpvar j) const { return lra.column_is_free(j); } -std::ostream & core::print_ineq(const ineq & in, std::ostream & out) const { - lra.print_term_as_indices(in.term(), out); - return out << " " << lconstraint_kind_string(in.cmp()) << " " << in.rs(); -} - -std::ostream & core::print_var(lpvar j, std::ostream & out) const { - if (is_monic_var(j)) - print_monic(m_emons[j], out); - - lra.print_column_info(j, out); - signed_var jr = m_evars.find(j); - out << "root="; - if (jr.sign()) { - out << "-"; - } - - out << lra.get_variable_name(jr.var()) << "\n"; - return out; -} - -std::ostream & core::print_monics(std::ostream & out) const { - for (auto &m : m_emons) { - print_monic_with_vars(m, out); - } - return out; -} - -std::ostream & core::print_ineqs(const lemma& l, std::ostream & out) const { - std::unordered_set vars; - out << "ineqs: "; - if (l.ineqs().size() == 0) { - out << "conflict\n"; - } else { - for (unsigned i = 0; i < l.ineqs().size(); i++) { - auto & in = l.ineqs()[i]; - print_ineq(in, out); - if (i + 1 < l.ineqs().size()) out << " or "; - for (lp::lar_term::ival p: in.term()) - vars.insert(p.j()); - } - out << std::endl; - for (lpvar j : vars) { - print_var(j, out); - } - out << "\n"; - } - return out; -} - -std::ostream & core::print_factorization(const factorization& f, std::ostream& out) const { - if (f.is_mon()){ - out << "is_mon " << pp_mon(*this, f.mon()); - } - else { - for (unsigned k = 0; k < f.size(); k++ ) { - out << "(" << pp(f[k]) << ")"; - if (k < f.size() - 1) - out << "*"; - } - } - return out; -} - bool core::find_canonical_monic_of_vars(const svector& vars, lpvar & i) const { monic const* sv = m_emons.find_canonical(vars); return sv && (i = sv->var(), true); @@ -630,16 +463,6 @@ bool core::is_canonical_monic(lpvar j) const { return m_emons.is_canonical_monic(j); } - -void core::trace_print_monic_and_factorization(const monic& rm, const factorization& f, std::ostream& out) const { - out << "rooted vars: "; - print_product(rm.rvars(), out) << "\n"; - out << "mon: " << pp_mon(*this, rm.var()) << "\n"; - out << "value: " << var_val(rm) << "\n"; - print_factorization(f, out << "fact: ") << "\n"; -} - - bool core::var_has_positive_lower_bound(lpvar j) const { return lra.column_has_lower_bound(j) && lra.get_lower_bound(j) > lp::zero_of_type(); } @@ -778,35 +601,6 @@ bool core::vars_are_roots(const T& v) const { } - -template -void core::trace_print_rms(const T& p, std::ostream& out) { - out << "p = {\n"; - for (auto j : p) { - out << "j = " << j << ", rm = " << m_emons[j] << "\n"; - } - out << "}"; -} - -void core::print_monic_stats(const monic& m, std::ostream& out) { - if (m.size() == 2) return; - monic_coeff mc = canonize_monic(m); - for(unsigned i = 0; i < mc.vars().size(); i++){ - if (abs(val(mc.vars()[i])) == rational(1)) { - auto vv = mc.vars(); - vv.erase(vv.begin()+i); - monic const* sv = m_emons.find_canonical(vv); - if (!sv) { - out << "nf length" << vv.size() << "\n"; ; - } - } - } -} - -void core::print_stats(std::ostream& out) { -} - - void core::clear() { m_lemmas.clear(); m_literals.clear(); @@ -1055,7 +849,6 @@ lemma_builder::lemma_builder(core& c, const char* name):name(name), c(c) { lemma_builder& lemma_builder::operator|=(ineq const& ineq) { if (!c.explain_ineq(*this, ineq.term(), ineq.cmp(), ineq.rs())) { CTRACE(nla_solver, c.ineq_holds(ineq), c.print_ineq(ineq, tout) << "\n";); - CTRACE(nra, c.ineq_holds(ineq), c.print_ineq(ineq, tout) << "\n";); SASSERT(c.m_use_nra_model || !c.ineq_holds(ineq)); current().push_back(ineq); } @@ -1515,6 +1308,10 @@ lbool core::check() { if (no_effect()) m_monomial_bounds.propagate(); + + if (no_effect() && refine_pseudo_linear()) + return l_false; + { std::function check1 = [&]() { if (no_effect() && run_horner) m_horner.horner_lemmas(); }; @@ -1537,9 +1334,9 @@ lbool core::check() { scoped_limits sl(m_reslim); sl.push_child(&m_nra_lim); ret = m_nra.check_assignment(); - IF_VERBOSE(1, verbose_stream() << "nra check_assignment returned " << ret << "\n";); - } - else if (no_effect() && should_run_bounded_nlsat()) + } + + if (no_effect() && should_run_bounded_nlsat()) ret = bounded_nlsat(); if (no_effect()) @@ -1551,6 +1348,7 @@ lbool core::check() { if (no_effect()) m_divisions.check(); + if (no_effect()) { std::function check1 = [&]() { m_order.order_lemma(); }; @@ -1577,10 +1375,7 @@ lbool core::check() { lp_settings().stats().m_nra_calls++; } - if (ret == l_undef) - return l_undef; - - if (!no_effect() && m_reslim.inc()) + if (ret == l_undef && !no_effect() && m_reslim.inc()) ret = l_false; lp_settings().stats().m_nla_lemmas += m_lemmas.size(); @@ -1588,6 +1383,8 @@ lbool core::check() { TRACE(nla_solver, tout << "ret = " << ret << ", lemmas count = " << m_lemmas.size() << "\n";); IF_VERBOSE(5, if(ret == l_undef) {verbose_stream() << "Monomials\n"; print_monics(verbose_stream());}); CTRACE(nla_solver, ret == l_undef, tout << "Monomials\n"; print_monics(tout);); + CTRACE(nla_solver, ret == l_undef, display_smt(tout);); + // if (ret == l_undef) IF_VERBOSE(0, display_smt(verbose_stream())); return ret; } @@ -1600,18 +1397,13 @@ bool core::should_run_bounded_nlsat() { } lbool core::bounded_nlsat() { - params_ref p; lbool ret; - p.set_uint("max_conflicts", 100); - m_nra.updt_params(p); { scoped_limits sl(m_reslim); sl.push_child(&m_nra_lim); scoped_rlimit sr(m_nra_lim, 100000); ret = m_nra.check(); } - p.set_uint("max_conflicts", UINT_MAX); - m_nra.updt_params(p); lp_settings().stats().m_nra_calls++; if (ret == l_undef) ++m_nlsat_delay_bound; @@ -1635,40 +1427,11 @@ bool core::no_lemmas_hold() const { return true; } - lbool core::test_check() { lra.set_status(lp::lp_status::OPTIMAL); return check(); } -std::ostream& core::print_terms(std::ostream& out) const { - for (const auto * t: lra.terms()) { - out << "term:"; print_term(*t, out) << std::endl; - print_var(t->j(), out); - } - return out; -} - -std::string core::var_str(lpvar j) const { - std::string result; - if (is_monic_var(j)) - result += product_indices_str(m_emons[j].vars()) + (check_monic(m_emons[j])? "": "_"); - else - result += std::string("j") + lp::T_to_string(j); - // result += ":w" + lp::T_to_string(get_var_weight(j)); - return result; -} - -std::ostream& core::print_term( const lp::lar_term& t, std::ostream& out) const { - return lp::print_linear_combination_customized( - t.coeffs_as_vector(), - [this](lpvar j) { return var_str(j); }, - out); -} - - - - std::unordered_set core::get_vars_of_expr_with_opening_terms(const nex *e ) { auto ret = get_vars_of_expr(e); auto & ls = lra; @@ -1691,12 +1454,10 @@ std::unordered_set core::get_vars_of_expr_with_opening_terms(const nex *e return ret; } - bool core::is_nl_var(lpvar j) const { return is_monic_var(j) || m_emons.is_used_in_monic(j); } - unsigned core::get_var_weight(lpvar j) const { unsigned k = 0; switch (lra.get_column_type(j)) { @@ -1765,6 +1526,49 @@ void core::simplify() { } +bool core::is_pseudo_linear(monic const& m) const { + bool has_unbounded = false; + for (auto v : m.vars()) { + if (lra.column_is_bounded(v) && lra.var_is_int(v)) { + auto lb = lra.get_lower_bound(v); + auto ub = lra.get_upper_bound(v); + if (ub - lb <= rational(4)) + continue; + } + if (has_unbounded) + return false; + has_unbounded = true; + } + return true; +} +bool core::refine_pseudo_linear() { + // Parameter support for this optimization is unavailable in this branch. + return false; +} - +void core::refine_pseudo_linear(monic const& m) { + lemma_builder lemma(*this, "nla-pseudo-linear"); + lpvar nlvar = null_lpvar; + rational prod(1); + for (unsigned i = 0; i < m.vars().size(); ++i) { + auto v = m.vars()[i]; + if (i == m.vars().size() - 1 && nlvar == null_lpvar) { + nlvar = v; + break; + } + if (lra.column_is_bounded(v) && lra.var_is_int(v)) { + auto lb = lra.get_lower_bound(v); + auto ub = lra.get_upper_bound(v); + if (ub - lb <= rational(4)) { + lemma |= ineq(v, llc::NE, val(v)); + prod *= val(v); + continue; + } + } + SASSERT(nlvar == null_lpvar); + nlvar = v; + } + SASSERT(nlvar != null_lpvar); + lemma |= ineq(lp::lar_term(m.var(), rational(-prod), nlvar), llc::EQ, rational(0)); +} diff --git a/src/math/lp/nla_core.h b/src/math/lp/nla_core.h index 048461ddc..95be7ae46 100644 --- a/src/math/lp/nla_core.h +++ b/src/math/lp/nla_core.h @@ -113,7 +113,12 @@ class core { void check_weighted(unsigned sz, std::pair>* checks); void add_bounds(); + bool refine_pseudo_linear(); + bool is_pseudo_linear(monic const& m) const; + void refine_pseudo_linear(monic const& m); + std::ostream& display_constraint_smt(std::ostream& out, unsigned id, lp::lar_base_constraint const& c) const; + std::ostream& display_declarations_smt(std::ostream& out) const; public: // constructor @@ -121,6 +126,8 @@ public: const auto& monics_with_changed_bounds() const { return m_monics_with_changed_bounds; } void insert_to_refine(lpvar j); void erase_from_to_refine(lpvar j); + + void updt_params(params_ref const& p); const indexed_uint_set& active_var_set () const { return m_active_var_set;} bool active_var_set_contains(unsigned j) const { return m_active_var_set.contains(j); } @@ -228,6 +235,9 @@ public: bool check_monic(const monic& m) const; + std::ostream & display_row(std::ostream& out, lp::row_strip const& row) const; + std::ostream & display(std::ostream& out); + std::ostream& display_smt(std::ostream& out); std::ostream & print_ineq(const ineq & in, std::ostream & out) const; std::ostream & print_var(lpvar j, std::ostream & out) const; std::ostream & print_monics(std::ostream & out) const; @@ -285,12 +295,8 @@ public: svector reduce_monic_to_rooted(const svector & vars, rational & sign) const; - // Reduce a single variable to its canonical root under current equalities - // and return the convertion sign as either 1 or -1 - lpvar reduce_var_to_rooted(lpvar v, rational & sign) const; - monic_coeff canonize_monic(monic const& m) const; - + int vars_sign(const svector& v); bool has_upper_bound(lpvar j) const; bool has_lower_bound(lpvar j) const; @@ -365,6 +371,10 @@ public: template bool vars_are_roots(const T& v) const; + void register_monic_in_tables(unsigned i_mon); + + void register_monics_in_tables(); + void clear(); void init_search(); @@ -444,6 +454,12 @@ public: nla_throttle& throttle() { return m_throttle; } const nla_throttle& throttle() const { return m_throttle; } + lp::lar_solver& lra_solver() { return lra; } + + indexed_uint_set const& to_refine() const { + return m_to_refine; + } + }; // end of core struct pp_mon { @@ -466,4 +482,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.cpp b/src/math/lp/nla_grobner.cpp index 09660a2a6..5c647f0fc 100644 --- a/src/math/lp/nla_grobner.cpp +++ b/src/math/lp/nla_grobner.cpp @@ -98,6 +98,10 @@ namespace nla { return m_solver.equations(); } + void grobner::updt_params(params_ref const&) { + // placeholder: nl2lin branch does not expose grobner-specific params from master + } + bool grobner::is_conflicting() { for (auto eq : m_solver.equations()) { if (is_conflicting(*eq)) { diff --git a/src/math/lp/nla_grobner.h b/src/math/lp/nla_grobner.h index ee41e4dae..5cf7ddf70 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" @@ -73,6 +74,7 @@ namespace nla { public: grobner(core *core); void operator()(); + void updt_params(params_ref const& p); dd::solver::equation_vector const& core_equations(bool all_eqs); }; } diff --git a/src/math/lp/nla_solver.cpp b/src/math/lp/nla_solver.cpp index 793789f8f..dcf2266c1 100644 --- a/src/math/lp/nla_solver.cpp +++ b/src/math/lp/nla_solver.cpp @@ -35,6 +35,10 @@ namespace nla { void solver::set_relevant(std::function& is_relevant) { m_core->set_relevant(is_relevant); } + + void solver::updt_params(params_ref const& p) { + m_core->updt_params(p); + } bool solver::is_monic_var(lpvar v) const { return m_core->is_monic_var(v); @@ -71,7 +75,7 @@ namespace nla { } std::ostream& solver::display(std::ostream& out) const { - m_core->print_monics(out); + m_core->display(out); if (use_nra_model()) m_core->m_nra.display(out); return out; diff --git a/src/math/lp/nla_solver.h b/src/math/lp/nla_solver.h index 57016927b..133117149 100644 --- a/src/math/lp/nla_solver.h +++ b/src/math/lp/nla_solver.h @@ -33,6 +33,7 @@ namespace nla { void add_bounded_division(lpvar q, lpvar x, lpvar y); void check_bounded_divisions(); void set_relevant(std::function& is_relevant); + void updt_params(params_ref const& p); void push(); void pop(unsigned scopes); bool need_check(); diff --git a/src/math/lp/nra_solver.cpp b/src/math/lp/nra_solver.cpp index 45ea7d3a8..4d91c12f4 100644 --- a/src/math/lp/nra_solver.cpp +++ b/src/math/lp/nra_solver.cpp @@ -9,6 +9,7 @@ #include #include "math/lp/lar_solver.h" #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" @@ -16,7 +17,6 @@ #include "util/map.h" #include "util/uint_set.h" #include "math/lp/nla_core.h" -#include "math/lp/monic.h" #include "params/smt_params_helper.hpp" @@ -27,174 +27,82 @@ typedef nla::mon_eq mon_eq; typedef nla::variable_map_type variable_map_type; struct solver::imp { + lp::lar_solver& lra; reslimit& m_limit; params_ref m_params; u_map m_lp2nl; // map from lar_solver variables to nlsat::solver variables - indexed_uint_set m_term_set; scoped_ptr m_nlsat; 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): lra(s), m_limit(lim), m_params(p), + m_coi(nla_core), m_nla_core(nla_core) {} bool need_check() { return m_nla_core.m_to_refine.size() != 0; } - indexed_uint_set m_mon_set, m_constraint_set; - - struct occurs { - unsigned_vector constraints; - unsigned_vector monics; - unsigned_vector terms; - }; - - void init_cone_of_influence() { - indexed_uint_set visited; - unsigned_vector todo; - vector var2occurs; - m_term_set.reset(); - m_mon_set.reset(); - m_constraint_set.reset(); - - for (auto ci : lra.constraints().indices()) { - auto const& c = lra.constraints()[ci]; - if (c.is_auxiliary()) - continue; - for (auto const& [coeff, v] : c.coeffs()) { - var2occurs.reserve(v + 1); - var2occurs[v].constraints.push_back(ci); - } - } - - for (auto const& m : m_nla_core.emons()) { - for (auto v : m.vars()) { - var2occurs.reserve(v + 1); - var2occurs[v].monics.push_back(m.var()); - } - } - - for (const auto *t : lra.terms() ) { - for (auto const iv : *t) { - auto v = iv.j(); - var2occurs.reserve(v + 1); - var2occurs[v].terms.push_back(t->j()); - } - } - - for (auto const& m : m_nla_core.m_to_refine) - todo.push_back(m); - - for (unsigned i = 0; i < todo.size(); ++i) { - auto v = todo[i]; - if (visited.contains(v)) - continue; - visited.insert(v); - var2occurs.reserve(v + 1); - for (auto ci : var2occurs[v].constraints) { - m_constraint_set.insert(ci); - auto const& c = lra.constraints()[ci]; - for (auto const& [coeff, w] : c.coeffs()) - todo.push_back(w); - } - for (auto w : var2occurs[v].monics) - todo.push_back(w); - - for (auto ti : var2occurs[v].terms) { - for (auto iv : lra.get_term(ti)) - todo.push_back(iv.j()); - todo.push_back(ti); - } - - if (lra.column_has_term(v)) { - m_term_set.insert(v); - for (auto kv : lra.get_term(v)) - todo.push_back(kv.j()); - } - - if (m_nla_core.is_monic_var(v)) { - m_mon_set.insert(v); - for (auto w : m_nla_core.emons()[v]) - todo.push_back(w); - } - } - } - void reset() { m_values = nullptr; m_tmp1 = nullptr; m_tmp2 = nullptr; m_nlsat = alloc(nlsat::solver, m_limit, m_params, false); m_values = alloc(scoped_anum_vector, am()); - m_term_set.reset(); m_lp2nl.reset(); } - void setup_solver() { - SASSERT(need_check()); - reset(); - - init_cone_of_influence(); - // add linear inequalities from lra_solver - for (auto ci : m_constraint_set) - add_constraint(ci); - - // add polynomial definitions. - for (auto const& m : m_mon_set) - add_monic_eq(m_nla_core.emons()[m]); - - // add term definitions. - for (unsigned i : m_term_set) - add_term(i); - - TRACE(nra, m_nlsat->display(tout)); - - log_nl(); - } - - void log_nl() { - smt_params_helper p(m_params); - if (p.arith_nl_log()) { - static unsigned id = 0; - std::stringstream strm; - -#ifndef SINGLE_THREAD - std::thread::id this_id = std::this_thread::get_id(); - strm << "nla_" << this_id << "." << (++id) << ".smt2"; -#else - strm << "nla_" << (++id) << ".smt2"; -#endif - std::ofstream out(strm.str()); - m_nlsat->display_smt2(out); - out << "(check-sat)\n"; - out.close(); - } - } - - // - // This setup is for check_assignment which is better suitated for working with input polynomials diretly. - // First slice the set of constraints to remove clusters that are satisfied by the current assignment. - // Then initialize each variable as either a polynomial variable or as a definition for a term or monomial. - // Finally process all constraints and use the definitions to represent these into the nlsat solver. - // - svector m_literal2constraint; - struct eq { - bool operator()(unsigned_vector const &a, unsigned_vector const &b) const { - return a == b; - } - }; - - - - map, eq> m_vars2mon; // 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(unsigned v, polynomial_ref_vector & definitions) { + void mk_definition(unsigned v, polynomial_ref_vector &definitions, vector& denominators) { + auto &pm = m_nlsat->pm(); + polynomial::polynomial_ref p(pm); + rational den(1); + if (m_nla_core.emons().is_monic_var(v)) { + auto const &m = m_nla_core.emons()[v]; + for (auto v2 : m.vars()) { + polynomial_ref pw(definitions.get(v2), m_nlsat->pm()); + if (!p) + p = pw; + else + p = p * pw; + } + } + else if (lra.column_has_term(v)) { + for (auto const &[w, coeff] : lra.get_term(v)) { + den = lcm(denominator(coeff), den); + } + for (auto const &[w, coeff] : lra.get_term(v)) { + auto coeff1 = den * coeff; + polynomial_ref pw(definitions.get(w), m_nlsat->pm()); + if (!p) + p = constant(coeff1) * pw; + else + p = p + (constant(coeff1) * pw); + } + } + else { + p = pm.mk_polynomial(lp2nl(v)); // nlsat var index equals v (verified above when created) + } + definitions.push_back(p); + 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)) { @@ -209,95 +117,94 @@ struct solver::imp { else p = pm.mul(p, pv); } - } - else if (lra.column_has_term(v)) { - // Scale coefficients by a common denominator so that they become integers. + } + 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); if (!p) - p = pm.mul(den*coeff, pw); + p = pm.mul(den * coeff, pw); else - p = pm.add(p, pm.mul(den*coeff, pw)); + p = pm.add(p, pm.mul(den * coeff, pw)); } - } - else { - p = pm.mk_polynomial(v); // nlsat var index equals v (verified above when created) + } + else { + p = pm.mk_polynomial(lp2nl(v)); } definitions.push_back(p); } - void setup_assignment_solver() { - SASSERT(need_check()); - reset(); - m_literal2constraint.reset(); - m_vars2mon.reset(); - init_cone_of_influence(); + void setup_solver_poly() { + m_coi.init(); auto &pm = m_nlsat->pm(); polynomial_ref_vector definitions(pm); + vector denominators; 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); // we don't really need this. It is going to be the identify map. - scoped_anum a(am()); - am().set(a, m_nla_core.val(v).to_mpq()); - m_values->push_back(a); - mk_definition(v, definitions); + if (m_coi.vars().contains(v)) { + auto j = m_nlsat->mk_var(lra.var_is_int(v)); + m_lp2nl.insert(v, j); // we don't really need this. It is going to be the identify map. + mk_definition(v, definitions, denominators); + } + else { + definitions.push_back(nullptr); + denominators.push_back(rational(0)); + } } // we rely on that all information encoded into the tableau is present as a constraint. - for (auto ci : m_constraint_set) { + 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)); + for (auto [coeff, v] : lhs) + den = lcm(lcm(den, denominator(coeff)), denominators[v]); 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)); + poly = definitions.get(v); + poly = poly * constant(den * coeff / denominators[v]); p = p + poly; } auto lit = add_constraint(p, ci, k); - m_literal2constraint.setx(lit.index(), ci, lp::null_ci); } - - log_nl(); + definitions.reset(); } - void validate_constraints() { - for (lp::constraint_index ci : lra.constraints().indices()) - if (!check_constraint(ci)) { - IF_VERBOSE(0, verbose_stream() << "constraint " << ci << " violated\n"; - lra.constraints().display(verbose_stream())); - UNREACHABLE(); - return; - } - for (auto const& m : m_nla_core.emons()) { - if (!check_monic(m)) { - IF_VERBOSE(0, verbose_stream() << "monic " << m << " violated\n"; - lra.constraints().display(verbose_stream())); - UNREACHABLE(); - return; - } - } + void setup_solver_terms() { + m_coi.init(); + // add linear inequalities from lra_solver + for (auto ci : m_coi.constraints()) + add_constraint(ci); + + // add polynomial definitions. + for (auto const &m : m_coi.mons()) + add_monic_eq(m_nla_core.emons()[m]); + + // add term definitions. + for (unsigned i : m_coi.terms()) + add_term(i); } - bool check_constraints() { - for (lp::constraint_index ci : lra.constraints().indices()) - if (!check_constraint(ci)) - return false; - for (auto const& m : m_nla_core.emons()) - if (!check_monic(m)) - return false; - return true; + + + polynomial::polynomial_ref sub(polynomial::polynomial *a, polynomial::polynomial *b) { + return polynomial_ref(m_nlsat->pm().sub(a, b), m_nlsat->pm()); + } + polynomial::polynomial_ref mul(polynomial::polynomial *a, polynomial::polynomial *b) { + return polynomial_ref(m_nlsat->pm().mul(a, b), m_nlsat->pm()); + } + polynomial::polynomial_ref var(lp::lpvar v) { + return polynomial_ref(m_nlsat->pm().mk_polynomial(lp2nl(v)), m_nlsat->pm()); + } + polynomial::polynomial_ref constant(rational const& r) { + return polynomial_ref(m_nlsat->pm().mk_const(r), m_nlsat->pm()); } /** @@ -312,7 +219,32 @@ struct solver::imp { TBD: explore more incremental ways of applying nlsat (using assumptions) */ lbool check() { - setup_solver(); + SASSERT(need_check()); + reset(); + vector core; + + smt_params_helper p(m_params); + + setup_solver_poly(); + + TRACE(nra, m_nlsat->display(tout)); + + if (p.arith_nl_log()) { + static unsigned id = 0; + std::stringstream strm; + +#ifndef SINGLE_THREAD + std::thread::id this_id = std::this_thread::get_id(); + strm << "nla_" << this_id << "." << (++id) << ".smt2"; +#else + strm << "nla_" << (++id) << ".smt2"; +#endif + std::ofstream out(strm.str()); + m_nlsat->display_smt2(out); + out << "(check-sat)\n"; + out.close(); + } + lbool r = l_undef; statistics& st = m_nla_core.lp_settings().stats().m_st; try { @@ -328,19 +260,43 @@ struct solver::imp { } } m_nlsat->collect_statistics(st); - TRACE(nra, m_nlsat->display(tout << r << "\n");); + TRACE(nra, tout << "nra result " << r << "\n"); + CTRACE(nra, false, + m_nlsat->display(tout << r << "\n"); + display(tout); + for (auto [j, x] : m_lp2nl) tout << "j" << j << " := x" << x << "\n";); switch (r) { case l_true: m_nla_core.set_use_nra_model(true); lra.init_model(); - validate_constraints(); + for (lp::constraint_index ci : lra.constraints().indices()) + if (!check_constraint(ci)) { + IF_VERBOSE(0, verbose_stream() << "constraint " << ci << " violated\n"; + lra.constraints().display(verbose_stream())); + UNREACHABLE(); + return l_undef; + } + for (auto const &m : m_nla_core.emons()) { + if (!check_monic(m)) { + IF_VERBOSE(0, verbose_stream() << "monic " << m << " violated\n"; + lra.constraints().display(verbose_stream())); + UNREACHABLE(); + return l_undef; + } + } break; case l_false: { lp::explanation ex; - constraint_core2ex(ex); + m_nlsat->get_core(core); nla::lemma_builder lemma(m_nla_core, __FUNCTION__); + for (auto c : core) { + unsigned idx = static_cast(static_cast(c) - this); + ex.push_back(idx); + } + lemma &= ex; m_nla_core.set_use_nra_model(true); + TRACE(nra, tout << lemma << "\n"); break; } case l_undef: @@ -349,13 +305,51 @@ 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& 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); - TRACE(nra, tout << "monomial: "; pm.display(tout, m); tout << "\n";); auto& coeff = pm.coeff(p, i); - TRACE(nra, tout << "coeff:"; pm.m().display(tout, coeff);); unsigned num_vars = pm.size(m); // add mon * coeff to t; @@ -378,7 +372,6 @@ struct solver::imp { v = m_vars2mon[vars]; else v = m_nla_core.add_mul_def(vars.size(), vars.data()); - TRACE(nra, tout << " vars=" << vars << "\n"); t.add_monomial(coeff, v); break; } @@ -394,7 +387,6 @@ struct solver::imp { } lbool check_assignment() { - IF_VERBOSE(1, verbose_stream() << "nra::solver::check_assignment\n";); setup_assignment_solver(); lbool r = l_undef; statistics &st = m_nla_core.lp_settings().stats().m_st; @@ -418,13 +410,16 @@ struct solver::imp { } } m_nlsat->collect_statistics(st); - TRACE(nra, m_nlsat->display(tout << r << "\n"); display(tout); tout << "m_lp2nl:\n"; - for (auto [j, x] : m_lp2nl) tout << "j" << j << " := x" << x << "\n";); switch (r) { case l_true: m_nla_core.set_use_nra_model(true); lra.init_model(); - validate_constraints(); + 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: @@ -449,22 +444,17 @@ struct solver::imp { continue; } nlsat::atom *a = m_nlsat->bool_var2atom(l.var()); - TRACE(nra, tout << "atom: "; m_nlsat->display(tout, *a); tout << "\n";); SASSERT(!a->is_root_atom()); SASSERT(a->is_ineq_atom()); auto &ia = *to_ineq_atom(a); if (ia.size() != 1) { - return l_undef; // levnach: not sure what to do here + return l_undef; // factored polynomials not handled here } - // VERIFY(ia.size() == 1); // deal with factored polynomials later - // a is an inequality atom, i.e., p > 0, p < 0, or p = 0. polynomial::polynomial const *p = ia.p(0); - TRACE(nra, tout << "polynomial: "; pm.display(tout, p); tout << "\n";); rational bound(0); lp::lar_term t; process_polynomial_check_assignment(p, bound, nl2lp, t); - // Introduce a single ineq variable and assign it per case; common handling after switch. nla::ineq inq(lp::lconstraint_kind::EQ, t, bound); // initial value overwritten in cases below switch (a->get_kind()) { case nlsat::atom::EQ: @@ -480,26 +470,14 @@ struct solver::imp { UNREACHABLE(); return l_undef; } - // Ignore a lemma which is satisfied if (m_nla_core.ineq_holds(inq)) return l_undef; lemma |= inq; } - IF_VERBOSE(1, verbose_stream() << "linear lemma: " << lemma << "\n"); this->m_nla_core.m_check_feasible = true; return l_false; } - void constraint_core2ex(lp::explanation& ex) { - vector core; - m_nlsat->get_core(core); - for (auto c : core) { - unsigned idx = static_cast(static_cast(c) - this); - ex.push_back(idx); - TRACE(nra, lra.display_constraint(tout << "ex: " << idx << ": ", idx) << "\n";); - } - } - void add_monic_eq_bound(mon_eq const& m) { if (!lra.column_has_lower_bound(m.var()) && @@ -533,15 +511,28 @@ struct solver::imp { coeffs.push_back(mpz(1)); coeffs.push_back(mpz(-1)); polynomial::polynomial_ref p(pm.mk_polynomial(2, coeffs.data(), mls), pm); - polynomial::polynomial* ps[1] = { p }; - bool even[1] = { false }; - nlsat::literal lit = m_nlsat->mk_ineq_literal(nlsat::atom::kind::EQ, 1, ps, even); + auto lit = mk_literal(p.get(), lp::lconstraint_kind::EQ); + nlsat::assumption a = nullptr; m_nlsat->mk_clause(1, &lit, nullptr); } + nlsat::literal mk_literal(polynomial::polynomial *p, lp::lconstraint_kind k) { + polynomial::polynomial *ps[1] = { p }; + bool is_even[1] = { false }; + switch (k) { + case lp::lconstraint_kind::LE: return ~m_nlsat->mk_ineq_literal(nlsat::atom::kind::GT, 1, ps, is_even); + case lp::lconstraint_kind::GE: return ~m_nlsat->mk_ineq_literal(nlsat::atom::kind::LT, 1, ps, is_even); + case lp::lconstraint_kind::LT: return m_nlsat->mk_ineq_literal(nlsat::atom::kind::LT, 1, ps, is_even); + case lp::lconstraint_kind::GT: return m_nlsat->mk_ineq_literal(nlsat::atom::kind::GT, 1, ps, is_even); + case lp::lconstraint_kind::EQ: return m_nlsat->mk_ineq_literal(nlsat::atom::kind::EQ, 1, ps, is_even); + default: UNREACHABLE(); // unreachable + } + throw default_exception("uexpected operator"); + } + void add_constraint(unsigned idx) { - auto &c = lra.constraints()[idx]; - auto &pm = m_nlsat->pm(); + auto& c = lra.constraints()[idx]; + auto& pm = m_nlsat->pm(); auto k = c.kind(); auto rhs = c.rhs(); auto lhs = c.coeffs(); @@ -558,32 +549,23 @@ struct solver::imp { } rhs *= den; polynomial::polynomial_ref p(pm.mk_linear(sz, coeffs.data(), vars.data(), -rhs), pm); - add_constraint(p, idx, k); + nlsat::literal lit = mk_literal(p.get(), k); + nlsat::assumption a = this + idx; + m_nlsat->mk_clause(1, &lit, a); } - - nlsat::literal add_constraint(polynomial::polynomial* p, unsigned idx, lp::lconstraint_kind k) { - polynomial::polynomial* ps[1] = { p }; - bool is_even[1] = { false }; + + nlsat::literal add_constraint(polynomial::polynomial *p, unsigned idx, lp::lconstraint_kind k) { + polynomial::polynomial *ps[1] = {p}; + bool is_even[1] = {false}; nlsat::literal lit; nlsat::assumption a = this + idx; switch (k) { - case lp::lconstraint_kind::LE: - lit = ~m_nlsat->mk_ineq_literal(nlsat::atom::kind::GT, 1, ps, is_even); - break; - case lp::lconstraint_kind::GE: - lit = ~m_nlsat->mk_ineq_literal(nlsat::atom::kind::LT, 1, ps, is_even); - break; - case lp::lconstraint_kind::LT: - lit = m_nlsat->mk_ineq_literal(nlsat::atom::kind::LT, 1, ps, is_even); - break; - case lp::lconstraint_kind::GT: - lit = m_nlsat->mk_ineq_literal(nlsat::atom::kind::GT, 1, ps, is_even); - break; - case lp::lconstraint_kind::EQ: - lit = m_nlsat->mk_ineq_literal(nlsat::atom::kind::EQ, 1, ps, is_even); - break; - default: - UNREACHABLE(); // unreachable + case lp::lconstraint_kind::LE: lit = ~m_nlsat->mk_ineq_literal(nlsat::atom::kind::GT, 1, ps, is_even); break; + case lp::lconstraint_kind::GE: lit = ~m_nlsat->mk_ineq_literal(nlsat::atom::kind::LT, 1, ps, is_even); break; + case lp::lconstraint_kind::LT: lit = m_nlsat->mk_ineq_literal(nlsat::atom::kind::LT, 1, ps, is_even); break; + case lp::lconstraint_kind::GT: lit = m_nlsat->mk_ineq_literal(nlsat::atom::kind::GT, 1, ps, is_even); break; + case lp::lconstraint_kind::EQ: lit = m_nlsat->mk_ineq_literal(nlsat::atom::kind::EQ, 1, ps, is_even); break; + default: UNREACHABLE(); // unreachable } m_nlsat->mk_clause(1, &lit, a); return lit; @@ -636,7 +618,7 @@ struct solver::imp { for (auto const& m : m_nla_core.emons()) if (any_of(m.vars(), [&](lp::lpvar v) { return m_lp2nl.contains(v); })) add_monic_eq_bound(m); - for (unsigned i : m_term_set) + for (unsigned i : m_coi.terms()) add_term(i); for (auto const& [v, w] : m_lp2nl) { if (lra.column_has_lower_bound(v)) @@ -665,8 +647,12 @@ struct solver::imp { case l_true: m_nla_core.set_use_nra_model(true); lra.init_model(); - if (!check_constraints()) - return l_undef; + 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; break; case l_false: { lp::explanation ex; @@ -680,6 +666,7 @@ struct solver::imp { ex.push_back(ci); nla::lemma_builder lemma(m_nla_core, __FUNCTION__); lemma &= ex; + TRACE(nra, tout << lemma << "\n"); break; } case l_undef: @@ -816,8 +803,8 @@ struct solver::imp { if (!m_lp2nl.find(v, r)) { r = m_nlsat->mk_var(is_int(v)); m_lp2nl.insert(v, r); - if (!m_term_set.contains(v) && lra.column_has_term(v)) { - m_term_set.insert(v); + if (!m_coi.terms().contains(v) && lra.column_has_term(v)) { + m_coi.terms().insert(v); } } return r; @@ -848,20 +835,55 @@ struct solver::imp { m_nlsat->mk_clause(1, &lit, nullptr); } - nlsat::anum const& value(lp::lpvar v) { - polynomial::var pv; - if (m_lp2nl.find(v, pv)) - return m_nlsat->value(pv); - else { - for (unsigned w = m_values->size(); w <= v; ++w) { - scoped_anum a(am()); - am().set(a, m_nla_core.val(w).to_mpq()); + nlsat::anum const &value(lp::lpvar v) { + init_values(v + 1); + return (*m_values)[v]; + } + + void init_values(unsigned sz) { + if (m_values->size() >= sz) + return; + unsigned w; + scoped_anum a(am()); + for (unsigned v = m_values->size(); v < sz; ++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); - } - return (*m_values)[v]; + } + else if (lra.column_has_term(v)) { + scoped_anum b(am()); + am().set(a, 0); + 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); + } + m_values->push_back(a); + } + else if (m_lp2nl.find(v, w)) { + m_values->push_back(m_nlsat->value(w)); + } + else { + am().set(a, m_nla_core.val(v).to_mpq()); + m_values->push_back(a); + } } } + + void set_value(lp::lpvar v, rational const& value) { + if (!m_values) + m_values = alloc(scoped_anum_vector, am()); + scoped_anum a(am()); + am().set(a, value.to_mpq()); + while (m_values->size() <= v) + m_values->push_back(a); + am().set((*m_values)[v], a); + } + nlsat::anum_manager& am() { return m_nlsat->am(); } @@ -919,7 +941,7 @@ lbool solver::check(dd::solver::equation_vector const& eqs) { lbool solver::check_assignment() { return m_imp->check_assignment(); -} +} bool solver::need_check() { return m_imp->need_check(); @@ -946,4 +968,8 @@ void solver::updt_params(params_ref& p) { m_imp->updt_params(p); } +void solver::set_value(lp::lpvar v, rational const& value) { + m_imp->set_value(v, value); +} + } diff --git a/src/math/lp/nra_solver.h b/src/math/lp/nra_solver.h index f3b3bf69c..1e4e2829f 100644 --- a/src/math/lp/nra_solver.h +++ b/src/math/lp/nra_solver.h @@ -48,7 +48,7 @@ namespace nra { lbool check(dd::solver::equation_vector const& eqs); /** - \brief Check feasibility moduo current value assignment. + \brief Check feasibility modulo current value assignment. */ lbool check_assignment(); @@ -64,6 +64,8 @@ namespace nra { nlsat::anum_manager& am(); + void set_value(lp::lpvar v, rational const &value); + scoped_anum& tmp1(); scoped_anum& tmp2(); From caec6927066a4a82877112a48ce417ec7a82d6ea Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Tue, 25 Nov 2025 06:16:08 -1000 Subject: [PATCH 32/42] add forgotten files Signed-off-by: Lev Nachmanson --- src/math/lp/nla_coi.cpp | 87 ++++++++ src/math/lp/nla_coi.h | 44 ++++ src/math/lp/nla_pp.cpp | 436 ++++++++++++++++++++++++++++++++++++++++ 3 files changed, 567 insertions(+) create mode 100644 src/math/lp/nla_coi.cpp create mode 100644 src/math/lp/nla_coi.h create mode 100644 src/math/lp/nla_pp.cpp diff --git a/src/math/lp/nla_coi.cpp b/src/math/lp/nla_coi.cpp new file mode 100644 index 000000000..2632ab217 --- /dev/null +++ b/src/math/lp/nla_coi.cpp @@ -0,0 +1,87 @@ +/*++ + Copyright (c) 2025 Microsoft Corporation + + Author: + Lev Nachmanson (levnach) + Nikolaj Bjorner (nbjorner) + --*/ + +#include "math/lp/nla_core.h" +#include "math/lp/nla_coi.h" + +namespace nla { + + void coi::init() { + indexed_uint_set visited; + unsigned_vector todo; + vector var2occurs; + m_term_set.reset(); + m_mon_set.reset(); + m_constraint_set.reset(); + m_var_set.reset(); + auto& lra = c.lra_solver(); + + for (auto ci : lra.constraints().indices()) { + auto const& c = lra.constraints()[ci]; + if (c.is_auxiliary()) + continue; + for (auto const& [coeff, v] : c.coeffs()) { + var2occurs.reserve(v + 1); + var2occurs[v].constraints.push_back(ci); + } + } + + for (auto const& m : c.emons()) { + for (auto v : m.vars()) { + var2occurs.reserve(v + 1); + var2occurs[v].monics.push_back(m.var()); + } + } + + for (const auto *t : lra.terms() ) { + for (auto const iv : *t) { + auto v = iv.j(); + var2occurs.reserve(v + 1); + var2occurs[v].terms.push_back(t->j()); + } + } + + for (auto const& m : c.to_refine()) + todo.push_back(m); + + for (unsigned i = 0; i < todo.size(); ++i) { + auto v = todo[i]; + if (visited.contains(v)) + continue; + visited.insert(v); + m_var_set.insert(v); + var2occurs.reserve(v + 1); + for (auto ci : var2occurs[v].constraints) { + m_constraint_set.insert(ci); + auto const& c = lra.constraints()[ci]; + for (auto const& [coeff, w] : c.coeffs()) + todo.push_back(w); + } + for (auto w : var2occurs[v].monics) + todo.push_back(w); + + for (auto ti : var2occurs[v].terms) { + for (auto iv : lra.get_term(ti)) + todo.push_back(iv.j()); + todo.push_back(ti); + } + + if (lra.column_has_term(v)) { + m_term_set.insert(v); + for (auto kv : lra.get_term(v)) + todo.push_back(kv.j()); + } + + if (c.is_monic_var(v)) { + m_mon_set.insert(v); + for (auto w : c.emons()[v]) + todo.push_back(w); + } + } + } +} diff --git a/src/math/lp/nla_coi.h b/src/math/lp/nla_coi.h new file mode 100644 index 000000000..7424a5392 --- /dev/null +++ b/src/math/lp/nla_coi.h @@ -0,0 +1,44 @@ +/*++ + Copyright (c) 2025 Microsoft Corporation + + Abstract: + Class for computing the cone of influence for NL constraints. + It includes variables that come from monomials that have incorrect evaluation and + transitively all constraints and variables that are connected. + + Author: + Lev Nachmanson (levnach) + Nikolaj Bjorner (nbjorner) + --*/ + +#pragma once +#include "util/uint_set.h" +#include "util/vector.h" + +namespace nla { + + class core; + + class coi { + core& c; + indexed_uint_set m_mon_set, m_constraint_set; + indexed_uint_set m_term_set, m_var_set; + + struct occurs { + unsigned_vector constraints; + unsigned_vector monics; + unsigned_vector terms; + }; + + public: + coi(core& c) : c(c) {} + + void init(); + + indexed_uint_set const& mons() const { return m_mon_set; } + indexed_uint_set const& constraints() const { return m_constraint_set; } + indexed_uint_set& terms() { return m_term_set; } + indexed_uint_set const &vars() { return m_var_set; } + + }; +} diff --git a/src/math/lp/nla_pp.cpp b/src/math/lp/nla_pp.cpp new file mode 100644 index 000000000..00ee7cb51 --- /dev/null +++ b/src/math/lp/nla_pp.cpp @@ -0,0 +1,436 @@ +/*++ +Copyright (c) 2017 Microsoft Corporation + +Module Name: + + nla_core.cpp + +Author: + Lev Nachmanson (levnach) + Nikolaj Bjorner (nbjorner) + +--*/ + +#include "math/lp/nla_core.h" +using namespace nla; + +template +std::ostream& core::print_product(const T& m, std::ostream& out) const { + bool first = true; + for (lpvar v : m) { + if (!first) + out << " * "; + else + first = false; + if (lp_settings().print_external_var_name()) + out << lra.get_variable_name(v); + else + out << "j" << v; + } + return out; +} + +template +std::string core::product_indices_str(const T& m) const { + std::stringstream out; + bool first = true; + for (lpvar v : m) { + if (!first) + out << "*"; + else + first = false; + out << "j" << v; + ; + } + return out.str(); +} + +std::ostream& core::print_factor(const factor& f, std::ostream& out) const { + if (f.sign()) + out << "- "; + if (f.is_var()) { + out << "VAR, " << pp(f.var()); + } else { + out << "MON, v" << m_emons[f.var()] << " = "; + print_product(m_emons[f.var()].rvars(), out); + } + out << "\n"; + return out; +} + +std::ostream& core::print_factor_with_vars(const factor& f, std::ostream& out) const { + if (f.is_var()) { + out << pp(f.var()); + } else { + out << " MON = " << pp_mon_with_vars(*this, m_emons[f.var()]); + } + return out; +} + +std::ostream& core::print_monic(const monic& m, std::ostream& out) const { + if (lp_settings().print_external_var_name()) + out << "[" << m.var() << "] := " << lra.get_variable_name(m.var()) << " := "; + else + out << "j" << m.var() << " := "; + print_product(m.vars(), out) << "\n"; + return out; +} + +std::ostream& core::print_bfc(const factorization& m, std::ostream& out) const { + SASSERT(m.size() == 2); + out << "( x = " << pp(m[0]) << "* y = " << pp(m[1]) << ")"; + return out; +} + +std::ostream& core::print_monic_with_vars(lpvar v, std::ostream& out) const { + return print_monic_with_vars(m_emons[v], out); +} + +template +std::ostream& core::print_product_with_vars(const T& m, std::ostream& out) const { + print_product(m, out) << "\n"; + for (unsigned k = 0; k < m.size(); k++) { + print_var(m[k], out); + } + return out; +} + +std::ostream& core::print_monic_with_vars(const monic& m, std::ostream& out) const { + out << "[" << pp(m.var()) << "]\n"; + out << "vars:"; + print_product_with_vars(m.vars(), out) << "\n"; + if (m.vars() == m.rvars()) + out << "same rvars, and m.rsign = " << m.rsign() << " of course\n"; + else { + out << "rvars:"; + print_product_with_vars(m.rvars(), out) << "\n"; + out << "rsign:" << m.rsign() << "\n"; + } + return out; +} + +std::ostream& core::print_explanation(const lp::explanation& exp, std::ostream& out) const { + out << "expl: "; + unsigned i = 0; + for (auto p : exp) { + out << "(" << p.ci() << ")"; + lra.constraints().display(out, [this](lpvar j) { return var_str(j); }, p.ci()); + if (++i < exp.size()) + out << " "; + } + return out; +} + +std::ostream& core::print_ineq(const ineq& in, std::ostream& out) const { + lra.print_term_as_indices(in.term(), out); + return out << " " << lconstraint_kind_string(in.cmp()) << " " << in.rs(); +} + +std::ostream& core::print_var(lpvar j, std::ostream& out) const { + if (is_monic_var(j)) + print_monic(m_emons[j], out); + + lra.print_column_info(j, out); + signed_var jr = m_evars.find(j); + out << "root="; + if (jr.sign()) { + out << "-"; + } + + out << lra.get_variable_name(jr.var()) << "\n"; + return out; +} + +std::ostream& core::print_monics(std::ostream& out) const { + for (auto& m : m_emons) + print_monic_with_vars(m, out); + return out; +} + +std::ostream& core::print_ineqs(const lemma& l, std::ostream& out) const { + std::unordered_set vars; + out << "ineqs: "; + if (l.ineqs().size() == 0) { + out << "conflict\n"; + } else { + for (unsigned i = 0; i < l.ineqs().size(); i++) { + auto& in = l.ineqs()[i]; + print_ineq(in, out); + if (i + 1 < l.ineqs().size()) out << " or "; + for (lp::lar_term::ival p : in.term()) + vars.insert(p.j()); + } + out << std::endl; + for (lpvar j : vars) { + print_var(j, out); + } + out << "\n"; + } + return out; +} + +std::ostream& core::print_factorization(const factorization& f, std::ostream& out) const { + if (f.is_mon()) { + out << "is_mon " << pp_mon(*this, f.mon()); + } else { + for (unsigned k = 0; k < f.size(); k++) { + out << "(" << pp(f[k]) << ")"; + if (k < f.size() - 1) + out << "*"; + } + } + return out; +} + +void core::trace_print_monic_and_factorization(const monic& rm, const factorization& f, std::ostream& out) const { + out << "rooted vars: "; + print_product(rm.rvars(), out) << "\n"; + out << "mon: " << pp_mon(*this, rm.var()) << "\n"; + out << "value: " << var_val(rm) << "\n"; + print_factorization(f, out << "fact: ") << "\n"; +} + +template +void core::trace_print_rms(const T& p, std::ostream& out) { + out << "p = {\n"; + for (auto j : p) { + out << "j = " << j << ", rm = " << m_emons[j] << "\n"; + } + out << "}"; +} + +void core::print_monic_stats(const monic& m, std::ostream& out) { + if (m.size() == 2) return; + monic_coeff mc = canonize_monic(m); + for (unsigned i = 0; i < mc.vars().size(); i++) { + if (abs(val(mc.vars()[i])) == rational(1)) { + auto vv = mc.vars(); + vv.erase(vv.begin() + i); + monic const* sv = m_emons.find_canonical(vv); + if (!sv) { + out << "nf length" << vv.size() << "\n"; + ; + } + } + } +} + +void core::print_stats(std::ostream& out) { +} + + +std::ostream& core::print_terms(std::ostream& out) const { + for (const auto* t : lra.terms()) { + out << "term:"; + print_term(*t, out) << std::endl; + print_var(t->j(), out); + } + return out; +} + +std::ostream& core::print_term(const lp::lar_term& t, std::ostream& out) const { + return lp::print_linear_combination_customized( + t.coeffs_as_vector(), + [this](lpvar j) { return var_str(j); }, + out); +} + +std::string core::var_str(lpvar j) const { + std::string result; + if (is_monic_var(j)) + result += product_indices_str(m_emons[j].vars()) + (check_monic(m_emons[j]) ? "" : "_"); + else + result += std::string("j") + lp::T_to_string(j); + // result += ":w" + lp::T_to_string(get_var_weight(j)); + return result; +} + +std::ostream& core::display_row(std::ostream& out, lp::row_strip const& row) const { + auto display_coeff = [&](bool first, lp::mpq const& p) { + if (first && p == 1) + return; + if (first && p > 0) + return; + else if (p == 1) + out << " + "; + else if (p > 0) + out << " + " << p << " * "; + else if (p == -1) + out << " - "; + else if (first) + out << p << " * "; + else + out << " - " << -p << " * "; + }; + auto display_var = [&](bool first, lp::mpq p, lp::lpvar v) { + if (is_monic_var(v)) { + for (auto w : m_emons[v].vars()) + p *= m_evars.find(w).rsign(); + } + else + p *= m_evars.find(v).rsign(); + + display_coeff(first, p); + if (is_monic_var(v)) { + bool first = true; + for (auto w : m_emons[v].vars()) + out << (first ? (first = false, "") : " * ") << "j" << m_evars.find(w).var(); + } + else + out << "j" << m_evars.find(v).var(); + }; + + bool first = true; + for (auto const& ri : row) { + auto v = ri.var(); + if (lra.column_is_fixed(v)) { + auto q = lra.get_column_value(v).x; + if (q == 0) + continue; + q = q * ri.coeff(); + if (first) + out << q; + else if (q > 0) + out << " + " << q; + else if (q < 0) + out << " - " << -q; + } + else if (lra.column_has_term(v)) { + auto const& t = lra.get_term(v); + for (lp::lar_term::ival p : t) { + display_var(first, p.coeff() * ri.coeff(), p.j()); + first = false; + } + } + else { + display_var(first, ri.coeff(), ri.var()); + } + first = false; + } + out << " = 0\n"; + return out; +} + +std::ostream& core::display(std::ostream& out) { + for (auto& m : m_emons) + print_monic(m, out); + return out; +} + +std::ostream& core::display_smt(std::ostream& out) { + out << "(set-option :unsat_core true)\n"; + display_declarations_smt(out); + unsigned id = 0; + for (auto& c : lra.constraints().active()) + display_constraint_smt(out, id++, c); + out << "(check-sat)\n"; + out << "(get-unsat-core)\n"; + out << "(reset)\n"; + return out; +} + + +std::ostream& core::display_declarations_smt(std::ostream& out) const { + for (unsigned v = 0; v < lra.column_count(); ++v) { + if (is_monic_var(v)) { + out << "(define-const x" << v << " "; + out << (lra.var_is_int(v) ? "Int" : "Real"); + auto const& m = m_emons[v]; + out << " (*"; + for (auto w : m.vars()) + out << " x" << w; + out << ")"; + out << "); " << val(v) << " = "; + rational p(1); + for (auto w : m.vars()) + p *= val(v); + out << p; + out << "\n"; + } + else { + out << "(declare-const x" << v << " "; + out << (lra.var_is_int(v) ? "Int" : "Real"); + out << "); " << val(v) << "\n"; + } + } + return out; +} + +std::ostream& core::display_constraint_smt(std::ostream& out, unsigned id, lp::lar_base_constraint const& c) const { + auto k = c.kind(); + auto rhs = c.rhs(); + auto lhs = c.coeffs(); + auto sz = lhs.size(); + rational den = denominator(rhs); + for (auto [coeff, v] : lhs) + den = lcm(den, denominator(coeff)); + rhs *= den; + + auto value_of = [&](lp::lpvar v) { + if (is_monic_var(v)) { + auto& m = m_emons[v]; + rational p(1); + for (auto w : m.vars()) + p *= val(w); + return p; + } + return val(v); + }; + + switch (k) { + case lp::lconstraint_kind::LE: + out << "(assert (! (<= "; + break; + case lp::lconstraint_kind::GE: + out << "(assert (! (>= "; + break; + case lp::lconstraint_kind::LT: + out << "(assert (! (< "; + break; + case lp::lconstraint_kind::GT: + out << "(assert (! (> "; + break; + case lp::lconstraint_kind::EQ: + out << "(assert (! (= "; + break; + default: + UNREACHABLE(); // unreachable + } + rational lhs_val(0); + if (lhs.size() > 1) + out << "(+"; + for (auto [coeff, v] : lhs) { + auto c = coeff * den; + if (c == 1) + out << " x" << v; + else + out << " (* " << c << " x" << v << ")"; + lhs_val += value_of(v) * c; + } + if (lhs.size() > 1) + out << ")"; + out << " " << rhs << ") :named a" << id << ")); "; + bool evaluation = true; + switch (k) { + case lp::lconstraint_kind::LE: + evaluation = lhs_val <= rhs; + break; + case lp::lconstraint_kind::GE: + evaluation = lhs_val >= rhs; + break; + case lp::lconstraint_kind::LT: + evaluation = lhs_val < rhs; + break; + case lp::lconstraint_kind::GT: + evaluation = lhs_val > rhs; + break; + case lp::lconstraint_kind::EQ: + evaluation = lhs_val == rhs; + break; + default: + UNREACHABLE(); // unreachable + } + out << (evaluation ? "true" : "false"); + out << "\n"; + return out; +} From 543a473993db14c1e9f1214e74544776d21ad82e Mon Sep 17 00:00:00 2001 From: Lev Nachmanson <5377127+levnach@users.noreply.github.com> Date: Tue, 16 Dec 2025 17:55:26 -1000 Subject: [PATCH 33/42] Update nlsat_explain.cpp Remove a duplicate call --- src/nlsat/nlsat_explain.cpp | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/src/nlsat/nlsat_explain.cpp b/src/nlsat/nlsat_explain.cpp index 2c744be4b..af5efae5f 100644 --- a/src/nlsat/nlsat_explain.cpp +++ b/src/nlsat/nlsat_explain.cpp @@ -457,8 +457,7 @@ namespace nlsat { TRACE(nlsat_explain, tout << "lc: " << lc << " reduct: " << reduct << "\n";); insert_fresh_factors_in_todo(lc); if (!is_zero(lc) && sign(lc)) { - insert_fresh_factors_in_todo(lc); - TRACE(nlsat_explain, tout << "lc does no vaninsh\n";); + TRACE(nlsat_explain, tout << "lc does no vanish\n";); return; } add_zero_assumption(lc); From 6d3f3f2c3528c8be6debe7fb9d4e2fd9d0336a89 Mon Sep 17 00:00:00 2001 From: Valentin Promies Date: Fri, 20 Feb 2026 12:56:27 +0100 Subject: [PATCH 34/42] fix --- src/nlsat/nlsat_explain.cpp | 17 ++++++++++------- src/nlsat/nlsat_solver.cpp | 2 +- 2 files changed, 11 insertions(+), 8 deletions(-) diff --git a/src/nlsat/nlsat_explain.cpp b/src/nlsat/nlsat_explain.cpp index 06e6e15d0..f4a04edf3 100644 --- a/src/nlsat/nlsat_explain.cpp +++ b/src/nlsat/nlsat_explain.cpp @@ -50,6 +50,7 @@ namespace nlsat { bool m_factor; bool m_add_all_coeffs; bool m_add_zero_disc; + bool m_linear_project; assignment const & sample() const { return m_solver.sample(); } assignment & sample() { return m_solver.sample(); } @@ -102,6 +103,8 @@ namespace nlsat { m_minimize_cores = false; m_add_all_coeffs = false; m_add_zero_disc = false; + m_linear_project = false; + } // display helpers moved to free functions in nlsat_common.h @@ -1144,9 +1147,9 @@ namespace nlsat { /** * \brief add cell literals for the linearized projection and categorize the polynomials in ps - * - ps_below will contain all polynomials from ps which have a root below m_assignment w.r.t. x - * - ps_above will contain all polynomials from ps which have a root above m_assignment w.r.t. x - * - ps_equal will contain at least one polynomial from ps which have a root equal to m_assignment + * - ps_below will contain all polynomials from ps which have a root below sample() w.r.t. x + * - ps_above will contain all polynomials from ps which have a root above sample() w.r.t. x + * - ps_equal will contain at least one polynomial from ps which have a root equal to sample() * - In addition, they may contain additional linear polynomials added as cell boundaries * - The back elements of ps_below, ps_above, ps_equal are the polynomials used for the cell literals */ @@ -1159,8 +1162,8 @@ namespace nlsat { ps_above.reset(); ps_equal.reset(); - SASSERT(m_assignment.is_assigned(x)); - anum const & x_val = m_assignment.value(x); + SASSERT(sample().is_assigned(x)); + anum const & x_val = sample().value(x); bool lower_inf = true, upper_inf = true; scoped_anum lower(m_am), upper(m_am); @@ -1177,7 +1180,7 @@ namespace nlsat { roots.reset(); // Temporarily unassign x, s.t. isolate_roots does not assume p as constant. - m_am.isolate_roots(p, undef_var_assignment(m_assignment, x), roots); + m_am.isolate_roots(p, undef_var_assignment(sample(), x), roots); unsigned num_roots = roots.size(); if (num_roots == 0) continue; @@ -1298,7 +1301,7 @@ namespace nlsat { polynomial_ref_vector ps_above_sample(m_pm); polynomial_ref_vector ps_equal_sample(m_pm); var x = m_todo.extract_max_polys(ps); - if (!m_assignment.is_assigned(x)) { + if (!sample().is_assigned(x)) { // top level projection like original // we could also do a covering-style projection, sparing some resultants add_lcs(ps, x); diff --git a/src/nlsat/nlsat_solver.cpp b/src/nlsat/nlsat_solver.cpp index fdfed0d9a..30673e901 100644 --- a/src/nlsat/nlsat_solver.cpp +++ b/src/nlsat/nlsat_solver.cpp @@ -2197,7 +2197,7 @@ namespace nlsat { clause.reset(); m_lazy_clause.reset(); m_explain.set_linear_project(true); - m_explain.main_operator(1, &best_literal, m_lazy_clause); + m_explain.compute_conflict_explanation(1, &best_literal, m_lazy_clause); m_explain.set_linear_project(false); for (auto l : m_lazy_clause) { From 95afda383c4ad147744cc3beb352ff1b44520b9d Mon Sep 17 00:00:00 2001 From: Valentin Promies Date: Fri, 20 Feb 2026 16:01:06 +0100 Subject: [PATCH 35/42] move linear cell construction to levelwise --- src/nlsat/levelwise.cpp | 77 +++++++++++- src/nlsat/levelwise.h | 2 +- src/nlsat/nlsat_explain.cpp | 234 ++++++------------------------------ src/nlsat/nlsat_explain.h | 7 +- src/nlsat/nlsat_solver.cpp | 4 +- 5 files changed, 119 insertions(+), 205 deletions(-) diff --git a/src/nlsat/levelwise.cpp b/src/nlsat/levelwise.cpp index 03459b019..1a1e23c4e 100644 --- a/src/nlsat/levelwise.cpp +++ b/src/nlsat/levelwise.cpp @@ -73,6 +73,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(); } // Utility: call fn for each distinct irreducible factor of poly @@ -245,7 +247,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), @@ -254,7 +257,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); @@ -994,6 +998,66 @@ namespace nlsat { } } + + void mk_linear_poly_from_root(anum const& a, polynomial_ref& p) { + rational r; + m_am.to_rational(a, r); + p = m_pm.mk_polynomial(m_level); + p = denominator(r)*p - numerator(r); + } + + // 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)) { + // TODO: FAIL + NOT_IMPLEMENTED_YET(); + } + else if (m_pm.total_degree(m_I[m_level].l) > 1) { + mk_linear_poly_from_root(v, p_lower); + // add p_lower and according i.r.e. to relevant places + m_I[m_level].l = p_lower; + m_I[m_level].l_index = 1; + m_level_ps.push_back(p_lower); + r.emplace((r.begin() + m_l_rf), m_am, p_lower, 1, v, m_level_ps.size()-1); + m_poly_has_roots.push_back(true); + } + 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); + mk_linear_poly_from_root(between, p_lower); + // add p_lower and according i.r.e. to relevant places + m_I[m_level].l = p_lower; + m_I[m_level].l_index = 1; + m_level_ps.push_back(p_lower); + r.emplace((r.begin() + m_l_rf + 1), m_am, p_lower, 1, between, m_level_ps.size()-1); + m_poly_has_roots.push_back(true); + ++m_l_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); + mk_linear_poly_from_root(between, p_upper); + // add p_lower and according i.r.e. to relevant places + m_I[m_level].u = p_upper; + m_I[m_level].u_index = 1; + m_level_ps.push_back(p_lower); + r.emplace((r.begin() + m_u_rf), m_am, p_upper, 1, between, m_level_ps.size()-1); + m_poly_has_roots.push_back(true); + } + } + // 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). @@ -1009,6 +1073,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; } @@ -1360,8 +1428,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 f4a04edf3..bd31d9866 100644 --- a/src/nlsat/nlsat_explain.cpp +++ b/src/nlsat/nlsat_explain.cpp @@ -50,7 +50,6 @@ namespace nlsat { bool m_factor; bool m_add_all_coeffs; bool m_add_zero_disc; - bool m_linear_project; assignment const & sample() const { return m_solver.sample(); } assignment & sample() { return m_solver.sample(); } @@ -103,8 +102,6 @@ namespace nlsat { m_minimize_cores = false; m_add_all_coeffs = false; m_add_zero_disc = false; - m_linear_project = false; - } // display helpers moved to free functions in nlsat_common.h @@ -1043,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";); @@ -1145,130 +1142,6 @@ namespace nlsat { } - /** - * \brief add cell literals for the linearized projection and categorize the polynomials in ps - * - ps_below will contain all polynomials from ps which have a root below sample() w.r.t. x - * - ps_above will contain all polynomials from ps which have a root above sample() w.r.t. x - * - ps_equal will contain at least one polynomial from ps which have a root equal to sample() - * - In addition, they may contain additional linear polynomials added as cell boundaries - * - The back elements of ps_below, ps_above, ps_equal are the polynomials used for the cell literals - */ - void add_cell_lits_linear(polynomial_ref_vector const& ps, - var const x, - polynomial_ref_vector& ps_below, - polynomial_ref_vector& ps_above, - polynomial_ref_vector& ps_equal) { - ps_below.reset(); - ps_above.reset(); - ps_equal.reset(); - - SASSERT(sample().is_assigned(x)); - anum const & x_val = sample().value(x); - - bool lower_inf = true, upper_inf = true; - scoped_anum lower(m_am), upper(m_am); - polynomial_ref p_lower(m_pm), p_upper(m_pm); - - scoped_anum_vector & roots = m_roots_tmp; - polynomial_ref p(m_pm); - - unsigned sz = ps.size(); - for (unsigned k = 0; k < sz; k++) { - p = ps.get(k); - if (max_var(p) != x) - continue; - roots.reset(); - - // Temporarily unassign x, s.t. isolate_roots does not assume p as constant. - m_am.isolate_roots(p, undef_var_assignment(sample(), x), roots); - unsigned num_roots = roots.size(); - if (num_roots == 0) - continue; - - // find p's smallest root above the sample - unsigned i = 0; - int s = 1; - for (; i < num_roots; ++i) { - s = m_am.compare(x_val, roots[i]); - if (s <= 0) break; - } - - if (s == 0) { - // roots[i] == x_val - ps_equal.push_back(p); - p_lower = p; - break; // TODO: choose the best among multiple section polynomials? - } - else if (s < 0) { - // x_val < roots[i] - ps_above.push_back(p); - if (upper_inf || m_am.lt(roots[i], upper)) { - upper_inf = false; - m_am.set(upper, roots[i]); - p_upper = p; - } - } - // in any case, roots[i-1] might provide a lower bound if it exists - if (i > 0) { - // roots[i-1] < x_val - ps_below.push_back(p); - if (lower_inf || m_am.lt(lower, roots[i-1])) { - lower_inf = false; - m_am.set(lower, roots[i-1]); - p_lower = p; - } - } - } - - // add linear cell bounds - - if (!ps_equal.empty()) { - if (!m_am.is_rational(x_val)) { - // TODO: FAIL - NOT_IMPLEMENTED_YET(); - } - else if (m_pm.total_degree(p_lower) > 1) { - rational bound; - m_am.to_rational(x_val, bound); - p_lower = m_pm.mk_polynomial(x); - p_lower = denominator(bound)*p_lower - numerator(bound); - } - add_root_literal(atom::ROOT_EQ, x, 1, p_lower); - // make sure bounding poly is at the back of the vector - ps_equal.push_back(p_lower); - return; - } - if (!lower_inf) { - bool approximate = (m_pm.total_degree(p_lower) > 1); - if (approximate) { - scoped_anum between(m_am); - m_am.select(lower, x_val, between); - rational new_bound; - m_am.to_rational(between, new_bound); - p_lower = m_pm.mk_polynomial(x); - p_lower = denominator(new_bound)*p_lower - numerator(new_bound); - } - add_root_literal((/*approximate ||*/ m_full_dimensional) ? atom::ROOT_GE : atom::ROOT_GT, x, 1, p_lower); - // make sure bounding poly is at the back of the vector - ps_below.push_back(p_lower); - } - if (!upper_inf) { - bool approximate = (m_pm.total_degree(p_upper) > 1); - if (approximate) { - scoped_anum between(m_am); - m_am.select(x_val, upper, between); - rational new_bound; - m_am.to_rational(between, new_bound); - p_upper = m_pm.mk_polynomial(x); - p_upper = denominator(new_bound)*p_upper - numerator(new_bound); - } - add_root_literal((/*approximate ||*/ m_full_dimensional) ? atom::ROOT_LE : atom::ROOT_LT, x, 1, p_upper); - // make sure bounding poly is at the back of the vector - ps_above.push_back(p_upper); - } - } - - /** * \brief compute the resultants of p with each polynomial in ps w.r.t. x */ @@ -1283,69 +1156,6 @@ namespace nlsat { } - /** - * Linearized projection based on: - * Valentin Promies, Jasper Nalbach, Erika Abraham and Paul Wagner - * "More is Less: Adding Polynomials for Faster Explanations in NLSAT" - * in CADE30, 2025 - */ - void linear_project(polynomial_ref_vector & ps, var max_x) { - if (ps.empty()) - return; - m_todo.reset(); - for (poly* p : ps) { - m_todo.insert(p); - } - - polynomial_ref_vector ps_below_sample(m_pm); - polynomial_ref_vector ps_above_sample(m_pm); - polynomial_ref_vector ps_equal_sample(m_pm); - var x = m_todo.extract_max_polys(ps); - if (!sample().is_assigned(x)) { - // top level projection like original - // we could also do a covering-style projection, sparing some resultants - add_lcs(ps, x); - psc_discriminant(ps, x); - psc_resultant(ps, x); - x = m_todo.extract_max_polys(ps); - } - - while (true) { - add_cell_lits_linear(ps, x, ps_below_sample, ps_above_sample, ps_equal_sample); - if (all_univ(ps, x) && m_todo.empty()) { - m_todo.reset(); - break; - } - add_lcs(ps, x); - psc_discriminant(ps, x); - polynomial_ref lb(m_pm); - polynomial_ref ub(m_pm); - - if (!ps_equal_sample.empty()) { - // section - lb = ps_equal_sample.back(); - psc_resultants_with(ps, lb, x); - } - else { - if (!ps_below_sample.empty()) { - lb = ps_below_sample.back(); - psc_resultants_with(ps_below_sample, lb, x); - } - if (!ps_above_sample.empty()) { - ub = ps_above_sample.back(); - psc_resultants_with(ps_above_sample, ub, x); - if (!ps_below_sample.empty()) { - // also need resultant between bounds - psc(lb, ub, x); - } - } - } - if (m_todo.empty()) - break; - x = m_todo.extract_max_polys(ps); - } - } - bool check_already_added() const { for (bool b : m_already_added_literal) { (void)b; @@ -1902,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, m_cache); // TODO: make lws call linear + 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) { @@ -2056,10 +1898,6 @@ namespace nlsat { m_imp->m_simplify_cores = f; } - void explain::set_linear_project(bool f) { - m_imp->m_linear_project = f; - } - void explain::set_full_dimensional(bool f) { m_imp->m_full_dimensional = f; } @@ -2084,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 d3c0e84e6..e33477a80 100644 --- a/src/nlsat/nlsat_explain.h +++ b/src/nlsat/nlsat_explain.h @@ -44,7 +44,6 @@ namespace nlsat { void set_full_dimensional(bool f); void set_minimize_cores(bool f); void set_factor(bool f); - void set_linear_project(bool f); void set_add_all_coeffs(bool f); void set_add_zero_disc(bool f); @@ -67,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 30673e901..a24cf1530 100644 --- a/src/nlsat/nlsat_solver.cpp +++ b/src/nlsat/nlsat_solver.cpp @@ -2196,9 +2196,7 @@ namespace nlsat { SASSERT(best_literal != null_literal); clause.reset(); m_lazy_clause.reset(); - m_explain.set_linear_project(true); - m_explain.compute_conflict_explanation(1, &best_literal, m_lazy_clause); - m_explain.set_linear_project(false); + m_explain.compute_linear_explanation(1, &best_literal, m_lazy_clause); for (auto l : m_lazy_clause) { clause.push_back(l); From 3a995bbb0c11099236038636947dc061d31ff7c5 Mon Sep 17 00:00:00 2001 From: Valentin Promies Date: Mon, 23 Feb 2026 14:45:03 +0100 Subject: [PATCH 36/42] fix --- src/nlsat/levelwise.cpp | 42 ++++++++++++++++++------------------- src/nlsat/nlsat_explain.cpp | 2 +- 2 files changed, 22 insertions(+), 22 deletions(-) diff --git a/src/nlsat/levelwise.cpp b/src/nlsat/levelwise.cpp index 1a1e23c4e..2ec1e74b1 100644 --- a/src/nlsat/levelwise.cpp +++ b/src/nlsat/levelwise.cpp @@ -999,11 +999,23 @@ namespace nlsat { } - void mk_linear_poly_from_root(anum const& a, polynomial_ref& p) { + 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. @@ -1016,17 +1028,12 @@ namespace nlsat { auto& r = m_rel.m_rfunc; if (m_I[m_level].is_section()) { if (!m_am.is_rational(v)) { - // TODO: FAIL NOT_IMPLEMENTED_YET(); } else if (m_pm.total_degree(m_I[m_level].l) > 1) { - mk_linear_poly_from_root(v, p_lower); - // add p_lower and according i.r.e. to relevant places - m_I[m_level].l = p_lower; - m_I[m_level].l_index = 1; - m_level_ps.push_back(p_lower); + 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); - m_poly_has_roots.push_back(true); } return; } @@ -1035,26 +1042,19 @@ namespace nlsat { 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); - mk_linear_poly_from_root(between, p_lower); - // add p_lower and according i.r.e. to relevant places - m_I[m_level].l = p_lower; - m_I[m_level].l_index = 1; - m_level_ps.push_back(p_lower); + 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_poly_has_roots.push_back(true); ++m_l_rf; - ++m_u_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); - mk_linear_poly_from_root(between, p_upper); - // add p_lower and according i.r.e. to relevant places - m_I[m_level].u = p_upper; - m_I[m_level].u_index = 1; - m_level_ps.push_back(p_lower); + // 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); - m_poly_has_roots.push_back(true); } } diff --git a/src/nlsat/nlsat_explain.cpp b/src/nlsat/nlsat_explain.cpp index bd31d9866..8f7ca86ba 100644 --- a/src/nlsat/nlsat_explain.cpp +++ b/src/nlsat/nlsat_explain.cpp @@ -1733,7 +1733,7 @@ namespace nlsat { // 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, m_cache); // TODO: make lws call linear + bool levelwise_ok = levelwise_single_cell(m_ps, max_x, m_cache, true); SASSERT(levelwise_ok); m_solver.record_levelwise_result(levelwise_ok); From 77d81de03fda0fc65ee9f2c336afd9b51c5a7a33 Mon Sep 17 00:00:00 2001 From: Valentin Promies Date: Fri, 6 Mar 2026 14:30:22 +0100 Subject: [PATCH 37/42] fix --- src/nlsat/nlsat_explain.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/nlsat/nlsat_explain.cpp b/src/nlsat/nlsat_explain.cpp index 8f7ca86ba..1555e2989 100644 --- a/src/nlsat/nlsat_explain.cpp +++ b/src/nlsat/nlsat_explain.cpp @@ -1733,7 +1733,7 @@ namespace nlsat { // 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, m_cache, true); + 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); From 6c27140bc9dccce09e00cf990c3fcba5c5837eb8 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Thu, 12 Mar 2026 14:35:52 -1000 Subject: [PATCH 38/42] 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> --- src/math/lp/nla_core.cpp | 6 +- src/math/lp/nla_core.h | 1 + src/math/lp/nra_solver.cpp | 95 ++++++++++++++++++-------------- src/params/smt_params_helper.pyg | 1 + 4 files changed, 62 insertions(+), 41 deletions(-) diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp index cda9a3383..a05975d8a 100644 --- a/src/math/lp/nla_core.cpp +++ b/src/math/lp/nla_core.cpp @@ -1330,10 +1330,14 @@ lbool core::check(unsigned level) { return l_false; } - if (no_effect()) { + if (no_effect() && params().arith_nl_nra_check_assignment() && m_check_assignment_fail_cnt < 10) { 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; + else + --m_check_assignment_fail_cnt; } if (no_effect() && should_run_bounded_nlsat()) diff --git a/src/math/lp/nla_core.h b/src/math/lp/nla_core.h index e7484396a..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(); diff --git a/src/math/lp/nra_solver.cpp b/src/math/lp/nra_solver.cpp index 82e4c64d7..b6d22bff5 100644 --- a/src/math/lp/nra_solver.cpp +++ b/src/math/lp/nra_solver.cpp @@ -448,48 +448,63 @@ struct solver::imp { lbool add_lemma(nlsat::literal_vector const &clause) { u_map nl2lp = reverse_lp2nl(); polynomial::manager &pm = m_nlsat->pm(); - 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()); - SASSERT(!a->is_root_atom()); - SASSERT(a->is_ineq_atom()); - auto &ia = *to_ineq_atom(a); - if (ia.size() != 1) { - return l_undef; // factored polynomials not handled here - } - polynomial::polynomial const *p = ia.p(0); - rational bound(0); - lp::lar_term t; - process_polynomial_check_assignment(p, bound, nl2lp, t); + 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(); - return l_undef; + 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 (m_nla_core.ineq_holds(inq)) - return l_undef; - lemma |= inq; - } - this->m_nla_core.m_check_feasible = true; - return l_false; + 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; } diff --git a/src/params/smt_params_helper.pyg b/src/params/smt_params_helper.pyg index 451a07964..7ea231f55 100644 --- a/src/params/smt_params_helper.pyg +++ b/src/params/smt_params_helper.pyg @@ -60,6 +60,7 @@ 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.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'), From 7c9f930ef18f15bdf7376d48ad7b0296bbe04087 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Thu, 12 Mar 2026 16:38:06 -1000 Subject: [PATCH 39/42] 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> --- src/math/lp/nla_core.cpp | 2 +- src/params/smt_params_helper.pyg | 1 + 2 files changed, 2 insertions(+), 1 deletion(-) diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp index a05975d8a..96f18ccf3 100644 --- a/src/math/lp/nla_core.cpp +++ b/src/math/lp/nla_core.cpp @@ -1330,7 +1330,7 @@ lbool core::check(unsigned level) { return l_false; } - if (no_effect() && params().arith_nl_nra_check_assignment() && m_check_assignment_fail_cnt < 10) { + 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(); diff --git a/src/params/smt_params_helper.pyg b/src/params/smt_params_helper.pyg index 7ea231f55..6cb7d315d 100644 --- a/src/params/smt_params_helper.pyg +++ b/src/params/smt_params_helper.pyg @@ -61,6 +61,7 @@ def_module_params(module_name='smt', ('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, 10, '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'), From b11e5a4f34b785c2cf709ef9a7810f056f2c382b Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Fri, 13 Mar 2026 07:59:09 -1000 Subject: [PATCH 40/42] Add cha_abort_on_fail parameter to control failure counter decrement Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> --- src/math/lp/nla_core.cpp | 2 +- src/params/smt_params_helper.pyg | 1 + 2 files changed, 2 insertions(+), 1 deletion(-) diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp index 96f18ccf3..5f256bc9f 100644 --- a/src/math/lp/nla_core.cpp +++ b/src/math/lp/nla_core.cpp @@ -1336,7 +1336,7 @@ lbool core::check(unsigned level) { ret = m_nra.check_assignment(); if (ret != l_true) ++m_check_assignment_fail_cnt; - else + else if (!params().arith_nl_cha_abort_on_fail()) --m_check_assignment_fail_cnt; } diff --git a/src/params/smt_params_helper.pyg b/src/params/smt_params_helper.pyg index 6cb7d315d..bdcc96c4a 100644 --- a/src/params/smt_params_helper.pyg +++ b/src/params/smt_params_helper.pyg @@ -62,6 +62,7 @@ def_module_params(module_name='smt', ('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, 10, 'maximum consecutive check_assignment failures before disabling it'), + ('arith.nl.cha_abort_on_fail', BOOL, False, 'if true, never decrement check_assignment failure counter on success'), ('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'), From 9f4e1f57059b931bf2e9d27d3fbeefc43101dff2 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Fri, 13 Mar 2026 14:33:30 -1000 Subject: [PATCH 41/42] abort nla check_assignment after a set number of allowed failures Signed-off-by: Lev Nachmanson --- src/math/lp/nla_core.cpp | 2 -- src/params/smt_params_helper.pyg | 1 - 2 files changed, 3 deletions(-) diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp index 5f256bc9f..e789bc637 100644 --- a/src/math/lp/nla_core.cpp +++ b/src/math/lp/nla_core.cpp @@ -1336,8 +1336,6 @@ lbool core::check(unsigned level) { ret = m_nra.check_assignment(); if (ret != l_true) ++m_check_assignment_fail_cnt; - else if (!params().arith_nl_cha_abort_on_fail()) - --m_check_assignment_fail_cnt; } if (no_effect() && should_run_bounded_nlsat()) diff --git a/src/params/smt_params_helper.pyg b/src/params/smt_params_helper.pyg index bdcc96c4a..6cb7d315d 100644 --- a/src/params/smt_params_helper.pyg +++ b/src/params/smt_params_helper.pyg @@ -62,7 +62,6 @@ def_module_params(module_name='smt', ('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, 10, 'maximum consecutive check_assignment failures before disabling it'), - ('arith.nl.cha_abort_on_fail', BOOL, False, 'if true, never decrement check_assignment failure counter on success'), ('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'), From 1e27af9f7a1b37d1dee31e8042c29eaa033820f9 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Sat, 14 Mar 2026 07:26:58 -1000 Subject: [PATCH 42/42] change the default number of failures in check_assignment to 7 Signed-off-by: Lev Nachmanson --- src/params/smt_params_helper.pyg | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/params/smt_params_helper.pyg b/src/params/smt_params_helper.pyg index 6cb7d315d..708d88bb6 100644 --- a/src/params/smt_params_helper.pyg +++ b/src/params/smt_params_helper.pyg @@ -61,7 +61,7 @@ def_module_params(module_name='smt', ('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, 10, 'maximum consecutive check_assignment failures before disabling it'), + ('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'),