From d1e9998332c0db020be30f63b976ff060eaf523a Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Wed, 8 Jan 2020 17:26:04 -0800 Subject: [PATCH] add a config parameter to grobner Signed-off-by: Lev Nachmanson --- src/math/grobner/pdd_solver.cpp | 8 +++----- src/math/grobner/pdd_solver.h | 1 + src/math/lp/nla_core.cpp | 9 ++++++--- src/math/lp/nla_params.pyg | 4 ++-- src/math/lp/nla_settings.h | 8 +++++--- src/smt/theory_lra.cpp | 2 ++ 6 files changed, 19 insertions(+), 13 deletions(-) diff --git a/src/math/grobner/pdd_solver.cpp b/src/math/grobner/pdd_solver.cpp index 265343fb1..56e71570a 100644 --- a/src/math/grobner/pdd_solver.cpp +++ b/src/math/grobner/pdd_solver.cpp @@ -70,11 +70,9 @@ namespace dd { } +// some of the config fields are set, others are calculated void solver::set_thresholds() { IF_VERBOSE(3, verbose_stream() << "start saturate\n"; display_statistics(verbose_stream())); - if (m_to_simplify.size() == 0) - return; - m_config.m_eqs_threshold = 10 * ceil(log(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) { @@ -89,9 +87,9 @@ namespace dd { 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; - + m_config.m_max_simplified = 7000; } + void solver::saturate() { simplify(); init_saturate(); diff --git a/src/math/grobner/pdd_solver.h b/src/math/grobner/pdd_solver.h index beefdbb71..82c8a1c87 100644 --- a/src/math/grobner/pdd_solver.h +++ b/src/math/grobner/pdd_solver.h @@ -55,6 +55,7 @@ public: unsigned m_max_simplified; unsigned m_random_seed; bool m_enable_exlin; + unsigned m_eqs_growth; config() : m_eqs_threshold(UINT_MAX), m_expr_size_limit(UINT_MAX), diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp index 5bd6baba4..8e5a981be 100644 --- a/src/math/lp/nla_core.cpp +++ b/src/math/lp/nla_core.cpp @@ -1425,18 +1425,21 @@ void core::run_pdd_grobner() { // 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()) { 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_eqs_threshold = m_pdd_grobner.equations().size()*5; - cfg.m_max_steps = m_pdd_grobner.equations().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;; + m_pdd_grobner.set(cfg); + m_pdd_grobner.set_thresholds(); m_pdd_manager.set_max_num_nodes(10000); // or something proportional to the number of initial nodes. - m_pdd_grobner.set_thresholds(); m_pdd_grobner.saturate(); bool conflict = false; for (auto eq : m_pdd_grobner.equations()) { diff --git a/src/math/lp/nla_params.pyg b/src/math/lp/nla_params.pyg index b1b971ffa..ebc668352 100644 --- a/src/math/lp/nla_params.pyg +++ b/src/math/lp/nla_params.pyg @@ -4,11 +4,11 @@ def_module_params('nla', ('order', BOOL, True, 'run order lemmas'), ('tangents', BOOL, True, 'run tangent lemmas'), ('horner', BOOL, True, 'run horner\'s heuristic'), - ('horner_subs_fixed', BOOL, True, 'substitute fixed variables by constants'), + ('horner_subs_fixed', BOOL, False, 'substitute fixed variables by constants'), ('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_threshold', UINT, 512, 'grobner\'s maximum number of equalities'), + ('grobner_eqs_growth', UINT, 10, 'grobner\'s maximum number of equalities'), ('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 f24346ecb..97b713ced 100644 --- a/src/math/lp/nla_settings.h +++ b/src/math/lp/nla_settings.h @@ -29,9 +29,10 @@ class nla_settings { unsigned m_horner_row_length_limit; bool m_horner_subs_fixed; // grobner fields - bool m_run_grobner; + bool m_run_grobner; unsigned m_grobner_row_length_limit; - bool m_grobner_subs_fixed; + bool m_grobner_subs_fixed; + unsigned m_grobner_eqs_growth; public: nla_settings() : m_run_order(true), m_run_tangents(true), @@ -43,7 +44,8 @@ public: m_grobner_row_length_limit(50), m_grobner_subs_fixed(false) {} - + unsigned grobner_eqs_growth() const { return m_grobner_eqs_growth;} + unsigned& grobner_eqs_growth() { return m_grobner_eqs_growth;} bool run_order() const { return m_run_order; } bool& run_order() { return m_run_order; } diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index 7690aac01..0a8c113bc 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -456,6 +456,8 @@ class theory_lra::imp { m_nla->get_core()->m_nla_settings.horner_row_length_limit() = nla.horner_row_length_limit(); 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(); + } }