From 48f7e69d0e3d06db65bebee9d7b969a0f5fc8fdc Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Wed, 18 Dec 2019 08:14:18 -1000 Subject: [PATCH] only run grobner when horner fails, introduce concat instead copy Signed-off-by: Lev Nachmanson --- src/math/lp/horner.cpp | 12 +++++++----- src/math/lp/horner.h | 2 +- src/math/lp/nla_core.cpp | 9 +++++---- src/math/lp/nla_core.h | 12 ++++++------ src/math/lp/nla_grobner.cpp | 21 ++++++++++++--------- src/math/lp/nla_grobner.h | 35 +++++++++++++++++++++++++++++++++-- src/math/lp/nla_settings.h | 2 -- src/smt/theory_lra.cpp | 1 - 8 files changed, 64 insertions(+), 30 deletions(-) diff --git a/src/math/lp/horner.cpp b/src/math/lp/horner.cpp index 7b968e236..fdb710f02 100644 --- a/src/math/lp/horner.cpp +++ b/src/math/lp/horner.cpp @@ -90,15 +90,15 @@ bool horner::lemmas_on_row(const T& row) { return lemmas_on_expr(cn, to_sum(e)); } -void horner::horner_lemmas() { +bool horner::horner_lemmas() { if (!c().m_nla_settings.run_horner()) { TRACE("nla_solver", tout << "not generating horner lemmas\n";); - return; + return false; } c().lp_settings().stats().m_horner_calls++; const auto& matrix = c().m_lar_solver.A_r(); // choose only rows that depend on m_to_refine variables - std::set rows_to_check; // we need it to be determenistic: cannot work with the unordered_set + std::set rows_to_check; for (lpvar j : c().m_to_refine) { for (auto & s : matrix.m_columns[j]) rows_to_check.insert(s.var()); @@ -112,13 +112,15 @@ void horner::horner_lemmas() { unsigned r = c().random(); unsigned sz = rows.size(); - for (unsigned i = 0; i < sz; i++) { + bool conflict = false; + for (unsigned i = 0; i < sz && !conflict; i++) { m_row_index = rows[(i + r) % sz]; if (lemmas_on_row(matrix.m_rows[m_row_index])) { c().lp_settings().stats().m_horner_conflicts++; - break; + conflict = true; } } + return conflict; } } diff --git a/src/math/lp/horner.h b/src/math/lp/horner.h index ffb40877d..2328d1cd2 100644 --- a/src/math/lp/horner.h +++ b/src/math/lp/horner.h @@ -36,7 +36,7 @@ class horner : common { public: typedef intervals::interval interv; horner(core *core, intervals*); - void horner_lemmas(); + bool horner_lemmas(); template // T has an iterator of (coeff(), var()) bool lemmas_on_row(const T&); template bool row_is_interesting(const T&) const; diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp index d4c075b96..712704b6d 100644 --- a/src/math/lp/nla_core.cpp +++ b/src/math/lp/nla_core.cpp @@ -1280,10 +1280,11 @@ lbool core::incremental_linearization(bool constraint_derived) { // obtain the lemmas lbool core::inner_check(bool constraint_derived) { if (constraint_derived) { - if (need_to_call_horner()) - m_horner.horner_lemmas(); - else if (need_to_call_grobner()) - m_grobner.grobner_lemmas(); + if (need_to_call_algebraic_methods()) + if (!(m_nla_settings.run_horner() && m_horner.horner_lemmas())) { + if (m_nla_settings.run_grobner()) + m_grobner.grobner_lemmas(); + } if (done()) { return l_false; } diff --git a/src/math/lp/nla_core.h b/src/math/lp/nla_core.h index f5bd8d6d9..cfa643bb9 100644 --- a/src/math/lp/nla_core.h +++ b/src/math/lp/nla_core.h @@ -145,12 +145,12 @@ public: lpvar var(const factor& f) const { return f.var(); } - bool need_to_call_horner() const { return lp_settings().stats().m_nla_calls % m_nla_settings.horner_frequency() == 0; } - - bool need_to_call_grobner() const { - return m_nla_settings.run_grobner() && - lp_settings().stats().m_nla_calls % m_nla_settings.grobner_frequency() == 0; - } + // returns true if the combination of the Horner's schema and Grobner Basis should be called + bool need_to_call_algebraic_methods() const { + return + lp_settings().stats().m_nla_calls < 20 || + lp_settings().stats().m_nla_calls % m_nla_settings.horner_frequency() == 0; + } lbool incremental_linearization(bool); diff --git a/src/math/lp/nla_grobner.cpp b/src/math/lp/nla_grobner.cpp index 488e94eef..c552fbbe1 100644 --- a/src/math/lp/nla_grobner.cpp +++ b/src/math/lp/nla_grobner.cpp @@ -247,7 +247,7 @@ grobner_core::equation* grobner_core::pick_next() { if (is_trivial(curr)) to_delete.push_back(curr); else if (is_simpler(curr, r)) { - TRACE("grobner", tout << "preferring "; display_equation(tout, *curr);); + TRACE("grobner", tout << "preferring " << *(curr->expr()) << "\n";);; r = curr; } } @@ -255,7 +255,7 @@ grobner_core::equation* grobner_core::pick_next() { del_equation(e); if (r) m_to_simplify.erase(r); - TRACE("grobner", tout << "selected equation: "; if (!r) tout << "\n"; else display_equation(tout, *r);); + TRACE("grobner", tout << "selected equation: "; if (!r) tout << "\n"; else tout << *r->expr() << "\n";); return r; } @@ -279,11 +279,8 @@ void grobner_core::simplify_eq_by_using_to_superpose(equation& 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); - for (auto e : m_to_superpose) m_all_eqs.insert(e); - return m_all_eqs; +concat grobner_core::equations() { + return concat(m_to_superpose, m_to_simplify); } void grobner_core::reset() { @@ -778,14 +775,20 @@ void grobner_core::display_equations(std::ostream & out, equation_set const & v, display_equation(out, *e); } +void grobner_core::display_equations_no_deps(std::ostream & out, equation_set const & v, char const * header) const { + out << header << "\n"; + for (const equation* e : v) + out << *(e->expr()) << "\n"; +} + std::ostream& grobner_core::display_equation(std::ostream & out, const equation & eq) const { out << "expr = " << *eq.expr() << "\n"; return display_dependency(out, eq.dep()); } std::ostream& grobner_core::display(std::ostream& out) const { - display_equations(out, m_to_superpose, "m_to_superpose:"); - display_equations(out, m_to_simplify, "m_to_simplify:"); + display_equations_no_deps(out, m_to_superpose, "m_to_superpose:"); + display_equations_no_deps(out, m_to_simplify, "m_to_simplify:"); return out; } diff --git a/src/math/lp/nla_grobner.h b/src/math/lp/nla_grobner.h index d56abaa4f..8f8bba765 100644 --- a/src/math/lp/nla_grobner.h +++ b/src/math/lp/nla_grobner.h @@ -36,6 +36,37 @@ struct grobner_stats { grobner_stats() { reset(); } }; +template +class concat { + const A& m_a; // the first container + const B& m_b; // the second container +public: + class iterator { + const concat& m_c; + typename A::iterator m_a_it; + typename B::iterator m_b_it; + public: + iterator(const concat& c, bool begin): + m_c(c), m_a_it(begin? m_c.m_a.begin() : m_c.m_a.end()), m_b_it(begin? m_c.m_b.begin() : m_c.m_b.end()) {} + const C operator*() { return m_a_it != m_c.m_a.end() ? *m_a_it : *m_b_it; } + iterator& operator++() { + if (m_a_it != m_c.m_a.end()) + m_a_it++; + else + m_b_it++; + return *this; + } + iterator operator++(int) { iterator tmp = *this; ++*this; return tmp; } + bool operator==(iterator const& other) const { return m_a_it == other.m_a_it && m_b_it == other.m_b_it; } + bool operator!=(iterator const& other) const { return m_a_it != other.m_a_it || m_b_it != other.m_b_it; } + }; + + concat(const A& a, const B& b) : m_a(a), m_b(b) {} + iterator begin() { return iterator(*this, true); } + iterator end() { return iterator(*this, false); } + +}; + class grobner_core { public: struct params { @@ -92,7 +123,6 @@ private: mutable common::ci_dependency_manager m_dep_manager; nex_lt m_lt; bool m_changed_leading_term; - equation_set m_all_eqs; params m_params; public: @@ -107,9 +137,10 @@ public: void reset(); bool compute_basis_loop(); void assert_eq_0(nex*, common::ci_dependency * dep); - equation_set const& equations(); + concat equations(); common::ci_dependency_manager& dep() const { return m_dep_manager; } + void display_equations_no_deps(std::ostream& out, equation_set const& v, char const* header) const; void display_equations(std::ostream& out, equation_set const& v, char const* header) const; std::ostream& display_equation(std::ostream& out, const equation& eq) const; std::ostream& display(std::ostream& out) const; diff --git a/src/math/lp/nla_settings.h b/src/math/lp/nla_settings.h index f4debc0c4..772589a2d 100644 --- a/src/math/lp/nla_settings.h +++ b/src/math/lp/nla_settings.h @@ -67,8 +67,6 @@ public: bool run_grobner() const { return m_run_grobner; } bool& run_grobner() { return m_run_grobner; } - 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_expr_size_limit() const { return m_grobner_expr_size_limit; } }; diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index ef2ace2af..aa0e33119 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -453,7 +453,6 @@ class theory_lra::imp { m_nla->get_core()->m_nla_settings.run_horner() = nla.horner(); m_nla->get_core()->m_nla_settings.horner_frequency() = nla.horner_frequency(); m_nla->get_core()->m_nla_settings.horner_row_length_limit() = nla.horner_row_length_limit(); - m_nla->get_core()->m_nla_settings.grobner_frequency() = nla.grobner_frequency(); m_nla->get_core()->m_nla_settings.run_grobner() = nla.grobner(); m_nla->get_core()->m_nla_settings.grobner_eqs_threshold() = nla.grobner_eqs_threshold(); }