diff --git a/src/math/grobner/pdd_solver.cpp b/src/math/grobner/pdd_solver.cpp index 74f4e80f9..2693c003b 100644 --- a/src/math/grobner/pdd_solver.cpp +++ b/src/math/grobner/pdd_solver.cpp @@ -70,17 +70,18 @@ namespace dd { } -void solver::set_thresholds(unsigned eqs_growth, unsigned expr_size_growth, unsigned expr_degree_growth) { + void solver::adjust_cfg() { + auto & cfg = m_config; IF_VERBOSE(3, verbose_stream() << "start saturate\n"; display_statistics(verbose_stream())); - 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; + cfg.m_eqs_threshold = static_cast(cfg.m_eqs_growth * ceil(log(1 + m_to_simplify.size()))* m_to_simplify.size()); + cfg.m_expr_size_limit = 0; + cfg.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()); + cfg.m_expr_size_limit = std::max(cfg.m_expr_size_limit, (unsigned)e->poly().tree_size()); + cfg.m_expr_degree_limit = std::max(cfg.m_expr_degree_limit, e->poly().degree()); } - m_config.m_expr_size_limit *= expr_size_growth; - m_config.m_expr_degree_limit *= expr_degree_growth;; + 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"; verbose_stream() << "set m_config.m_expr_size_limit to " << m_config.m_expr_size_limit << "\n"; diff --git a/src/math/grobner/pdd_solver.h b/src/math/grobner/pdd_solver.h index ad767c80a..35f918779 100644 --- a/src/math/grobner/pdd_solver.h +++ b/src/math/grobner/pdd_solver.h @@ -55,6 +55,10 @@ public: unsigned m_max_simplified; unsigned m_random_seed; bool m_enable_exlin; + unsigned m_eqs_growth; + unsigned m_expr_size_growth; + unsigned m_expr_degree_growth; + unsigned m_number_of_conflicts_to_report; config() : m_eqs_threshold(UINT_MAX), m_expr_size_limit(UINT_MAX), @@ -62,7 +66,11 @@ public: m_max_steps(UINT_MAX), m_max_simplified(UINT_MAX), m_random_seed(0), - m_enable_exlin(false) + m_enable_exlin(false), + m_eqs_growth(10), + m_expr_size_growth(10), + m_expr_degree_growth(5), + m_number_of_conflicts_to_report(1) {} }; @@ -121,6 +129,7 @@ public: void set(print_dep_t& pd) { m_print_dep = pd; } void set(config const& c) { m_config = c; } + void adjust_cfg(); void reset(); void add(pdd const& p) { add(p, nullptr); } @@ -138,7 +147,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(unsigned eqs_growth, unsigned expr_size_growth, unsigned expr_degree_growth); + unsigned number_of_conflicts_to_report() const { return m_config.m_number_of_conflicts_to_report; } private: bool step(); @@ -185,7 +194,6 @@ private: scoped_process(solver& g, equation* e): g(g), e(e) {} ~scoped_process(); }; - void update_stats_max_degree_and_size(const equation& e); }; diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp index 4f7b6e24c..c3e4a8fd1 100644 --- a/src/math/lp/nla_core.cpp +++ b/src/math/lp/nla_core.cpp @@ -1401,10 +1401,13 @@ void core::run_grobner() { configure_grobner(); m_pdd_grobner.saturate(); bool conflict = false; + unsigned n = m_pdd_grobner.number_of_conflicts_to_report(); + SASSERT(n > 0); for (auto eq : m_pdd_grobner.equations()) { if (check_pdd_eq(eq)) { conflict = true; - break; + if (--n == 0) + break; } } if (conflict) { @@ -1452,11 +1455,12 @@ void core::configure_grobner() { cfg.m_expr_size_limit = (unsigned)tree_size; cfg.m_max_steps = gr_eq_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(); + cfg.m_expr_degree_growth = m_nla_settings.grobner_expr_degree_growth(); + cfg.m_number_of_conflicts_to_report = m_nla_settings.grobner_number_of_conflicts_to_report(); m_pdd_grobner.set(cfg); - 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_grobner.adjust_cfg(); m_pdd_manager.set_max_num_nodes(10000); // or something proportional to the number of initial nodes. } diff --git a/src/math/lp/nla_params.pyg b/src/math/lp/nla_params.pyg index 6e6a6509b..0e0c5df15 100644 --- a/src/math/lp/nla_params.pyg +++ b/src/math/lp/nla_params.pyg @@ -12,6 +12,7 @@ def_module_params('nla', ('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_cnfl_to_report', UINT, 1, 'grobner\'s maximum number of conflicts to report'), ('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 60bd87354..cf63bb9dd 100644 --- a/src/math/lp/nla_settings.h +++ b/src/math/lp/nla_settings.h @@ -37,6 +37,7 @@ class nla_settings { unsigned m_grobner_expr_size_growth; unsigned m_grobner_expr_degree_growth; unsigned m_grobner_max_simplified; + unsigned m_grobner_number_of_conflicts_to_report; public: nla_settings() : m_run_order(true), m_run_tangents(true), @@ -86,6 +87,9 @@ public: unsigned grobner_max_simplified() const { return m_grobner_max_simplified; } unsigned & grobner_max_simplified() { return m_grobner_max_simplified; } + unsigned grobner_number_of_conflicts_to_report() const { return m_grobner_number_of_conflicts_to_report; } + unsigned & grobner_number_of_conflicts_to_report() { return m_grobner_number_of_conflicts_to_report; } + }; } diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index c5e649153..d491f42ad 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -460,6 +460,7 @@ class theory_lra::imp { 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(); + m_nla->get_core()->m_nla_settings.grobner_number_of_conflicts_to_report() = nla.grobner_cnfl_to_report(); } }