mirror of
https://github.com/Z3Prover/z3
synced 2026-05-13 05:35:26 +00:00
Add adaptive growth knobs for Gröbner under arith.nl.grobner_adaptive (#9390)
* 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) <noreply@anthropic.com> * 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) <noreply@anthropic.com> Co-authored-by: Arie Gurfinkel <arie.gurfinkel@gmail.com> Co-authored-by: Copilot <175728472+Copilot@users.noreply.github.com>
This commit is contained in:
Arie
GitHub
parent
c40f8a200e
commit
dbb91de64b
3 changed files with 81 additions and 30 deletions
|
|
@ -10,6 +10,8 @@ Author:
|
|||
Nikolaj Bjorner (nbjorner)
|
||||
|
||||
--*/
|
||||
#include <algorithm>
|
||||
#include <climits>
|
||||
#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<uint64_t>(x) * boost) / unit;
|
||||
return y > UINT_MAX ? UINT_MAX : static_cast<unsigned>(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();
|
||||
|
|
|
|||
|
|
@ -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<unsigned_vector, lpvar, hash_svector> 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();
|
||||
|
|
|
|||
|
|
@ -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'),
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue