From dbb91de64b1671a2318e9aa1c431c1839c0d18e6 Mon Sep 17 00:00:00 2001 From: Arie <123119895+1arie1@users.noreply.github.com> Date: Tue, 28 Apr 2026 11:50:38 -0400 Subject: [PATCH] =?UTF-8?q?Add=20adaptive=20growth=20knobs=20for=20Gr?= =?UTF-8?q?=C3=B6bner=20under=20arith.nl.grobner=5Fadaptive=20(#9390)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit * Add adaptive growth knobs for Gröbner under arith.nl.grobner_adaptive When enabled, the per-call growth budget (m_eqs_growth, m_expr_size_growth, m_expr_degree_growth, m_max_simplified) is scaled by m_growth_boost: - two consecutive productive runs bump the boost by 3/2 (cap 4x) - a miss resets the streak and decays the boost toward 1.0x by 1/4 of excess Default is off; the existing miss-frequency throttle (m_quota / m_delay_base) is unchanged, so this only affects per-call power, not call frequency. Co-Authored-By: Claude Opus 4.7 (1M context) * Update src/params/smt_params_helper.pyg Co-authored-by: Copilot <175728472+Copilot@users.noreply.github.com> --------- Co-authored-by: Claude Opus 4.7 (1M context) Co-authored-by: Arie Gurfinkel Co-authored-by: Copilot <175728472+Copilot@users.noreply.github.com> --- src/math/lp/nla_grobner.cpp | 98 ++++++++++++++++++++++---------- src/math/lp/nla_grobner.h | 12 +++- src/params/smt_params_helper.pyg | 1 + 3 files changed, 81 insertions(+), 30 deletions(-) diff --git a/src/math/lp/nla_grobner.cpp b/src/math/lp/nla_grobner.cpp index 5df8439a9..94c8c6990 100644 --- a/src/math/lp/nla_grobner.cpp +++ b/src/math/lp/nla_grobner.cpp @@ -10,6 +10,8 @@ Author: Nikolaj Bjorner (nbjorner) --*/ +#include +#include #include "util/uint_set.h" #include "params/smt_params_helper.hpp" #include "math/lp/nla_core.h" @@ -77,48 +79,45 @@ namespace nla { if (!configure()) return; + bool productive = false; + try { if (propagate_gcd_test()) - return; + productive = true; } catch (...) { - + } - m_solver.saturate(); - TRACE(grobner, m_solver.display(tout)); + if (!productive) { + m_solver.saturate(); + TRACE(grobner, m_solver.display(tout)); - if (m_delay_base > 0) - --m_delay_base; - - try { + if (m_delay_base > 0) + --m_delay_base; - if (is_conflicting()) - return; + try { + productive = is_conflicting() + || propagate_quotients() + || propagate_gcd_test() + || propagate_eqs() + || propagate_factorization() + || propagate_linear_equations(); + } + catch (...) { - if (propagate_quotients()) - return; - - if (propagate_gcd_test()) - return; - - if (propagate_eqs()) - return; - - if (propagate_factorization()) - return; - - if (propagate_linear_equations()) - return; - - } - catch (...) { - + } } // DEBUG_CODE(for (auto e : m_solver.equations()) check_missing_propagation(*e);); // for (auto e : m_solver.equations()) check_missing_propagation(*e); - + + if (c().params().arith_nl_grobner_adaptive()) + update_growth_boost(productive); + + if (productive) + return; + ++m_delay_base; if (m_quota > 0) --m_quota; @@ -127,6 +126,32 @@ namespace nla { IF_VERBOSE(5, diagnose_pdd_miss(verbose_stream())); } + void grobner::update_growth_boost(bool productive) { + // Bumping is conservative: requires two consecutive productive runs + // before any boost; misses decay toward unit by 1/4 per call. + unsigned const unit = m_config.m_adaptive_unit; + unsigned const cap = m_config.m_adaptive_max; + if (productive) { + ++m_hit_streak; + if (m_hit_streak >= m_config.m_adaptive_bump_after) { + unsigned next = m_growth_boost + (m_growth_boost >> 1); + m_growth_boost = std::min(next, cap); + m_hit_streak = 0; + } + } + else { + m_hit_streak = 0; + if (m_growth_boost > unit) { + unsigned excess = m_growth_boost - unit; + m_growth_boost -= (excess + 3) / 4; + if (m_growth_boost < unit) + m_growth_boost = unit; + } + } + IF_VERBOSE(5, verbose_stream() << "grobner adaptive boost " << m_growth_boost + << "/" << unit << (productive ? " (hit)" : " (miss)") << "\n"); + } + bool grobner::is_conflicting() { for (auto eq : m_solver.equations()) { if (is_conflicting(*eq)) { @@ -578,6 +603,21 @@ namespace nla { cfg.m_eqs_growth = c().params().arith_nl_grobner_eqs_growth(); cfg.m_expr_size_growth = c().params().arith_nl_grobner_expr_size_growth(); cfg.m_expr_degree_growth = c().params().arith_nl_grobner_expr_degree_growth(); + if (c().params().arith_nl_grobner_adaptive() && m_growth_boost != m_config.m_adaptive_unit) { + // Wider intermediate to prevent overflow when a user param is + // close to UINT_MAX; clamp before assigning back to the unsigned + // config fields. + uint64_t const unit = m_config.m_adaptive_unit; + uint64_t const boost = m_growth_boost; + auto scale = [unit, boost](unsigned x) -> unsigned { + uint64_t y = (static_cast(x) * boost) / unit; + return y > UINT_MAX ? UINT_MAX : static_cast(y); + }; + cfg.m_eqs_growth = scale(cfg.m_eqs_growth); + cfg.m_expr_size_growth = scale(cfg.m_expr_size_growth); + cfg.m_expr_degree_growth = scale(cfg.m_expr_degree_growth); + cfg.m_max_simplified = scale(cfg.m_max_simplified); + } cfg.m_number_of_conflicts_to_report = c().params().arith_nl_grobner_cnfl_to_report(); m_solver.set(cfg); m_solver.adjust_cfg(); diff --git a/src/math/lp/nla_grobner.h b/src/math/lp/nla_grobner.h index b9ed043d5..411954343 100644 --- a/src/math/lp/nla_grobner.h +++ b/src/math/lp/nla_grobner.h @@ -24,7 +24,13 @@ namespace nla { bool m_propagate_quotients = false; bool m_gcd_test = false; bool m_expand_terms = false; + // Adaptive growth (gated by arith.nl.grobner_adaptive). m_growth_boost + // is in fixed-point units of 1/m_adaptive_unit (m_adaptive_unit == 1.0x). + unsigned m_adaptive_unit = 16; + unsigned m_adaptive_max = 4 * 16; + unsigned m_adaptive_bump_after = 2; }; + config m_config; dd::pdd_manager m_pdd_manager; dd::solver m_solver; lp::lar_solver& lra; @@ -32,8 +38,9 @@ namespace nla { unsigned m_quota = 0; unsigned m_delay_base = 0; unsigned m_delay = 0; + unsigned m_growth_boost = m_config.m_adaptive_unit; + unsigned m_hit_streak = 0; bool m_add_all_eqs = false; - config m_config; std::unordered_map m_mon2var; lp::lp_settings& lp_settings(); @@ -70,6 +77,9 @@ namespace nla { bool equation_is_true(dd::solver::equation const& eq); + // adaptive growth (gated by arith.nl.grobner_adaptive) + void update_growth_boost(bool productive); + // setup bool configure(); void set_level2var(); diff --git a/src/params/smt_params_helper.pyg b/src/params/smt_params_helper.pyg index efb85a2ab..6c8ce796d 100644 --- a/src/params/smt_params_helper.pyg +++ b/src/params/smt_params_helper.pyg @@ -86,6 +86,7 @@ def_module_params(module_name='smt', ('arith.nl.grobner_propagate_quotients', BOOL, True, 'detect conflicts x*y + z = 0 where x doesn\'t divide z'), ('arith.nl.grobner_gcd_test', BOOL, True, 'detect gcd conflicts for polynomial powers x^k - y = 0'), ('arith.nl.grobner_exp_delay', BOOL, True, 'use exponential delay between grobner basis attempts'), + ('arith.nl.grobner_adaptive', BOOL, False, 'scale grobner growth knobs (eqs/size/degree/max_simplified) up on productive runs and down on misses'), ('arith.nl.gr_q', UINT, 10, 'grobner\'s quota'), ('arith.nl.grobner_subs_fixed', UINT, 1, '0 - no subs, 1 - substitute, 2 - substitute fixed zeros only'), ('arith.nl.grobner_expand_terms', BOOL, True, 'expand terms before computing grobner basis'),