mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-28 18:29:23 +00:00
Code Activity

refactor and assert _irreducible

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2025-09-04 16:11:48 -10:00
parent 000ada361d
commit 83019e3da5
1 changed files with 25 additions and 14 deletions
Download patch file Download diff file Expand all files Collapse all files

39
src/nlsat/levelwise.cpp
View file

@ -40,7 +40,7 @@ namespace nlsat {
unsigned s_idx = -1; // index of the root function, if applicable; -1 means unspecified
unsigned level = -1; // -1 means unspecified
property(prop_enum pr, polynomial_ref const & pp, int si, int lvl) : prop_tag(pr), poly(pp), s_idx(si), level(lvl) {}
property(prop_enum pr, polynomial_ref const & pp) : prop_tag(pr), poly(pp), s_idx(-1), level(-1) {}
property(prop_enum pr, polynomial_ref const & pp, polynomial::manager& pm) : prop_tag(pr), poly(pp), s_idx(-1), level(pm.max_var(pp)) {}
property(prop_enum pr, polynomial::manager& pm, unsigned lvl) : prop_tag(pr), poly(polynomial_ref(pm)), s_idx(-1), level(lvl) {}
};
@ -216,7 +216,14 @@ namespace nlsat {
NOT_IMPLEMENTED_YET();// ambiguous resultant - not handled yet
return false;
}
m_Q.push_back(property(prop_enum::ord_inv_reducible, r, /*s_idx*/ -1, max_var(r)));
// Instead of adding property with r, add property with irreducible factors of r
polynomial::factors factors(m_pm);
factor(r, factors);
for (unsigned i = 0; i < factors.distinct_factors(); ++i) {
polynomial_ref f(m_pm);
f = factors[i];
m_Q.push_back(property(prop_enum::ord_inv_irreducible, f, m_pm));
}
}
return true;
}
@ -605,18 +612,22 @@ namespace nlsat {
if (sign(coeff, sample(), m_am) == 0)
continue;
auto it = std::find_if(m_Q.begin(), m_Q.end(), [&](const property & q) {
return (q.prop_tag == prop_enum::sgn_inv_irreducible || q.prop_tag == prop_enum::sgn_inv_reducible)
&& q.poly == p.poly;
});
if (it != m_Q.end()) {
erase_from_Q(p);
return true;
}
add_to_Q_if_new(property(prop_enum::sgn_inv_reducible, coeff, 0u, max_var(coeff)));
erase_from_Q(p);
return true;
polynomial::factors factors(m_pm);
factor(coeff, factors);
for (unsigned i = 0; i < factors.distinct_factors(); ++i) {
polynomial_ref f(m_pm);
f = factors[i];
auto it = std::find_if(m_Q.begin(), m_Q.end(), [f](const property & q) {
return
(q.prop_tag == prop_enum::sgn_inv_irreducible || q.prop_tag == prop_enum::sgn_inv_reducible) && q.poly == f;
});
if (it != m_Q.end()) //already asserted
return true;
m_Q.push_back(property(prop_enum::sgn_inv_reducible, f, m_pm));
}
erase_from_Q(p);
return true;
}
return false;
}