From 26956cafb088c4743da2f505a8284e2c1550a109 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Mon, 16 Dec 2019 11:24:14 -1000 Subject: [PATCH] limit the size of expressions in Grobner Signed-off-by: Lev Nachmanson --- src/math/lp/nla_grobner.cpp | 33 ++++++++++++++++++++------------- src/math/lp/nla_grobner.h | 10 ++++++---- src/math/lp/nla_settings.h | 6 +++--- 3 files changed, 29 insertions(+), 20 deletions(-) diff --git a/src/math/lp/nla_grobner.cpp b/src/math/lp/nla_grobner.cpp index 7b076f378..3ed157190 100644 --- a/src/math/lp/nla_grobner.cpp +++ b/src/math/lp/nla_grobner.cpp @@ -27,7 +27,7 @@ grobner::grobner(core *c, intervals *s) m_gc(m_nex_creator, c->m_reslim, c->m_nla_settings.grobner_eqs_threshold(), - c->m_nla_settings.grobner_superposed_expr_size_limit() + c->m_nla_settings.grobner_expr_size_limit() ), m_look_for_fixed_vars_in_rows(false) { std::function de; @@ -205,12 +205,19 @@ bool grobner_core::compute_basis_step() { } m_stats.m_compute_steps++; simplify_using_to_superpose(*eq); + if (equation_is_too_complex(eq)) + return false; if (!canceled() && simplify_to_superpose_with_eq(eq)) { TRACE("grobner", tout << "eq = "; display_equation(tout, *eq);); superpose(eq); - insert_to_superpose(eq); - simplify_m_to_simplify(eq); - TRACE("grobner", tout << "end of iteration:\n"; display(tout);); + if (equation_is_too_complex(eq)) { + TRACE("grobner", display_equation(tout, *eq) << " is too complex: deleting it\n;";); + del_equation(eq); + } else { + insert_to_superpose(eq); + simplify_m_to_simplify(eq); + TRACE("grobner", tout << "end of iteration:\n"; display(tout);); + } } return false; } @@ -486,7 +493,9 @@ void grobner_core::simplify_target_monomials_sum_j(equation const& source, equat bool grobner_core::simplify_source_target(equation const& source, equation& target) { TRACE("grobner", tout << "simplifying: "; display_equation(tout, target); tout << "\nusing: "; display_equation(tout, source);); TRACE("grobner_d", tout << "simplifying: " << *(target.expr()) << " using " << *(source.expr()) << "\n";); - SASSERT(m_nex_creator.is_simplified(*source.expr())); + SASSERT(m_nex_creator.is_simplified(*source.expr()) && !equation_is_too_complex(&source)); + if (equation_is_too_complex(&target)) + return false; SASSERT(m_nex_creator.is_simplified(*target.expr())); if (target.expr()->is_scalar()) { TRACE("grobner_d", tout << "no simplification\n";); @@ -514,7 +523,7 @@ bool grobner_core::simplify_source_target(equation const& source, equation& targ } void grobner_core::process_simplified_target(equation* target, ptr_buffer& to_remove) { - if (is_trivial(target)) { + if (is_trivial(target) || equation_is_too_complex(target)) { to_remove.push_back(target); } else if (m_changed_leading_term) { insert_to_simplify(target); @@ -525,8 +534,7 @@ void grobner_core::process_simplified_target(equation* target, ptr_bufferexp " << *(eq->expr()) << "\n";); - - ptr_buffer to_insert; + SASSERT(!equation_is_too_complex(eq)); ptr_buffer to_remove; ptr_buffer to_delete; for (equation * target : m_to_superpose) { @@ -537,15 +545,14 @@ bool grobner_core::simplify_to_superpose_with_eq(equation* eq) { if (simplify_source_target(*eq, *target)) { process_simplified_target(target, to_remove); } - if (is_trivial(target)) { + if (is_trivial(target)||equation_is_too_complex(target)) { to_delete.push_back(target); } else { SASSERT(m_nex_creator.is_simplified(*target->expr())); } } - for (equation* eq : to_insert) - insert_to_superpose(eq); + for (equation* eq : to_remove) m_to_superpose.erase(eq); for (equation* eq : to_delete) @@ -560,7 +567,7 @@ void grobner_core::simplify_m_to_simplify(equation* eq) { TRACE("grobner_d", tout << "eq->exp " << *(eq->expr()) << "\n";); ptr_buffer to_delete; for (equation* target : m_to_simplify) { - if (simplify_source_target(*eq, *target) && is_trivial(target)) + if (simplify_source_target(*eq, *target) && (is_trivial(target) || equation_is_too_complex(target))) to_delete.push_back(target); } for (equation* eq : to_delete) @@ -613,7 +620,7 @@ void grobner_core::superpose(equation * eq1, equation * eq2) { TRACE("grobner_d", tout << "eq1="; display_equation(tout, *eq1) << "eq2="; display_equation(tout, *eq2);); init_equation(eq, expr_superpose(eq1->expr(), eq2->expr(), ab, ac, b, c), m_dep_manager.mk_join(eq1->dep(), eq2->dep())); if (m_nex_creator.gt(eq->expr(), eq1->expr()) || m_nex_creator.gt(eq->expr(), eq2->expr()) || - eq->expr()->size() > m_superposed_exp_size_limit) { + equation_is_too_complex(eq)) { TRACE("grobner", display_equation(tout, *eq) << " is too complex: deleting it\n;";); del_equation(eq); } else { diff --git a/src/math/lp/nla_grobner.h b/src/math/lp/nla_grobner.h index 2d968b234..d7ae2bf71 100644 --- a/src/math/lp/nla_grobner.h +++ b/src/math/lp/nla_grobner.h @@ -89,15 +89,15 @@ private: bool m_changed_leading_term; equation_set m_all_eqs; unsigned m_grobner_eqs_threshold; - unsigned m_superposed_exp_size_limit; + unsigned m_expr_size_limit; public: - grobner_core(nex_creator& nc, reslimit& lim, unsigned eqs_threshold, unsigned superposed_expr_size_limit) : + grobner_core(nex_creator& nc, reslimit& lim, unsigned eqs_threshold, unsigned expr_size_limit) : m_nex_creator(nc), m_limit(lim), m_dep_manager(m_val_manager, m_alloc), m_changed_leading_term(false), m_grobner_eqs_threshold(eqs_threshold), - m_superposed_exp_size_limit(superposed_expr_size_limit) + m_expr_size_limit(expr_size_limit) {} ~grobner_core(); @@ -159,7 +159,9 @@ private: std::ostream& print_stats(std::ostream&) const; std::ostream& display_dependency(std::ostream& out, common::ci_dependency*) const; - + bool equation_is_too_complex(const equation* eq) const { + return eq->expr()->size() > m_expr_size_limit; + } #ifdef Z3DEBUG bool test_find_b_c(const nex* ab, const nex* ac, const nex_mul* b, const nex_mul* c); bool test_find_b(const nex* ab, const nex_mul* b); diff --git a/src/math/lp/nla_settings.h b/src/math/lp/nla_settings.h index e2ebe96bb..f4debc0c4 100644 --- a/src/math/lp/nla_settings.h +++ b/src/math/lp/nla_settings.h @@ -32,7 +32,7 @@ class nla_settings { unsigned m_grobner_frequency; unsigned m_grobner_eqs_threshold; unsigned m_grobner_row_length_limit; - unsigned m_grobner_superposed_expr_size_limit; + unsigned m_grobner_expr_size_limit; public: nla_settings() : m_run_order(true), @@ -44,7 +44,7 @@ public: m_grobner_frequency(5), m_grobner_eqs_threshold(512), m_grobner_row_length_limit(10), - m_grobner_superposed_expr_size_limit(50) + m_grobner_expr_size_limit(50) {} unsigned grobner_eqs_threshold() const { return m_grobner_eqs_threshold; } @@ -70,6 +70,6 @@ public: unsigned grobner_frequency() const { return m_grobner_frequency; } unsigned& grobner_frequency() { return m_grobner_frequency; } unsigned grobner_row_length_limit() const { return m_grobner_row_length_limit; } - unsigned grobner_superposed_expr_size_limit() const { return m_grobner_superposed_expr_size_limit; } + unsigned grobner_expr_size_limit() const { return m_grobner_expr_size_limit; } }; }