mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
make grobner quota a parameter
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
parent
06203d227e
commit
b577544830
|
@ -1397,7 +1397,7 @@ std::ostream& core::print_term( const lp::lar_term& t, std::ostream& out) const
|
|||
|
||||
|
||||
void core::run_grobner() {
|
||||
static unsigned quota = 8;
|
||||
unsigned& quota = m_grobner_quota;
|
||||
if (quota == 0) {
|
||||
return;
|
||||
}
|
||||
|
@ -1418,10 +1418,7 @@ void core::run_grobner() {
|
|||
IF_VERBOSE(2, verbose_stream() << "grobner conflict\n");
|
||||
}
|
||||
else {
|
||||
if (quota == 1)
|
||||
quota = 0;
|
||||
else
|
||||
quota /= 2;
|
||||
quota >>= 1;
|
||||
IF_VERBOSE(2, verbose_stream() << "grobner miss, quota " << quota << "\n");
|
||||
IF_VERBOSE(4, diagnose_pdd_miss(verbose_stream()));
|
||||
}
|
||||
|
|
|
@ -96,14 +96,13 @@ public:
|
|||
nla_settings m_nla_settings;
|
||||
dd::pdd_manager m_pdd_manager;
|
||||
dd::solver m_pdd_grobner;
|
||||
|
||||
private:
|
||||
emonics m_emons;
|
||||
svector<lpvar> m_add_buffer;
|
||||
mutable lp::int_set m_active_var_set;
|
||||
lp::int_set m_rows;
|
||||
|
||||
public:
|
||||
unsigned m_grobner_quota;
|
||||
reslimit m_reslim;
|
||||
|
||||
|
||||
|
|
|
@ -13,6 +13,7 @@ def_module_params('nla',
|
|||
('grobner_expr_degree_growth', UINT, 2, 'grobner\'s maximum expr degree growth'),
|
||||
('grobner_max_simplified', UINT, 10000, 'grobner\'s maximum number of simplifications'),
|
||||
('grobner_cnfl_to_report', UINT, 1, 'grobner\'s maximum number of conflicts to report'),
|
||||
('gr_q', UINT, 8, 'grobner\'s quota'),
|
||||
('grobner_subs_fixed', BOOL, False, 'substitute fixed variables by constants')
|
||||
))
|
||||
|
||||
|
|
|
@ -461,6 +461,7 @@ class theory_lra::imp {
|
|||
m_nla->get_core()->m_nla_settings.grobner_expr_degree_growth() = nla.grobner_expr_degree_growth();
|
||||
m_nla->get_core()->m_nla_settings.grobner_max_simplified() = nla.grobner_max_simplified();
|
||||
m_nla->get_core()->m_nla_settings.grobner_number_of_conflicts_to_report() = nla.grobner_cnfl_to_report();
|
||||
m_nla->get_core()->m_grobner_quota = nla.gr_q();
|
||||
|
||||
}
|
||||
}
|
||||
|
|
Loading…
Reference in a new issue