From 4c2279343bf13e23c59693460fbaa1bc6f138a16 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Thu, 25 Jul 2019 17:49:07 -0700 Subject: [PATCH] chande row_is_interesting() in horner Signed-off-by: Lev Nachmanson --- src/math/lp/horner.cpp | 22 ++++++++++++++++++---- 1 file changed, 18 insertions(+), 4 deletions(-) diff --git a/src/math/lp/horner.cpp b/src/math/lp/horner.cpp index 012002ac9..01b44aa4a 100644 --- a/src/math/lp/horner.cpp +++ b/src/math/lp/horner.cpp @@ -27,13 +27,27 @@ namespace nla { typedef intervals::interval interv; horner::horner(core * c) : common(c), m_intervals(c, c->reslim()) {} +// Returns true if the row has at least two monomials sharing a variable template bool horner::row_is_interesting(const T& row) const { - if (row.size() <= 1) - return false; + std::unordered_set seen; for (const auto& p : row) { - if (c().m_to_refine.contains(p.var())) - return true; + lpvar j = p.var(); + if (!c().is_monomial_var(j)) + continue; + auto & m = c().emons()[j]; + + std::unordered_set local_vars; + for (lpvar k : m.vars()) { // have to do it to ignore the powers + local_vars.insert(k); + } + for (lpvar k : local_vars) { + auto it = seen.find(k); + if (it == seen.end()) + seen.insert(k); + else + return true; + } } return false; }