mirror of
https://github.com/Z3Prover/z3
synced 2026-07-17 12:35:44 +00:00
dbb91de64b
* 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>
106 lines
3.9 KiB
C++
106 lines
3.9 KiB
C++
/*++
|
|
Copyright (c) 2017 Microsoft Corporation
|
|
|
|
Author:
|
|
Nikolaj Bjorner (nbjorner)
|
|
Lev Nachmanson (levnach)
|
|
|
|
--*/
|
|
#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/params.h"
|
|
#include "util/uint_set.h"
|
|
#include "math/grobner/pdd_solver.h"
|
|
|
|
namespace nla {
|
|
class core;
|
|
|
|
class grobner : common {
|
|
struct config {
|
|
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;
|
|
indexed_uint_set m_rows;
|
|
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;
|
|
std::unordered_map<unsigned_vector, lpvar, hash_svector> m_mon2var;
|
|
|
|
lp::lp_settings& lp_settings();
|
|
|
|
// solving
|
|
bool is_conflicting();
|
|
bool is_conflicting(dd::solver::equation const& eq);
|
|
|
|
bool propagate_eqs();
|
|
bool propagate_fixed(dd::solver::equation const& eq);
|
|
|
|
bool propagate_factorization();
|
|
bool propagate_factorization(dd::solver::equation const& eq);
|
|
|
|
bool propagate_linear_equations();
|
|
bool propagate_linear_equations(dd::solver::equation const& eq);
|
|
|
|
bool propagate_quotients();
|
|
bool propagate_quotients(dd::solver::equation const& eq);
|
|
|
|
svector<std::pair<unsigned, unsigned>> m_powers;
|
|
bool propagate_gcd_test();
|
|
bool propagate_gcd_test(dd::solver::equation const& eq);
|
|
|
|
std::pair<lp::lar_term, rational> linear_to_term(dd::pdd q);
|
|
|
|
void add_dependencies(lemma_builder& lemma, dd::solver::equation const& eq);
|
|
void explain(dd::solver::equation const& eq, lp::explanation& exp);
|
|
|
|
bool add_horner_conflict(dd::solver::equation const& eq);
|
|
bool is_nla_conflict(dd::solver::equation const& eq);
|
|
bool add_nla_conflict(dd::solver::equation const& eq);
|
|
void check_missing_propagation(dd::solver::equation const& eq);
|
|
|
|
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();
|
|
void find_nl_cluster();
|
|
void prepare_rows_and_active_vars();
|
|
void add_var_and_its_factors_to_q_and_collect_new_rows(lpvar j, svector<lpvar>& q);
|
|
void add_row(const std_vector<lp::row_cell<rational>>& row);
|
|
void add_fixed_monic(unsigned j);
|
|
bool is_solved(dd::pdd const& p, unsigned& v, dd::pdd& r);
|
|
void add_eq(dd::pdd& p, u_dependency* dep);
|
|
bool is_pseudo_linear(monic const& m) const;
|
|
const rational& val_of_fixed_var_with_deps(lpvar j, u_dependency*& dep);
|
|
dd::pdd pdd_expr(const rational& c, lpvar j, u_dependency*& dep);
|
|
dd::pdd pdd_expr(lp::lar_term const& t, u_dependency*& dep);
|
|
|
|
void display_matrix_of_m_rows(std::ostream& out) const;
|
|
std::ostream& diagnose_pdd_miss(std::ostream& out);
|
|
|
|
public:
|
|
grobner(core *core);
|
|
void operator()();
|
|
void updt_params(params_ref const& p);
|
|
};
|
|
}
|