diff --git a/src/math/grobner/pdd_simplifier.cpp b/src/math/grobner/pdd_simplifier.cpp index 2d7dc9500..72b629d90 100644 --- a/src/math/grobner/pdd_simplifier.cpp +++ b/src/math/grobner/pdd_simplifier.cpp @@ -152,7 +152,7 @@ namespace dd { s.push_equation(solver::to_simplify, dst); } // v has been eliminated. - SASSERT(!dst->poly().free_vars().contains(v)); + // SASSERT(!dst->poly().free_vars().contains(v)); add_to_use(dst, use_list); } if (all_reduced) { diff --git a/src/math/grobner/pdd_solver.cpp b/src/math/grobner/pdd_solver.cpp index 32065a5c4..74f4e80f9 100644 --- a/src/math/grobner/pdd_solver.cpp +++ b/src/math/grobner/pdd_solver.cpp @@ -70,26 +70,22 @@ namespace dd { } - void solver::set_thresholds() { +void solver::set_thresholds(unsigned eqs_growth, unsigned expr_size_growth, unsigned expr_degree_growth) { IF_VERBOSE(3, verbose_stream() << "start saturate\n"; display_statistics(verbose_stream())); - if (m_to_simplify.size() == 0) - return; - m_config.m_eqs_threshold = static_cast(10 * ceil(log(m_to_simplify.size()))*m_to_simplify.size()); + m_config.m_eqs_threshold = static_cast(eqs_growth * ceil(log(1 + m_to_simplify.size()))* m_to_simplify.size()); m_config.m_expr_size_limit = 0; m_config.m_expr_degree_limit = 0; for (equation* e: m_to_simplify) { m_config.m_expr_size_limit = std::max(m_config.m_expr_size_limit, (unsigned)e->poly().tree_size()); m_config.m_expr_degree_limit = std::max(m_config.m_expr_degree_limit, e->poly().degree()); } - m_config.m_expr_size_limit *= 2; - m_config.m_expr_degree_limit *= 2; + m_config.m_expr_size_limit *= expr_size_growth; + m_config.m_expr_degree_limit *= 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"; 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"; ); - m_config.m_max_steps = 700; - m_config.m_max_simplified = 7000; } void solver::saturate() { diff --git a/src/math/grobner/pdd_solver.h b/src/math/grobner/pdd_solver.h index 2308e5e46..ad767c80a 100644 --- a/src/math/grobner/pdd_solver.h +++ b/src/math/grobner/pdd_solver.h @@ -138,7 +138,7 @@ public: std::ostream& display_statistics(std::ostream& out) const; const stats& get_stats() const { return m_stats; } stats& get_stats() { return m_stats; } - void set_thresholds(); + void set_thresholds(unsigned eqs_growth, unsigned expr_size_growth, unsigned expr_degree_growth); private: bool step(); diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp index 8e5a981be..4f7b6e24c 100644 --- a/src/math/lp/nla_core.cpp +++ b/src/math/lp/nla_core.cpp @@ -1289,7 +1289,7 @@ lbool core::inner_check(bool constraint_derived) { clear_and_resize_active_var_set(); if (m_nla_settings.run_grobner()) { find_nl_cluster(); - run_pdd_grobner(); + run_grobner(); } } if (done()) { @@ -1396,13 +1396,32 @@ std::ostream& core::print_term( const lp::lar_term& t, std::ostream& out) const } -void core::run_pdd_grobner() { +void core::run_grobner() { lp_settings().stats().m_grobner_calls++; + configure_grobner(); + m_pdd_grobner.saturate(); + bool conflict = false; + for (auto eq : m_pdd_grobner.equations()) { + if (check_pdd_eq(eq)) { + conflict = true; + break; + } + } + if (conflict) { + IF_VERBOSE(2, verbose_stream() << "grobner conflict\n"); + } + else { + IF_VERBOSE(2, verbose_stream() << "grobner miss\n"); + IF_VERBOSE(4, diagnose_pdd_miss(verbose_stream())); + } +} + +void core::configure_grobner() { m_pdd_grobner.reset(); try { - set_level2var_for_pdd_grobner(); + set_level2var_for_grobner(); for (unsigned i : m_rows) { - add_row_to_pdd_grobner(m_lar_solver.A_r().m_rows[i]); + add_row_to_grobner(m_lar_solver.A_r().m_rows[i]); } } catch (...) { @@ -1422,8 +1441,6 @@ void core::run_pdd_grobner() { } #endif - // configure grobner - // TBD: move this code somewhere self-contained, and tune it. double tree_size = 100; unsigned gr_eq_size = 0; for (auto* e : m_pdd_grobner.equations()) { @@ -1434,27 +1451,13 @@ void core::run_pdd_grobner() { struct dd::solver::config cfg; cfg.m_expr_size_limit = (unsigned)tree_size; cfg.m_max_steps = gr_eq_size; - cfg.m_eqs_threshold = m_nla_settings.grobner_eqs_growth() * ceil(log(gr_eq_size + 1)) * gr_eq_size;; + cfg.m_max_simplified = m_nla_settings.grobner_max_simplified(); m_pdd_grobner.set(cfg); - m_pdd_grobner.set_thresholds(); + m_pdd_grobner.set_thresholds(m_nla_settings.grobner_eqs_growth(), m_nla_settings.grobner_expr_size_growth(), + m_nla_settings.grobner_expr_degree_growth()); m_pdd_manager.set_max_num_nodes(10000); // or something proportional to the number of initial nodes. - m_pdd_grobner.saturate(); - bool conflict = false; - for (auto eq : m_pdd_grobner.equations()) { - if (check_pdd_eq(eq)) { - conflict = true; - break; - } - } - if (conflict) { - IF_VERBOSE(2, verbose_stream() << "grobner conflict\n"); - } - else { - IF_VERBOSE(2, verbose_stream() << "grobner miss\n"); - IF_VERBOSE(4, diagnose_pdd_miss(verbose_stream())); - } } std::ostream& core::diagnose_pdd_miss(std::ostream& out) { @@ -1568,7 +1571,7 @@ dd::pdd core::pdd_expr(const rational& c, lpvar j, u_dependency*& dep) { return r; } -void core::add_row_to_pdd_grobner(const vector> & row) { +void core::add_row_to_grobner(const vector> & row) { u_dependency *dep = nullptr; dd::pdd sum = m_pdd_manager.mk_val(rational(0)); for (const auto &p : row) { @@ -1639,7 +1642,7 @@ void core::set_active_vars_weights(nex_creator& nc) { } } -void core::set_level2var_for_pdd_grobner() { +void core::set_level2var_for_grobner() { unsigned n = m_lar_solver.column_count(); unsigned_vector sorted_vars(n), weighted_vars(n); for (unsigned j = 0; j < n; j++) { diff --git a/src/math/lp/nla_core.h b/src/math/lp/nla_core.h index 316f53c3a..7cccfb2b8 100644 --- a/src/math/lp/nla_core.h +++ b/src/math/lp/nla_core.h @@ -399,7 +399,7 @@ public: return lp::print_linear_combination_customized(v, [this](lpvar j) { return var_str(j); }, out); } - void run_pdd_grobner(); + void run_grobner(); 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& q); @@ -407,11 +407,12 @@ public: void display_matrix_of_m_rows(std::ostream & out) const; void set_active_vars_weights(nex_creator&); unsigned get_var_weight(lpvar) const; - void add_row_to_pdd_grobner(const vector> & row); + void add_row_to_grobner(const vector> & row); bool check_pdd_eq(const dd::solver::equation*); const rational& val_of_fixed_var_with_deps(lpvar j, u_dependency*& dep); dd::pdd pdd_expr(const rational& c, lpvar j, u_dependency*&); - void set_level2var_for_pdd_grobner(); + void set_level2var_for_grobner(); + void configure_grobner(); }; // end of core struct pp_mon { diff --git a/src/math/lp/nla_params.pyg b/src/math/lp/nla_params.pyg index ebc668352..6e6a6509b 100644 --- a/src/math/lp/nla_params.pyg +++ b/src/math/lp/nla_params.pyg @@ -8,7 +8,10 @@ def_module_params('nla', ('horner_frequency', UINT, 4, 'horner\'s call frequency'), ('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 maximum number of equalities'), + ('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_max_simplified', UINT, 10000, 'grobner\'s maximum number of simplifications'), ('grobner_subs_fixed', BOOL, False, 'substitute fixed variables by constants') )) diff --git a/src/math/lp/nla_settings.h b/src/math/lp/nla_settings.h index 97b713ced..60bd87354 100644 --- a/src/math/lp/nla_settings.h +++ b/src/math/lp/nla_settings.h @@ -33,6 +33,10 @@ class nla_settings { unsigned m_grobner_row_length_limit; bool m_grobner_subs_fixed; unsigned m_grobner_eqs_growth; + unsigned m_grobner_tree_size_growth; + unsigned m_grobner_expr_size_growth; + unsigned m_grobner_expr_degree_growth; + unsigned m_grobner_max_simplified; public: nla_settings() : m_run_order(true), m_run_tangents(true), @@ -69,5 +73,19 @@ public: unsigned& grobner_row_length_limit() { return m_grobner_row_length_limit; } bool grobner_subs_fixed() const { return m_grobner_subs_fixed; } bool& grobner_subs_fixed() { return m_grobner_subs_fixed; } + + unsigned grobner_tree_size_growth() const { return m_grobner_tree_size_growth; } + unsigned & grobner_tree_size_growth() { return m_grobner_tree_size_growth; } + + unsigned grobner_expr_size_growth() const { return m_grobner_expr_size_growth; } + unsigned & grobner_expr_size_growth() { return m_grobner_expr_size_growth; } + + unsigned grobner_expr_degree_growth() const { return m_grobner_expr_degree_growth; } + unsigned & grobner_expr_degree_growth() { return m_grobner_expr_degree_growth; } + + unsigned grobner_max_simplified() const { return m_grobner_max_simplified; } + unsigned & grobner_max_simplified() { return m_grobner_max_simplified; } + + }; } diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index 0a8c113bc..c5e649153 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -457,6 +457,9 @@ class theory_lra::imp { m_nla->get_core()->m_nla_settings.run_grobner() = nla.grobner(); m_nla->get_core()->m_nla_settings.grobner_subs_fixed() = nla.grobner_subs_fixed(); m_nla->get_core()->m_nla_settings.grobner_eqs_growth() = nla.grobner_eqs_growth(); + m_nla->get_core()->m_nla_settings.grobner_expr_size_growth() = nla.grobner_expr_size_growth(); + 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(); } }