mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
cleanup the grobner config init
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
parent
f2884088cc
commit
06203d227e
|
@ -46,6 +46,7 @@ namespace dd {
|
|||
public:
|
||||
enum semantics { free_e, mod2_e, zero_one_vars_e };
|
||||
private:
|
||||
friend test;
|
||||
friend pdd;
|
||||
friend pdd_iterator;
|
||||
|
||||
|
|
|
@ -83,7 +83,7 @@ namespace dd {
|
|||
cfg.m_expr_size_limit *= cfg.m_expr_size_growth;
|
||||
cfg.m_expr_degree_limit *= cfg.m_expr_degree_growth;;
|
||||
|
||||
IF_VERBOSE(3, verbose_stream() << "set m_config.m_eqs_threshold to 10 * " << 10 * ceil(log(m_to_simplify.size())) << "* " << m_to_simplify.size() << " = " << m_config.m_eqs_threshold << "\n";
|
||||
IF_VERBOSE(3, verbose_stream() << "set m_config.m_eqs_threshold " << m_config.m_eqs_threshold << "\n";
|
||||
verbose_stream() << "set m_config.m_expr_size_limit to " << m_config.m_expr_size_limit << "\n";
|
||||
verbose_stream() << "set m_config.m_expr_degree_limit to " << m_config.m_expr_degree_limit << "\n";
|
||||
);
|
||||
|
@ -91,6 +91,9 @@ namespace dd {
|
|||
}
|
||||
void solver::saturate() {
|
||||
simplify();
|
||||
if (done()) {
|
||||
return;
|
||||
}
|
||||
init_saturate();
|
||||
TRACE("dd.solver", display(tout););
|
||||
try {
|
||||
|
|
|
@ -1452,16 +1452,8 @@ void core::configure_grobner() {
|
|||
}
|
||||
#endif
|
||||
|
||||
double tree_size = 100;
|
||||
unsigned gr_eq_size = 0;
|
||||
for (auto* e : m_pdd_grobner.equations()) {
|
||||
tree_size = std::max(tree_size, e->poly().tree_size());
|
||||
gr_eq_size ++;
|
||||
}
|
||||
tree_size *= 10;
|
||||
struct dd::solver::config cfg;
|
||||
cfg.m_expr_size_limit = (unsigned)tree_size;
|
||||
cfg.m_max_steps = gr_eq_size;
|
||||
cfg.m_max_steps = m_pdd_grobner.equations().size();
|
||||
cfg.m_max_simplified = m_nla_settings.grobner_max_simplified();
|
||||
cfg.m_eqs_growth = m_nla_settings.grobner_eqs_growth();
|
||||
cfg.m_expr_size_growth = m_nla_settings.grobner_expr_size_growth();
|
||||
|
|
|
@ -9,8 +9,8 @@ def_module_params('nla',
|
|||
('horner_row_length_limit', UINT, 10, 'row is disregarded by the heuristic if its length is longer than the value'),
|
||||
('grobner', BOOL, True, 'run grobner\'s basis heuristic'),
|
||||
('grobner_eqs_growth', UINT, 10, 'grobner\'s number of equalities growth '),
|
||||
('grobner_expr_size_growth', UINT, 10, 'grobner\'s maximum expr size growth'),
|
||||
('grobner_expr_degree_growth', UINT, 10, 'grobner\'s maximum expr degree growth'),
|
||||
('grobner_expr_size_growth', UINT, 2, 'grobner\'s maximum expr size growth'),
|
||||
('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'),
|
||||
('grobner_subs_fixed', BOOL, False, 'substitute fixed variables by constants')
|
||||
|
|
Loading…
Reference in a new issue