mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-31 03:32:28 +00:00
Code Activity

add complexity throttle

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-12-18 14:31:31 -08:00
parent f5164d166b
commit 1287572f4f
2 changed files with 6 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/math/grobner/pdd_grobner.cpp
View file

@ -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);

3
src/math/grobner/pdd_grobner.h
View file

@ -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);