mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-26 17:29:21 +00:00
Code Activity

create irreducible polynomials on init

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2025-10-10 13:58:41 -07:00
parent d235829b3d
commit a6d5c9762c
1 changed files with 13 additions and 11 deletions
Download patch file Download diff file Expand all files Collapse all files

24
src/nlsat/levelwise.cpp
View file

@ -174,17 +174,19 @@ namespace nlsat {
void collect_level_properties(std::vector<poly*> & ps_of_n_level) { void collect_level_properties(std::vector<poly*> & ps_of_n_level) {
for (unsigned i = 0; i < m_P.size(); ++i) { for (unsigned i = 0; i < m_P.size(); ++i) {
poly* p = m_P[i]; poly* p = m_P[i];
SASSERT(is_irreducible(p)); polynomial_ref pref(p, m_pm);
unsigned level = max_var(p); for_each_distinct_factor( pref, [&](const polynomial_ref& f) {
if (level < m_n) unsigned level = max_var(f);
m_Q[level].push(property(prop_enum::sgn_inv, polynomial_ref(p, m_pm))); if (level < m_n)
else if (level == m_n){ m_Q[level].push(property(prop_enum::sgn_inv, f));
m_Q[level].push(property(prop_enum::an_del, polynomial_ref(p, m_pm))); else if (level == m_n){
ps_of_n_level.push_back(p); m_Q[level].push(property(prop_enum::an_del, f));
} ps_of_n_level.push_back(f.get());
else { }
UNREACHABLE(); else {
} UNREACHABLE();
}
});
} }
} }