diff --git a/src/math/lp/explanation.h b/src/math/lp/explanation.h index ed06d0825..c80b94eaf 100644 --- a/src/math/lp/explanation.h +++ b/src/math/lp/explanation.h @@ -65,7 +65,7 @@ public: public: cimpq(constraint_index var, const optional & val) : m_var(var), m_coeff(val) { } constraint_index ci() const { return m_var; } - mpq coeff() const { return m_coeff.undef()? one_of_type(): *m_coeff; } + mpq coeff() const { return m_coeff.initialized()? *m_coeff: one_of_type(); } }; class iterator { u_map>::iterator m_it; diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp index 66d2c7534..8cc347eec 100644 --- a/src/math/lp/nla_core.cpp +++ b/src/math/lp/nla_core.cpp @@ -1396,15 +1396,13 @@ lbool core::check(vector& l_vec) { set_use_nra_model(false); - if (false && l_vec.empty() && !done()) + if (l_vec.empty() && !done() && m_nla_settings.propagate_bounds()) m_monomial_bounds(); - if (l_vec.empty() && !done() && need_to_call_algebraic_methods()) + if (l_vec.empty() && !done() && need_run_horner()) m_horner.horner_lemmas(); - if (l_vec.empty() && !done() && m_nla_settings.run_grobner()) { - clear_and_resize_active_var_set(); - find_nl_cluster(); + if (l_vec.empty() && !done() && need_run_grobner()) { run_grobner(); } @@ -1492,6 +1490,9 @@ void core::run_grobner() { if (quota == 1) { return; } + clear_and_resize_active_var_set(); + find_nl_cluster(); + lp_settings().stats().m_grobner_calls++; configure_grobner(); m_pdd_grobner.saturate(); diff --git a/src/math/lp/nla_core.h b/src/math/lp/nla_core.h index 6b0e71537..09bc44e91 100644 --- a/src/math/lp/nla_core.h +++ b/src/math/lp/nla_core.h @@ -229,8 +229,12 @@ public: lpvar var(const factor& f) const { return f.var(); } // returns true if the combination of the Horner's schema and Grobner Basis should be called - bool need_to_call_algebraic_methods() const { - return lp_settings().stats().m_nla_calls % m_nla_settings.horner_frequency() == 0; + bool need_run_horner() const { + return m_nla_settings.run_horner() && lp_settings().stats().m_nla_calls % m_nla_settings.horner_frequency() == 0; + } + + bool need_run_grobner() const { + return m_nla_settings.run_grobner() && lp_settings().stats().m_nla_calls % m_nla_settings.grobner_frequency() == 0; } void incremental_linearization(bool); diff --git a/src/math/lp/nla_settings.h b/src/math/lp/nla_settings.h index e51dc19e0..606f69088 100644 --- a/src/math/lp/nla_settings.h +++ b/src/math/lp/nla_settings.h @@ -28,7 +28,10 @@ class nla_settings { unsigned m_grobner_max_simplified; unsigned m_grobner_number_of_conflicts_to_report; unsigned m_grobner_quota; + unsigned m_grobner_frequency; bool m_run_nra; + // propagate bounds + bool m_bp; public: nla_settings() : m_run_order(true), m_run_tangents(true), @@ -40,8 +43,12 @@ public: m_grobner_row_length_limit(50), m_grobner_subs_fixed(false), m_grobner_quota(0), - m_run_nra(false) + m_grobner_frequency(4), + m_run_nra(false), + m_bp(false) {} + bool propagate_bounds() const { return m_bp; } + bool& propagate_bounds() { return m_bp; } 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; } @@ -62,6 +69,8 @@ public: bool run_grobner() const { return m_run_grobner; } bool& run_grobner() { return m_run_grobner; } + unsigned grobner_frequency() const { return m_grobner_frequency; } + unsigned& grobner_frequency() { return m_grobner_frequency; } bool run_nra() const { return m_run_nra; } bool& run_nra() { return m_run_nra; } diff --git a/src/smt/params/smt_params_helper.pyg b/src/smt/params/smt_params_helper.pyg index 9359ceed3..6cbbf77fb 100644 --- a/src/smt/params/smt_params_helper.pyg +++ b/src/smt/params/smt_params_helper.pyg @@ -48,11 +48,13 @@ def_module_params(module_name='smt', ('arith.nl.branching', BOOL, True, 'branching on integer variables in non linear clusters, relevant only if smt.arith.solver=2'), ('arith.nl.rounds', UINT, 1024, 'threshold for number of (nested) final checks for non linear arithmetic, relevant only if smt.arith.solver=2'), ('arith.nl.order', BOOL, True, 'run order lemmas'), + ('arith.nl.bp', BOOL, False, 'propagate bounds on monomials'), ('arith.nl.tangents', BOOL, True, 'run tangent lemmas'), ('arith.nl.horner', BOOL, True, 'run horner\'s heuristic'), ('arith.nl.horner_subs_fixed', UINT, 2, '0 - no subs, 1 - substitute, 2 - substitute fixed zeros only'), ('arith.nl.horner_frequency', UINT, 4, 'horner\'s call frequency'), ('arith.nl.horner_row_length_limit', UINT, 10, 'row is disregarded by the heuristic if its length is longer than the value'), + ('arith.nl.grobner_frequency', UINT, 4, 'grobner\'s call frequency'), ('arith.nl.grobner', BOOL, True, 'run grobner\'s basis heuristic'), ('arith.nl.grobner_eqs_growth', UINT, 10, 'grobner\'s number of equalities growth '), ('arith.nl.grobner_expr_size_growth', UINT, 2, 'grobner\'s maximum expr size growth'), diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index 26d7bb9fa..ee0c05afc 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -411,7 +411,9 @@ class theory_lra::imp { m_nla->settings().grobner_expr_degree_growth() = prms.arith_nl_grobner_expr_degree_growth(); m_nla->settings().grobner_max_simplified() = prms.arith_nl_grobner_max_simplified(); m_nla->settings().grobner_number_of_conflicts_to_report() = prms.arith_nl_grobner_cnfl_to_report(); - m_nla->settings().grobner_quota() = prms.arith_nl_gr_q(); + m_nla->settings().grobner_quota() = prms.arith_nl_gr_q(); + m_nla->settings().grobner_frequency() = prms.arith_nl_grobner_frequency(); + m_nla->settings().propagate_bounds() = prms.arith_nl_bp(); } }