mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-09 01:11:55 +00:00
Code Activity

t

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2025-09-08 07:22:59 -10:00
parent 2a3cccaec3
commit 3cf0c730b9
1 changed files with 27 additions and 16 deletions
Download patch file Download diff file Expand all files Collapse all files

27
src/nlsat/levelwise.cpp
View file

@ -376,17 +376,23 @@ namespace nlsat {
// Extracted helper: handle ord_inv(discriminant_{x_{i+1}}(p)) for an_del pre-processing // Extracted helper: handle ord_inv(discriminant_{x_{i+1}}(p)) for an_del pre-processing
void add_ord_inv_discriminant_for(const property& p) { void add_ord_inv_discriminant_for(const property& p) {
polynomial_ref disc(m_pm); polynomial_ref disc(m_pm);
disc = discriminant(p.poly, p.level); // todo - factor the discriminant!!!! disc = discriminant(p.poly, p.level);
TRACE(levelwise, ::nlsat::display(tout << "discriminant: ", m_solver, disc) << "\n";); TRACE(levelwise, ::nlsat::display(tout << "discriminant: ", m_solver, disc) << "\n";);
if (!is_const(disc)) { if (!is_const(disc)) {
if (coeffs_are_zeroes_on_sample(disc, m_pm, sample(), m_am)) { // Factor the discriminant
polynomial::factors disc_factors(m_pm);
factor(disc, disc_factors);
for (unsigned i = 0; i < disc_factors.distinct_factors(); ++i) {
polynomial_ref f = disc_factors[i];
if (coeffs_are_zeroes_on_sample(f, m_pm, sample(), m_am)) {
m_fail = true; // ambiguous multiplicity -- not handled yet m_fail = true; // ambiguous multiplicity -- not handled yet
NOT_IMPLEMENTED_YET(); NOT_IMPLEMENTED_YET();
return; return;
} }
else { else {
unsigned lvl = max_var(disc); unsigned lvl = max_var(f);
add_to_Q_if_new(property(prop_enum::ord_inv, disc, /*s_idx*/ 0u, lvl)); add_to_Q_if_new(property(prop_enum::ord_inv, f, /*s_idx*/ 0u, lvl));
}
} }
} }
} }
@ -398,14 +404,19 @@ namespace nlsat {
if (deg > 0) { if (deg > 0) {
polynomial_ref lc(m_pm); polynomial_ref lc(m_pm);
lc = m_pm.coeff(pp, p.level, deg); lc = m_pm.coeff(pp, p.level, deg);
// todo - factor lc
if (!is_const(lc)) { if (!is_const(lc)) {
if (coeffs_are_zeroes_on_sample(lc, m_pm, sample(), m_am)) { // Factor the leading coefficient
polynomial::factors lc_factors(m_pm);
factor(lc, lc_factors);
for (unsigned i = 0; i < lc_factors.distinct_factors(); ++i) {
polynomial_ref f = lc_factors[i];
if (coeffs_are_zeroes_on_sample(f, m_pm, sample(), m_am)) {
NOT_IMPLEMENTED_YET(); // leading coeff vanished as polynomial -- not handled yet NOT_IMPLEMENTED_YET(); // leading coeff vanished as polynomial -- not handled yet
} }
else { else {
unsigned lvl = max_var(lc); unsigned lvl = max_var(f);
add_to_Q_if_new(property(prop_enum::sgn_inv, lc, /*s_idx*/ 0u, lvl)); add_to_Q_if_new(property(prop_enum::sgn_inv, f, /*s_idx*/ 0u, lvl));
}
} }
} }
} }