mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-22 22:03:39 +00:00
Code Activity

experiment with substituting zeros in Horner&Grobner

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2020-01-11 15:43:54 -08:00
parent 45c0f2225c
commit f0b530b0e4
4 changed files with 26 additions and 12 deletions
Download patch file Download diff file Expand all files Collapse all files

12
src/math/lp/nla_common.cpp
View file

@ -125,9 +125,13 @@ unsigned common::random() {
// creates a nex expression for the coeff and var, // creates a nex expression for the coeff and var,
nex * common::nexvar(const rational & coeff, lpvar j, nex_creator& cn) { nex * common::nexvar(const rational & coeff, lpvar j, nex_creator& cn) {
SASSERT(!coeff.is_zero()); 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); 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)) { if (!c().is_monic_var(j)) {
c().insert_to_active_var_set(j); c().insert_to_active_var_set(j);
return cn.mk_mul(cn.mk_scalar(coeff), cn.mk_var(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()) { for (lpvar k : m.vars()) {
if (c().m_nla_settings.horner_subs_fixed() && c().var_is_fixed(k)) { if (c().m_nla_settings.horner_subs_fixed() && c().var_is_fixed(k)) {
mf *= c().m_lar_solver.column_lower_bound(k).x; 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); c().insert_to_active_var_set(k);
mf *= cn.mk_var(k); mf *= cn.mk_var(k);
CTRACE("nla_grobner", c().is_monic_var(k), c().print_var(k, tout) << "\n";); CTRACE("nla_grobner", c().is_monic_var(k), c().print_var(k, tout) << "\n";);

8
src/math/lp/nla_core.cpp
View file

@ -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) { 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)); 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)) if (!is_monic_var(j))
return c * m_pdd_manager.mk_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()) { for (lpvar k : m.vars()) {
if (m_nla_settings.grobner_subs_fixed() && var_is_fixed(k)) { 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)); 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 { } else {
r *= m_pdd_manager.mk_var(k); r *= m_pdd_manager.mk_var(k);
} }

4
src/math/lp/nla_params.pyg
View file

@ -4,7 +4,7 @@ def_module_params('nla',
('order', BOOL, True, 'run order lemmas'), ('order', BOOL, True, 'run order lemmas'),
('tangents', BOOL, True, 'run tangent lemmas'), ('tangents', BOOL, True, 'run tangent lemmas'),
('horner', BOOL, True, 'run horner\'s heuristic'), ('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_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'), ('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', 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_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_cnfl_to_report', UINT, 1, 'grobner\'s maximum number of conflicts to report'),
('gr_q', UINT, 8, 'grobner\'s quota'), ('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')
)) ))

14
src/math/lp/nla_settings.h
View file

@ -27,11 +27,11 @@ class nla_settings {
// how often to call the horner heuristic // how often to call the horner heuristic
unsigned m_horner_frequency; unsigned m_horner_frequency;
unsigned m_horner_row_length_limit; unsigned m_horner_row_length_limit;
bool m_horner_subs_fixed; unsigned m_horner_subs_fixed;
// grobner fields // grobner fields
bool m_run_grobner; bool m_run_grobner;
unsigned m_grobner_row_length_limit; unsigned m_grobner_row_length_limit;
bool m_grobner_subs_fixed; unsigned m_grobner_subs_fixed;
unsigned m_grobner_eqs_growth; unsigned m_grobner_eqs_growth;
unsigned m_grobner_tree_size_growth; unsigned m_grobner_tree_size_growth;
unsigned m_grobner_expr_size_growth; unsigned m_grobner_expr_size_growth;
@ -44,7 +44,7 @@ public:
m_run_horner(true), m_run_horner(true),
m_horner_frequency(4), m_horner_frequency(4),
m_horner_row_length_limit(10), m_horner_row_length_limit(10),
m_horner_subs_fixed(true), m_horner_subs_fixed(2),
m_run_grobner(true), m_run_grobner(true),
m_grobner_row_length_limit(50), m_grobner_row_length_limit(50),
m_grobner_subs_fixed(false) m_grobner_subs_fixed(false)
@ -64,16 +64,16 @@ public:
unsigned& horner_frequency() { return m_horner_frequency; } unsigned& horner_frequency() { return m_horner_frequency; }
unsigned horner_row_length_limit() const { return m_horner_row_length_limit; } unsigned horner_row_length_limit() const { return m_horner_row_length_limit; }
unsigned& horner_row_length_limit() { 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; } unsigned horner_subs_fixed() const { return m_horner_subs_fixed; }
bool& horner_subs_fixed() { 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() const { return m_run_grobner; }
bool& run_grobner() { 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() const { return m_grobner_row_length_limit; }
unsigned& grobner_row_length_limit() { 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; } unsigned grobner_subs_fixed() const { return m_grobner_subs_fixed; }
bool& grobner_subs_fixed() { 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() const { return m_grobner_tree_size_growth; }
unsigned & grobner_tree_size_growth() { return m_grobner_tree_size_growth; } unsigned & grobner_tree_size_growth() { return m_grobner_tree_size_growth; }