mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

chande row_is_interesting() in horner

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2019-07-25 17:49:07 -07:00
parent c605c5e5f6
commit 4c2279343b
1 changed files with 18 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

22
src/math/lp/horner.cpp
View file

@ -27,13 +27,27 @@ namespace nla {
typedef intervals::interval interv; typedef intervals::interval interv;
horner::horner(core * c) : common(c), m_intervals(c, c->reslim()) {} 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 <typename T> template <typename T>
bool horner::row_is_interesting(const T& row) const { bool horner::row_is_interesting(const T& row) const {
if (row.size() <= 1) std::unordered_set<lpvar> seen;
return false;
for (const auto& p : row) { for (const auto& p : row) {
if (c().m_to_refine.contains(p.var())) lpvar j = p.var();
return true; if (!c().is_monomial_var(j))
continue;
auto & m = c().emons()[j];
std::unordered_set<lpvar> 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; return false;
} }