From d60d6a0665971cf4f7813d0b9c11c145ed28e37c Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 23 Jul 2026 19:49:41 -0700 Subject: [PATCH] add incremental propagate for nla to retain some propagation lemmas --- src/math/lp/monomial_bounds.cpp | 12 +++++------- src/math/lp/monomial_bounds.h | 4 ++-- src/math/lp/nla_core.cpp | 16 +++++++++++++++- src/math/lp/nla_core.h | 1 + src/math/lp/nla_solver.cpp | 4 ++++ src/math/lp/nla_solver.h | 1 + src/smt/theory_lra.cpp | 14 ++++++++++++-- 7 files changed, 40 insertions(+), 12 deletions(-) diff --git a/src/math/lp/monomial_bounds.cpp b/src/math/lp/monomial_bounds.cpp index ddf6ae516f..36f498e333 100644 --- a/src/math/lp/monomial_bounds.cpp +++ b/src/math/lp/monomial_bounds.cpp @@ -199,13 +199,15 @@ namespace nla { } } - bool monomial_bounds::propagate_linear_monomials() { + bool monomial_bounds::propagate_changed_bounds() { bool propagated = false; for (lpvar v : c().m_monics_with_changed_bounds) { if (!c().is_monic_var(v)) continue; monic& m = c().emon(v); - if (propagate_linear_monomial(m)) + if (propagate_changed_bound(m)) + propagated = true; + if (tighten_lp(m)) propagated = true; if (c().lra.get_status() == lp::lp_status::INFEASIBLE) break; @@ -223,7 +225,7 @@ namespace nla { return true; } - bool monomial_bounds::propagate_linear_monomial(monic & m) { + bool monomial_bounds::propagate_changed_bound(monic & m) { if (m.is_propagated()) return false; lpvar w, fixed_to_zero; @@ -642,7 +644,6 @@ namespace nla { */ void monomial_bounds::propagate_lp_bound(lpvar v, lp::lconstraint_kind cmp, rational const &q, u_dependency *d) { SASSERT(cmp != llc::EQ && cmp != llc::NE); - IF_VERBOSE(1, verbose_stream() << "propagate_lp_bound: v=" << v << " cmp=" << cmp << " q=" << q << "\n";); if (!c().var_is_int(v)) c().lra.update_column_type_and_bound(v, cmp, q, d); else if (q.is_int()) { @@ -673,9 +674,6 @@ namespace nla { for (auto &m : c().emons()) if (tighten_lp(m)) new_bound = true; - if (propagate_linear_monomials()) - new_bound = true; - IF_VERBOSE(1, verbose_stream() << "tighten_lp_bounds: new_bound=" << new_bound << "\n";); return new_bound; } diff --git a/src/math/lp/monomial_bounds.h b/src/math/lp/monomial_bounds.h index a018af4539..37cdac8490 100644 --- a/src/math/lp/monomial_bounds.h +++ b/src/math/lp/monomial_bounds.h @@ -48,13 +48,13 @@ namespace nla { // linear-monomial equality propagation: // when all but one variable of a monomial are fixed, the monomial is // linear and its value/equality can be propagated into the LP solver. - bool propagate_linear_monomial(monic & m); - bool propagate_linear_monomials(); + bool propagate_changed_bound(monic & m); bool is_linear(monic const& m, lpvar& w, lpvar & fixed_to_zero); rational fixed_var_product(monic const& m, lpvar w); public: monomial_bounds(core* core); void generate_lemmas(); bool tighten_lp_bounds(); + bool propagate_changed_bounds(); }; } diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp index 2cfe1d2efa..f4baca1ced 100644 --- a/src/math/lp/nla_core.cpp +++ b/src/math/lp/nla_core.cpp @@ -1525,12 +1525,26 @@ void core::set_use_nra_model(bool m) { bool core::propagate() { - clear(); bool propagated = m_monomial_bounds.tighten_lp_bounds(); + if (m_monomial_bounds.propagate_changed_bounds()) + propagated = true; m_monics_with_changed_bounds.reset(); + if (propagated) + m_check_feasible = true; return propagated; } +bool core::incremental_propagate() { + bool propagated = false; + clear(); + if (m_monomial_bounds.propagate_changed_bounds()) + propagated = true; + m_monics_with_changed_bounds.reset(); + if (propagated) + m_check_feasible = true; + return propagated; +} + /** \brief Tighten the bounds of variables occurring in nonlinear monomials by maximizing/minimizing them over the LP tableau (analogous to theory_arith's diff --git a/src/math/lp/nla_core.h b/src/math/lp/nla_core.h index 3d6eaafabb..e0db94c1ae 100644 --- a/src/math/lp/nla_core.h +++ b/src/math/lp/nla_core.h @@ -410,6 +410,7 @@ public: bool no_lemmas_hold() const; bool propagate(); + bool incremental_propagate(); void simplify(); diff --git a/src/math/lp/nla_solver.cpp b/src/math/lp/nla_solver.cpp index 08f8c23433..b3c8453bdf 100644 --- a/src/math/lp/nla_solver.cpp +++ b/src/math/lp/nla_solver.cpp @@ -57,6 +57,10 @@ namespace nla { bool solver::propagate() { return m_core->propagate(); } + + bool solver::incremental_propagate() { + return m_core->incremental_propagate(); + } void solver::push(){ m_core->push(); diff --git a/src/math/lp/nla_solver.h b/src/math/lp/nla_solver.h index 79556c50cd..5adb87c41c 100644 --- a/src/math/lp/nla_solver.h +++ b/src/math/lp/nla_solver.h @@ -40,6 +40,7 @@ namespace nla { bool need_check(); lbool check(unsigned level); bool propagate(); + bool incremental_propagate(); void simplify() { m_core->simplify(); } lbool check_power(lpvar r, lpvar x, lpvar y); bool is_monic_var(lpvar) const; diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index 1ea654be0b..644a927293 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -2319,7 +2319,7 @@ public: get_infeasibility_explanation_and_set_conflict(); break; case l_true: - propagate_nla(); + incremental_propagate_nla(); propagate_bounds_with_lp_solver(); break; case l_undef: @@ -2332,7 +2332,17 @@ public: bool propagate_nla() { bool propagated = false; if (m_nla) { - propagated = m_nla->propagate() || propagated; + propagated = m_nla->propagate(); + add_lemmas(); + lp().collect_more_rows_for_lp_propagation(); + } + return propagated; + } + + bool incremental_propagate_nla() { + bool propagated = false; + if (m_nla) { + propagated = m_nla->incremental_propagate(); add_lemmas(); lp().collect_more_rows_for_lp_propagation(); }