From cf54e985e841e41ca4df766daf6a0a2918be0342 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 29 Oct 2025 11:19:10 -0700 Subject: [PATCH] separate out bounds Signed-off-by: Nikolaj Bjorner --- src/math/lp/CMakeLists.txt | 1 + src/math/lp/nla_bounds.cpp | 42 +++++++++++++++++++++++++++++++++ src/math/lp/nla_bounds.h | 40 +++++++++++++++++++++++++++++++ src/math/lp/nla_core.cpp | 23 +++--------------- src/math/lp/nla_core.h | 16 ++++++++----- src/math/lp/nla_stellensatz.cpp | 11 +++++---- 6 files changed, 103 insertions(+), 30 deletions(-) create mode 100644 src/math/lp/nla_bounds.cpp create mode 100644 src/math/lp/nla_bounds.h diff --git a/src/math/lp/CMakeLists.txt b/src/math/lp/CMakeLists.txt index 03dad2cc2..011c03f29 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_bounds.cpp nla_coi.cpp nla_common.cpp nla_core.cpp diff --git a/src/math/lp/nla_bounds.cpp b/src/math/lp/nla_bounds.cpp new file mode 100644 index 000000000..57b5a1ba2 --- /dev/null +++ b/src/math/lp/nla_bounds.cpp @@ -0,0 +1,42 @@ + +/*++ + Copyright (c) 2025 Microsoft Corporation + + Module Name: + + nla_bounds.cpp + + Author: + Lev Nachmanson (levnach) + Nikolaj Bjorner (nbjorner) + +--*/ + +#include "nla_bounds.h" +#include "nla_core.h" + + +namespace nla { + + bounds::bounds(core *c) : common(c) {} + + // looking for a free variable inside of a monic to split + void bounds::operator()() { + for (lpvar i : c().to_refine()) { + auto const &m = c().emons()[i]; + for (lpvar j : m.vars()) { + if (!c().var_is_free(j)) + continue; + if (m.is_bound_propagated()) + continue; + c().emons().set_bound_propagated(m); + // split the free variable (j <= 0, or j > 0), and return + auto i(ineq(j, lp::lconstraint_kind::LE, rational::zero())); + c().add_literal(i); + TRACE(nla_solver, c().print_ineq(i, tout) << "\n"); + ++c().lp_settings().stats().m_nla_add_bounds; + return; + } + } + } +} // namespace nla diff --git a/src/math/lp/nla_bounds.h b/src/math/lp/nla_bounds.h new file mode 100644 index 000000000..2d46f32fb --- /dev/null +++ b/src/math/lp/nla_bounds.h @@ -0,0 +1,40 @@ + +/*++ + Copyright (c) 2025 Microsoft Corporation + + Module Name: + + nla_bounds.h + + Author: + Lev Nachmanson (levnach) + Nikolaj Bjorner (nbjorner) + + Abstract: + Create bounds for variables that occur in non-linear monomials. + The bounds should ensure that variables are either fixes at -1, 0, 1, below or above these values. + This ensures that basic lemmas that case split on values -1, 0, 1 are robust under model changes. + +--*/ +#pragma once + + + +#include "math/lp/nla_common.h" +#include "math/lp/nla_intervals.h" +#include "math/lp/nex.h" +#include "math/lp/cross_nested.h" +#include "util/uint_set.h" +#include "math/grobner/pdd_solver.h" + +namespace nla { + class core; + + class bounds : common { + public: + bounds(core *core); + void operator()(); + + }; + +} // namespace nla diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp index 4457a4224..1cefffec5 100644 --- a/src/math/lp/nla_core.cpp +++ b/src/math/lp/nla_core.cpp @@ -37,7 +37,8 @@ core::core(lp::lar_solver& s, params_ref const& p, reslimit & lim) : m_monomial_bounds(this), m_stellensatz(this), m_horner(this), - m_grobner(this), + m_grobner(this), + m_bounds(this), m_emons(m_evars), m_use_nra_model(false), m_nra(s, m_nra_lim, *this, p), @@ -1268,24 +1269,6 @@ void core::check_bounded_divisions() { clear(); m_divisions.check_bounded_divisions(); } -// looking for a free variable inside of a monic to split -void core::add_bounds() { - for (auto i : m_to_refine) { - auto const& m = m_emons[i]; - for (lpvar j : m.vars()) { - if (!var_is_free(j)) - continue; - if (m.is_bound_propagated()) - continue; - m_emons.set_bound_propagated(m); - // split the free variable (j <= 0, or j > 0), and return - m_literals.push_back(ineq(j, lp::lconstraint_kind::EQ, rational::zero())); - TRACE(nla_solver, print_ineq(m_literals.back(), tout) << "\n"); - ++lp_settings().stats().m_nla_add_bounds; - return; - } - } -} lbool core::check() { lp_settings().stats().m_nla_calls++; @@ -1321,7 +1304,7 @@ lbool core::check() { { std::function check1 = [&]() { if (no_effect() && run_horner) m_horner.horner_lemmas(); }; std::function check2 = [&]() { if (no_effect() && run_grobner) m_grobner(); }; - std::function check3 = [&]() { if (no_effect() && run_bounds) add_bounds(); }; + std::function check3 = [&]() { if (no_effect() && run_bounds) m_bounds(); }; std::pair> checks[] = { {1, check1}, diff --git a/src/math/lp/nla_core.h b/src/math/lp/nla_core.h index 491729a7b..5ec5e6ad1 100644 --- a/src/math/lp/nla_core.h +++ b/src/math/lp/nla_core.h @@ -14,14 +14,15 @@ #include "math/lp/factorization.h" #include "math/lp/lp_types.h" #include "math/lp/var_eqs.h" -#include "math/lp/nla_tangent_lemmas.h" #include "math/lp/nla_basics_lemmas.h" -#include "math/lp/nla_order_lemmas.h" -#include "math/lp/nla_monotone_lemmas.h" -#include "math/lp/nla_grobner.h" -#include "math/lp/nla_powers.h" +#include "math/lp/nla_bounds.h" #include "math/lp/nla_divisions.h" +#include "math/lp/nla_grobner.h" +#include "math/lp/nla_monotone_lemmas.h" +#include "math/lp/nla_order_lemmas.h" +#include "math/lp/nla_powers.h" #include "math/lp/nla_stellensatz.h" +#include "math/lp/nla_tangent_lemmas.h" #include "math/lp/emonics.h" #include "math/lp/nex.h" #include "math/lp/horner.h" @@ -95,6 +96,7 @@ class core { bool m_check_feasible = false; horner m_horner; grobner m_grobner; + bounds m_bounds; emonics m_emons; svector m_add_buffer; mutable indexed_uint_set m_active_var_set; @@ -113,7 +115,6 @@ 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; @@ -454,6 +455,9 @@ public: bool use_nra_model() const { return m_use_nra_model; } vector const& lemmas() const { return m_lemmas; } vector const& literals() const { return m_literals; } + void add_literal(const ineq &n) { + m_literals.push_back(n); + } vector const& equalities() const { return m_equalities; } vector const& fixed_equalities() const { return m_fixed_equalities; } bool should_check_feasible() const { return m_check_feasible; } diff --git a/src/math/lp/nla_stellensatz.cpp b/src/math/lp/nla_stellensatz.cpp index 603002ba5..1e5661be4 100644 --- a/src/math/lp/nla_stellensatz.cpp +++ b/src/math/lp/nla_stellensatz.cpp @@ -317,9 +317,11 @@ namespace nla { lhs.add_monomial(rational(1), j); if (non_unit != lp::null_lpvar) { lhs.add_monomial(rational(-sign), non_unit); - add_ineq(bounds, lhs, lp::lconstraint_kind::EQ, rational(0)); + add_ineq(bounds, lhs, lp::lconstraint_kind::GE, rational(0)); + add_ineq(bounds, lhs, lp::lconstraint_kind::LE, rational(0)); } else { - add_ineq(bounds, lhs, lp::lconstraint_kind::EQ, rational(sign)); + add_ineq(bounds, lhs, lp::lconstraint_kind::GE, rational(sign)); + add_ineq(bounds, lhs, lp::lconstraint_kind::LE, rational(sign)); } } @@ -617,8 +619,8 @@ namespace nla { while (!to_refine.empty()) { lpvar j = to_refine.erase_min(); - IF_VERBOSE(2, verbose_stream() << "refining " << m_mon2vars[j] << "\n"); unsigned sz = m_monomials_to_refine.size(); + TRACE(arith, tout << "refining " << m_mon2vars[j] << " sz " << sz << "\n"); eliminate(j); for (unsigned i = sz; i < m_monomials_to_refine.size(); ++i) { auto e = m_monomials_to_refine.elem_at(i); @@ -678,6 +680,7 @@ namespace nla { // punt on equality constraints for now } } + TRACE(arith, tout << "eliminate " << m_mon2vars[mi] << " los: " << los << " his: " << his << "\n"); if (los.empty() || his.empty()) return; IF_VERBOSE(3, verbose_stream() << "lo " << los << " hi " << his << "\n"); @@ -1522,7 +1525,7 @@ namespace nla { TRACE(arith, s.display(tout)); if (!s.saturate_factors()) return l_false; - // s.saturate_constraints(); ? + s.saturate_constraints2(); if (sz == lra_solver->number_of_vars()) return l_undef; }