From aef26598e523fc0b287348417157069bb963f562 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Wed, 31 Jul 2019 12:12:30 -0700 Subject: [PATCH] fix choosing rows for horner's schem Signed-off-by: Lev Nachmanson --- src/math/lp/emonomials.cpp | 18 +++++++++--------- src/math/lp/horner.cpp | 15 ++++++++++++++- src/math/lp/horner.h | 3 +++ src/math/lp/nla_core.cpp | 6 +++--- src/math/lp/nla_intervals.cpp | 4 ++-- 5 files changed, 31 insertions(+), 15 deletions(-) diff --git a/src/math/lp/emonomials.cpp b/src/math/lp/emonomials.cpp index d7b464ce9..57c8659f1 100644 --- a/src/math/lp/emonomials.cpp +++ b/src/math/lp/emonomials.cpp @@ -173,7 +173,7 @@ void emonomials::remove_cg_mon(const monomial& m) { lpvar u = m.var(), w; // equivalence class of u: if (m_cg_table.find(u, w)) { - TRACE("nla_solver", tout << "erase << " << m << "\n";); + TRACE("nla_solver_mons", tout << "erase << " << m << "\n";); m_cg_table.erase(u); } } @@ -226,7 +226,7 @@ bool emonomials::elists_are_consistent(std::unordered_mapsecond != c, + CTRACE("nla_solver_mons", it->second != c, tout << "m = " << m << "\n"; tout << "c = " ; print_vector(c, tout); tout << "\n"; if (it == lists.end()) { @@ -249,7 +249,7 @@ void emonomials::insert_cg_mon(monomial & m) { lpvar v = m.var(), w; if (m_cg_table.find(v, w)) { if (v == w) { - TRACE("nla_solver", tout << "found " << v << "\n";); + TRACE("nla_solver_mons", tout << "found " << v << "\n";); return; } unsigned v_idx = m_var2index[v]; @@ -257,11 +257,11 @@ void emonomials::insert_cg_mon(monomial & m) { unsigned max_i = std::max(v_idx, w_idx); while (m_u_f.get_num_vars() <= max_i) m_u_f.mk_var(); - TRACE("nla_solver", tout << "merge " << v << " idx " << v_idx << ", and " << w << " idx " << w_idx << "\n";); + TRACE("nla_solver_mons", tout << "merge " << v << " idx " << v_idx << ", and " << w << " idx " << w_idx << "\n";); m_u_f.merge(v_idx, w_idx); } else { - TRACE("nla_solver", tout << "insert " << m << "\n";); + TRACE("nla_solver_mons", tout << "insert " << m << "\n";); m_cg_table.insert(v); } } @@ -282,7 +282,7 @@ bool emonomials::is_visited(monomial const& m) const { class of equal up-to var_eqs monomials. */ void emonomials::add(lpvar v, unsigned sz, lpvar const* vs) { - TRACE("nla_solver", tout << "v = " << v << "\n";); + TRACE("nla_solver_mons", tout << "v = " << v << "\n";); unsigned idx = m_monomials.size(); m_monomials.push_back(monomial(v, sz, vs, idx)); lpvar last_var = UINT_MAX; @@ -376,17 +376,17 @@ void emonomials::merge_eh(signed_var r2, signed_var r1, signed_var v2, signed_va } void emonomials::after_merge_eh(signed_var r2, signed_var r1, signed_var v2, signed_var v1) { - TRACE("nla_solver", tout << r2 << " <- " << r1 << "\n";); + TRACE("nla_solver_mons", tout << r2 << " <- " << r1 << "\n";); if (m_ve.find(~r1) == m_ve.find(~r2)) { // the other sign has also been merged m_use_lists.reserve(std::max(r2.var(), r1.var()) + 1); - TRACE("nla_solver", tout << "rehasing " << r1.var() << "\n";); + TRACE("nla_solver_mons", tout << "rehasing " << r1.var() << "\n";); merge_cells(m_use_lists[r2.var()], m_use_lists[r1.var()]); rehash_cg(r1.var()); } } void emonomials::unmerge_eh(signed_var r2, signed_var r1) { - TRACE("nla_solver", tout << r2 << " -> " << r1 << "\n";); + TRACE("nla_solver_mons", tout << r2 << " -> " << r1 << "\n";); if (m_ve.find(~r1) != m_ve.find(~r2)) { // the other sign has also been unmerged unmerge_cells(m_use_lists[r2.var()], m_use_lists[r1.var()]); rehash_cg(r1.var()); diff --git a/src/math/lp/horner.cpp b/src/math/lp/horner.cpp index e8ce097b8..f6b48cdd2 100644 --- a/src/math/lp/horner.cpp +++ b/src/math/lp/horner.cpp @@ -27,9 +27,20 @@ namespace nla { typedef intervals::interval interv; horner::horner(core * c) : common(c), m_intervals(c, c->reslim()) {} +template +bool horner::row_has_monomial_to_refine(const T& row) const { + for (const auto& p : row) { + if (c().m_to_refine.contains(p.var())) + return true; + } + return false; + +} // Returns true if the row has at least two monomials sharing a variable template bool horner::row_is_interesting(const T& row) const { + TRACE("nla_solver", m_core->print_term(row, tout);); + SASSERT(row_has_monomial_to_refine(row)); std::unordered_set seen; for (const auto& p : row) { lpvar j = p.var(); @@ -98,7 +109,8 @@ void horner::horner_lemmas() { unsigned r = c().random(); unsigned sz = rows.size(); for (unsigned i = 0; i < sz; i++) { - if (lemmas_on_row(matrix.m_rows[(i + r) % sz])) + unsigned row_index = rows[(i + r) % sz]; + if (lemmas_on_row(matrix.m_rows[row_index])) break; } } @@ -113,6 +125,7 @@ nex horner::nexvar(lpvar j) const { nex e(expr_type::MUL); for (lpvar k : m.vars()) { e.add_child(nex::var(k)); + CTRACE("nla_horner", c().is_monomial_var(k), c().print_var(k, tout) << "\n";); } return e; } diff --git a/src/math/lp/horner.h b/src/math/lp/horner.h index 48aa3080f..635e00756 100644 --- a/src/math/lp/horner.h +++ b/src/math/lp/horner.h @@ -46,5 +46,8 @@ public: void set_interval_for_scalar(intervals::interval&, const rational&); void set_var_interval(lpvar j, intervals::interval&); bool lemmas_on_expr(nex &); + + template // T has an iterator of (coeff(), var()) + bool row_has_monomial_to_refine(const T&) const; }; // end of horner } diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp index f6bd9a5dc..209003c6f 100644 --- a/src/math/lp/nla_core.cpp +++ b/src/math/lp/nla_core.cpp @@ -1238,7 +1238,7 @@ void core::negate_relation(unsigned j, const rational& a) { } } -bool core:: conflict_found() const { +bool core::conflict_found() const { for (const auto & l : * m_lemma_vec) { if (l.is_conflict()) return true; @@ -1246,11 +1246,11 @@ bool core:: conflict_found() const { return false; } -bool core:: done() const { +bool core::done() const { return m_lemma_vec->size() >= 10 || conflict_found(); } -lbool core:: inner_check(bool derived) { +lbool core::inner_check(bool derived) { if (derived && (lp_settings().st().m_nla_calls % m_settings.horner_frequency() == 0)) m_horner.horner_lemmas(); if (done()) { diff --git a/src/math/lp/nla_intervals.cpp b/src/math/lp/nla_intervals.cpp index 9a59c016b..37f918ac0 100644 --- a/src/math/lp/nla_intervals.cpp +++ b/src/math/lp/nla_intervals.cpp @@ -52,7 +52,7 @@ bool intervals::check_interval_for_conflict_on_zero_upper(const interval & i) { svector expl; m_dep_manager.linearize(i.m_upper_dep, expl); _().current_expl().add_expl(expl); - TRACE("nla_cn", print_lemma(tout);); + TRACE("nla_solver", print_lemma(tout);); return true; } @@ -67,7 +67,7 @@ bool intervals::check_interval_for_conflict_on_zero_lower(const interval & i) { svector expl; m_dep_manager.linearize(i.m_lower_dep, expl); _().current_expl().add_expl(expl); - TRACE("nla_cn_lemmas", print_lemma(tout);); + TRACE("nla_solver", print_lemma(tout);); return true; }