From f0b530b0e40ee60270e4551487d67b23f5c150fa Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Sat, 11 Jan 2020 15:43:54 -0800 Subject: [PATCH] experiment with substituting zeros in Horner&Grobner Signed-off-by: Lev Nachmanson --- src/math/lp/nla_common.cpp | 12 ++++++++++-- src/math/lp/nla_core.cpp | 8 +++++++- src/math/lp/nla_params.pyg | 4 ++-- src/math/lp/nla_settings.h | 14 +++++++------- 4 files changed, 26 insertions(+), 12 deletions(-) diff --git a/src/math/lp/nla_common.cpp b/src/math/lp/nla_common.cpp index 0bcddb930..a76ca57e3 100644 --- a/src/math/lp/nla_common.cpp +++ b/src/math/lp/nla_common.cpp @@ -125,9 +125,13 @@ unsigned common::random() { // creates a nex expression for the coeff and var, nex * common::nexvar(const rational & coeff, lpvar j, nex_creator& cn) { SASSERT(!coeff.is_zero()); - if (c().m_nla_settings.horner_subs_fixed() && c().var_is_fixed(j)) { + if (c().m_nla_settings.horner_subs_fixed() == 1 && c().var_is_fixed(j)) { return cn.mk_scalar(coeff * c().m_lar_solver.column_lower_bound(j).x); } + if (c().m_nla_settings.horner_subs_fixed() == 2 && c().var_is_fixed_to_zero(j)) { + return cn.mk_scalar(rational(0)); + } + if (!c().is_monic_var(j)) { c().insert_to_active_var_set(j); return cn.mk_mul(cn.mk_scalar(coeff), cn.mk_var(j)); @@ -138,7 +142,11 @@ nex * common::nexvar(const rational & coeff, lpvar j, nex_creator& cn) { for (lpvar k : m.vars()) { if (c().m_nla_settings.horner_subs_fixed() && c().var_is_fixed(k)) { mf *= c().m_lar_solver.column_lower_bound(k).x; - } else { + } else if (c().m_nla_settings.horner_subs_fixed() == 2 && + c().var_is_fixed_to_zero(j)) { + return cn.mk_scalar(rational(0)); + } + else { c().insert_to_active_var_set(k); mf *= cn.mk_var(k); CTRACE("nla_grobner", c().is_monic_var(k), c().print_var(k, tout) << "\n";); diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp index b2bf682ff..0fea75e64 100644 --- a/src/math/lp/nla_core.cpp +++ b/src/math/lp/nla_core.cpp @@ -1553,10 +1553,14 @@ const rational& core::val_of_fixed_var_with_deps(lpvar j, u_dependency*& dep) { } dd::pdd core::pdd_expr(const rational& c, lpvar j, u_dependency*& dep) { - if (m_nla_settings.grobner_subs_fixed() && var_is_fixed(j)) { + if (m_nla_settings.grobner_subs_fixed() == 1 && var_is_fixed(j)) { return m_pdd_manager.mk_val(c * val_of_fixed_var_with_deps(j, dep)); } + if (m_nla_settings.grobner_subs_fixed() == 2 && var_is_fixed_to_zero(j)) { + return m_pdd_manager.mk_val(val_of_fixed_var_with_deps(j, dep)); + } + if (!is_monic_var(j)) return c * m_pdd_manager.mk_var(j); @@ -1566,6 +1570,8 @@ dd::pdd core::pdd_expr(const rational& c, lpvar j, u_dependency*& dep) { for (lpvar k : m.vars()) { if (m_nla_settings.grobner_subs_fixed() && var_is_fixed(k)) { r *= m_pdd_manager.mk_val(val_of_fixed_var_with_deps(k, dep)); + } else if (m_nla_settings.grobner_subs_fixed() == 2 && var_is_fixed_to_zero(k)) { + return m_pdd_manager.mk_val(val_of_fixed_var_with_deps(k, dep)); } else { r *= m_pdd_manager.mk_var(k); } diff --git a/src/math/lp/nla_params.pyg b/src/math/lp/nla_params.pyg index 1098bd586..b141c8cb1 100644 --- a/src/math/lp/nla_params.pyg +++ b/src/math/lp/nla_params.pyg @@ -4,7 +4,7 @@ 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, False, 'substitute fixed variables by constants'), + ('horner_subs_fixed', UINT, 2, '0 - no subs, 1 - substitute, 2 - substitute fixed zeros only'), ('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'), @@ -14,7 +14,7 @@ def_module_params('nla', ('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'), ('gr_q', UINT, 8, 'grobner\'s quota'), - ('grobner_subs_fixed', BOOL, False, 'substitute fixed variables by constants') + ('grobner_subs_fixed', UINT, 2, '0 - no subs, 1 - substitute, 2 - substitute fixed zeros only') )) diff --git a/src/math/lp/nla_settings.h b/src/math/lp/nla_settings.h index cf63bb9dd..418c23599 100644 --- a/src/math/lp/nla_settings.h +++ b/src/math/lp/nla_settings.h @@ -27,11 +27,11 @@ class nla_settings { // how often to call the horner heuristic unsigned m_horner_frequency; unsigned m_horner_row_length_limit; - bool m_horner_subs_fixed; + unsigned m_horner_subs_fixed; // grobner fields bool m_run_grobner; unsigned m_grobner_row_length_limit; - bool m_grobner_subs_fixed; + unsigned m_grobner_subs_fixed; unsigned m_grobner_eqs_growth; unsigned m_grobner_tree_size_growth; unsigned m_grobner_expr_size_growth; @@ -44,7 +44,7 @@ public: m_run_horner(true), m_horner_frequency(4), m_horner_row_length_limit(10), - m_horner_subs_fixed(true), + m_horner_subs_fixed(2), m_run_grobner(true), m_grobner_row_length_limit(50), m_grobner_subs_fixed(false) @@ -64,16 +64,16 @@ public: unsigned& horner_frequency() { return m_horner_frequency; } unsigned horner_row_length_limit() const { return m_horner_row_length_limit; } unsigned& horner_row_length_limit() { return m_horner_row_length_limit; } - bool horner_subs_fixed() const { return m_horner_subs_fixed; } - bool& horner_subs_fixed() { return m_horner_subs_fixed; } + unsigned horner_subs_fixed() const { return m_horner_subs_fixed; } + unsigned& horner_subs_fixed() { return m_horner_subs_fixed; } bool run_grobner() const { return m_run_grobner; } bool& run_grobner() { return m_run_grobner; } unsigned grobner_row_length_limit() const { return m_grobner_row_length_limit; } 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_subs_fixed() const { return m_grobner_subs_fixed; } + unsigned& 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; }