mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-31 11:42:28 +00:00
Code Activity

align the univariate helper manager with the main polynomial manager

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2025-10-25 12:02:54 -07:00
parent 53e4d9562a
commit c72da53d19
1 changed files with 6 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

9
src/math/polynomial/polynomial.cpp
View file

@ -7203,15 +7203,18 @@ namespace polynomial {
}
void manager::set_z() {
return m_imp->m().set_z();
m_imp->m().set_z();
m_imp->upm().set_z();
}
void manager::set_zp(numeral const & p) {
return m_imp->m().set_zp(p);
m_imp->m().set_zp(p);
m_imp->upm().set_zp(p);
}
void manager::set_zp(uint64_t p) {
return m_imp->m().set_zp(p);
m_imp->m().set_zp(p);
m_imp->upm().set_zp(p);
}
bool manager::is_var(polynomial const* p, var& v) {