From 0535e24dd1e710480889ed4af37f9fa898a8af37 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 17 Dec 2019 08:24:30 -0800 Subject: [PATCH] consolidate parameters, add comment (#102) * updates Signed-off-by: Nikolaj Bjorner * code review of nla_intervals: combine functionality Signed-off-by: Nikolaj Bjorner * tidy Signed-off-by: Nikolaj Bjorner * formatting Signed-off-by: Nikolaj Bjorner * add comments Signed-off-by: Nikolaj Bjorner * merge issue Signed-off-by: Nikolaj Bjorner * tired of looking at compiler warning Signed-off-by: Nikolaj Bjorner --- src/math/lp/nla_grobner.cpp | 96 ++++++++++++++++++++--------------- src/math/lp/nla_grobner.h | 18 ++++--- src/math/lp/nla_intervals.cpp | 1 + src/math/lp/nla_intervals.h | 3 ++ src/smt/theory_lra.cpp | 2 +- 5 files changed, 72 insertions(+), 48 deletions(-) diff --git a/src/math/lp/nla_grobner.cpp b/src/math/lp/nla_grobner.cpp index cc469ea23..29ee6047b 100644 --- a/src/math/lp/nla_grobner.cpp +++ b/src/math/lp/nla_grobner.cpp @@ -24,15 +24,15 @@ using namespace nla; grobner::grobner(core *c, intervals *s) : common(c, s), - m_gc(m_nex_creator, - c->m_reslim, - c->m_nla_settings.grobner_eqs_threshold(), - c->m_nla_settings.grobner_expr_size_limit() - ), + m_gc(m_nex_creator, c->m_reslim), m_look_for_fixed_vars_in_rows(false) { std::function de; de = [this](lp::explanation const& e, std::ostream& out) { m_core->print_explanation(e, out); }; + grobner_core::params p; + p.m_expr_size_limit = c->m_nla_settings.grobner_expr_size_limit(); + p.m_grobner_eqs_threshold = c->m_nla_settings.grobner_eqs_threshold(); m_gc = de; + m_gc = p; } void grobner::grobner_lemmas() { @@ -183,6 +183,22 @@ void grobner::add_row(unsigned i) { /// ------------------------------- /// grobner_core +/*** +The main algorithm maintains two sets (S, A), +where S is m_to_superpose, and A is m_to_simplify. +Initially S is empty and A contains the initial equations. + +Each step proceeds as follows: + - pick a in A, and remove a from A + - simplify a using S + - simplify S using a + - for s in S: + b = superpose(a, s) + add b to A + - add a to S + - simplify A using a +*/ + bool grobner_core::compute_basis_loop() { while (!done()) { if (compute_basis_step()) { @@ -205,20 +221,22 @@ 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); - 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);); - } + if (!simplify_to_superpose_with_eq(eq)) { + return false; } + TRACE("grobner", tout << "eq = "; display_equation(tout, *eq);); + superpose(eq); + if (equation_is_too_complex(eq)) { + TRACE("grobner", display_equation(tout, *eq) << " is too complex: deleting it\n;";); + del_equation(eq); + return false; + } + insert_to_superpose(eq); + simplify_m_to_simplify(eq); + TRACE("grobner", tout << "end of iteration:\n"; display(tout);); return false; } @@ -241,6 +259,26 @@ grobner_core::equation* grobner_core::pick_next() { return r; } +void grobner_core::simplify_using_to_superpose(equation& eq) { + bool simplified; + TRACE("grobner", tout << "simplifying: "; display_equation(tout, eq); tout << "using equalities of m_to_superpose of size " << m_to_superpose.size() << "\n";); + do { + simplified = false; + for (equation* p : m_to_superpose) { + if (simplify_source_target(*p, eq)) { + simplified = true; + } + if (canceled() || eq.expr()->is_scalar()) { + break; + } + } + } while (simplified && !eq.expr()->is_scalar()); + + TRACE("grobner", + if (simplified) { tout << "simplification result: "; display_equation(tout, eq); } + else { tout << "no simplification\n"; }); +} + grobner_core::equation_set const& grobner_core::equations() { m_all_eqs.reset(); for (auto e : m_to_simplify) m_all_eqs.insert(e); @@ -279,29 +317,7 @@ void grobner_core::del_equation(equation * eq) { SASSERT(m_equations_to_delete[eq->m_bidx] == eq); m_equations_to_delete[eq->m_bidx] = nullptr; dealloc(eq); -} - -void grobner_core::simplify_using_to_superpose(equation& eq) { - bool simplified; - TRACE("grobner", tout << "simplifying: "; display_equation(tout, eq); tout << "using equalities of m_to_superpose of size " << m_to_superpose.size() << "\n";); - do { - simplified = false; - for (equation* p : m_to_superpose) { - if (simplify_source_target(*p, eq)) { - simplified = true; - } - if (canceled() || eq.expr()->is_scalar()) { - break; - } - } - } - while (simplified && !eq.expr()->is_scalar()); - - TRACE("grobner", - if (simplified) { tout << "simplification result: "; display_equation(tout, eq);} - else {tout << "no simplification\n";}); -} - +} const nex* grobner_core::get_highest_monomial(const nex* e) const { switch (e->type()) { @@ -725,7 +741,7 @@ bool grobner_core::canceled() { } bool grobner_core::done() { - return num_of_equations() >= m_grobner_eqs_threshold || canceled(); + return num_of_equations() >= m_params.m_grobner_eqs_threshold || canceled(); } void grobner_core::del_equations(unsigned old_size) { diff --git a/src/math/lp/nla_grobner.h b/src/math/lp/nla_grobner.h index d7ae2bf71..72cb887d1 100644 --- a/src/math/lp/nla_grobner.h +++ b/src/math/lp/nla_grobner.h @@ -38,6 +38,11 @@ struct grobner_stats { class grobner_core { public: + struct params { + unsigned m_grobner_eqs_threshold; + unsigned m_expr_size_limit; + }; + class equation { unsigned m_bidx; //!< position at m_equations_to_delete nex * m_expr; // simplified expressionted monomials @@ -88,16 +93,14 @@ private: nex_lt m_lt; bool m_changed_leading_term; equation_set m_all_eqs; - unsigned m_grobner_eqs_threshold; - unsigned m_expr_size_limit; + params m_params; + public: - grobner_core(nex_creator& nc, reslimit& lim, unsigned eqs_threshold, unsigned expr_size_limit) : + grobner_core(nex_creator& nc, reslimit& lim) : 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_expr_size_limit(expr_size_limit) + m_changed_leading_term(false) {} ~grobner_core(); @@ -112,6 +115,7 @@ public: std::ostream& display(std::ostream& out) const; void operator=(print_expl_t& pe) { m_print_explanation = pe; } + void operator=(params const& p) { m_params = p; } private: bool compute_basis_step(); @@ -160,7 +164,7 @@ 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; + return eq->expr()->size() > m_params.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); diff --git a/src/math/lp/nla_intervals.cpp b/src/math/lp/nla_intervals.cpp index 7cdf9cb2e..4a0f7c4f9 100644 --- a/src/math/lp/nla_intervals.cpp +++ b/src/math/lp/nla_intervals.cpp @@ -5,6 +5,7 @@ namespace nla { + typedef intervals::interval interv; typedef enum intervals::with_deps_t e_with_deps; diff --git a/src/math/lp/nla_intervals.h b/src/math/lp/nla_intervals.h index 82d07b104..3bef696d8 100644 --- a/src/math/lp/nla_intervals.h +++ b/src/math/lp/nla_intervals.h @@ -293,6 +293,7 @@ public: if (wd == with_deps) { i.m_lower_dep = a.m_lower_dep; } + } template @@ -313,8 +314,10 @@ public: } template + bool interval_from_term(const nex& e, interval& i) const; + template interval interval_of_sum_no_term(const nex_sum& e); diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index 724e6da01..ef2ace2af 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -2171,7 +2171,7 @@ public: for(const nla::lemma & l : lv) { m_lemma = l; //todo avoid the copy m_explanation = l.expl(); - m_stats.m_nla_explanations += l.expl().size(); + m_stats.m_nla_explanations += static_cast(l.expl().size()); false_case_of_check_nla(); } break;