From 1287572f4f87e39df21ee9e34e270002f501f4c4 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 18 Dec 2019 14:31:31 -0800 Subject: [PATCH] add complexity throttle Signed-off-by: Nikolaj Bjorner --- src/math/grobner/pdd_grobner.cpp | 3 +++ src/math/grobner/pdd_grobner.h | 3 +++ 2 files changed, 6 insertions(+) diff --git a/src/math/grobner/pdd_grobner.cpp b/src/math/grobner/pdd_grobner.cpp index d1ef03533..aee5e8535 100644 --- a/src/math/grobner/pdd_grobner.cpp +++ b/src/math/grobner/pdd_grobner.cpp @@ -126,6 +126,8 @@ namespace dd { if (simplify_source_target(eq, *target, changed_leading_term)) { if (is_trivial(*target)) to_delete.push_back(target); + else if (is_too_complex(*target)) + to_delete.push_back(target); else if (check_conflict(*target)) return false; else if (changed_leading_term && target->is_processed()) { @@ -170,6 +172,7 @@ namespace dd { if (!m.try_spoly(eq1.poly(), eq2.poly(), r)) return; m_stats.m_superposed++; if (r.is_zero()) return; + if (is_too_complex(r)) return; equation* eq = alloc(equation, r, m_dep_manager.mk_join(eq1.dep(), eq2.dep()), m_equations.size()); m_equations.push_back(eq); update_stats_max_degree_and_size(*eq); diff --git a/src/math/grobner/pdd_grobner.h b/src/math/grobner/pdd_grobner.h index bdf123369..f89f54e83 100644 --- a/src/math/grobner/pdd_grobner.h +++ b/src/math/grobner/pdd_grobner.h @@ -119,6 +119,9 @@ private: bool is_simpler(equation const& eq1, equation const& eq2) { return eq1.poly() < eq2.poly(); } bool check_conflict(equation const& eq) { return eq.poly().is_val() && !is_trivial(eq) && (set_conflict(), true); } void set_conflict() { m_conflict = true; } + bool is_too_complex(const equation& eq) const { return is_too_complex(eq.poly()); } + bool is_too_complex(const pdd& p) const { return p.tree_size() > m_config.m_expr_size_limit; } + void del_equations(unsigned old_size); void del_equation(equation* eq);