mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-01-04 10:08:46 +00:00
Code Activity

handle the zero case in add_ord_inv_resultant

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2025-12-17 10:49:31 -10:00
parent 9fc7e6cfe0
commit c37adafe12
1 changed files with 70 additions and 40 deletions
Download patch file Download diff file Expand all files Collapse all files

110
src/nlsat/levelwise.cpp
View file

@ -46,15 +46,7 @@ namespace nlsat {
fn(pr);
}
}
template<typename Func>
void for_first_distinct_factor(polynomial::polynomial_ref& poly, Func&& fn) {
polynomial::polynomial_ref_vector factors(m_pm);
::nlsat::factor(poly, m_cache, factors);
polynomial_ref pr(m_pm);
pr = factors.get(0);
fn(pr);
}
// todo: consider to key polynomials in a set by using m_pm.eq
struct property {
prop_enum m_prop_tag;
@ -318,19 +310,7 @@ namespace nlsat {
if (added_pairs.find(key) != added_pairs.end())
continue;
added_pairs.insert(key);
polynomial_ref r(m_pm);
r = resultant(polynomial_ref(p1, m_pm), polynomial_ref(p2, m_pm), m_n);
if (is_const(r)) continue;
TRACE(lws, tout << "resultant: "; ::nlsat::display(tout, m_solver, r); tout << std::endl;);
if (is_zero(r)) {
TRACE(lws, tout << "fail\n";);
SASSERT(same_polynomial_up_to_constant( p1, p2));
continue;
}
for_each_distinct_factor(r, [&](polynomial_ref& f) {
normalize(f);
mk_prop(prop_enum::ord_inv, f);
});
add_ord_inv_resultant(p1, p2, m_n);
}
}
@ -536,6 +516,71 @@ namespace nlsat {
return m_pm.eq(ca, cb);
}
void add_ord_inv_resultant(poly* a, poly* b, unsigned x) {
polynomial_ref pa(a, m_pm);
polynomial_ref pb(b, m_pm);
polynomial_ref r(m_pm);
r = resultant(pa, pb, x);
TRACE(lws,
tout << "resultant wrt x" << x << "\n";
::nlsat::display(tout << "a: ", m_solver, pa) << "\n";
::nlsat::display(tout << "b: ", m_solver, pb) << "\n";
::nlsat::display(tout << "r: ", m_solver, r) << "\n";);
if (is_zero(r)) {
TRACE(lws, tout << "zero resultant\n";);
polynomial_ref g(m_pm);
m_pm.gcd(a, b, g);
SASSERT (!is_const(g));
TRACE(lws, tout << "g:" << g << "\n;");
polynomial_ref p(m_pm), q(m_pm);
p = polynomial_ref(m_pm.exact_div(pa.get(), g.get()), m_pm);
q = polynomial_ref(m_pm.exact_div(pb.get(), g.get()), m_pm);
polynomial_ref_vector ps(m_pm), qs(m_pm);
::nlsat::factor(p, m_cache, ps);
::nlsat::factor(q, m_cache, qs);
TRACE(lws,
tout << "factors of p:";
for (unsigned i = 0; i < ps.size(); ++i) {
::nlsat::display(tout << " ", m_solver, polynomial_ref(ps.get(i), m_pm));
}
tout << "\n";
tout << "factors of q:";
for (unsigned i = 0; i < qs.size(); ++i) {
::nlsat::display(tout << " ", m_solver, polynomial_ref(qs.get(i), m_pm));
}
tout << "\n";);
for (unsigned i = 0; i < ps.size(); ++i) {
poly* a1 = ps.get(i);
if (max_var(a1) != x)
continue;
for (unsigned j = 0; j < qs.size(); ++j) {
poly* b1 = qs.get(j);
if (max_var(b1) != x)
continue;
TRACE(lws,
tout << "recurse add_ord_inv_resultant on factors\n";
::nlsat::display(tout << "a: ", m_solver, polynomial_ref(a1, m_pm)) << "\n";
::nlsat::display(tout << "b: ", m_solver, polynomial_ref(b1, m_pm)) << "\n";);
add_ord_inv_resultant(a1, b1, x);
}
}
for_each_distinct_factor(q, [&](polynomial_ref& f) {
TRACE(lws, tout << "an_del for q factor:" << f << "\n";);
mk_prop(prop_enum::an_del, f);
});
return;
}
for_each_distinct_factor(r, [&](polynomial_ref& f) {
TRACE(lws, tout << "f:" << f << "\n";);
mk_prop(prop_enum::ord_inv, f);
});
}
// add a property to m_Q if an equivalent one is not already present.
// Equivalence: same m_prop_tag and same level; polynomials checked for equality
@ -819,14 +864,8 @@ namespace nlsat {
if (I.l == p.m_poly.get()) {
// nothing is added
} else {
polynomial_ref res = resultant(I.l, p.m_poly, m_level);
SASSERT(m_unique_set.contains(I.l) && m_unique_set.contains(p.m_poly));
TRACE(lws,
tout << "m_level:" << m_level<< "\nresultant of (" << I.l << "," << p.m_poly << "):";
tout << "\nresultant:"; ::nlsat::display(tout, m_solver, res) << "\n");
SASSERT(!is_zero(res) || same_polynomial_up_to_constant(I.l, p.m_poly));
// Factor the resultant and add ord_inv for each distinct non-constant factor
for_each_distinct_factor(res, [&](polynomial::polynomial_ref f) { mk_prop(prop_enum::ord_inv, f);});
add_ord_inv_resultant(I.l, p.m_poly.get(), m_level);
}
} else {
/*
@ -942,17 +981,8 @@ namespace nlsat {
poly *a = m_rel.m_rfunc[pair.first].ire.p;
poly *b = m_rel.m_rfunc[pair.second].ire.p;
SASSERT(max_var(a) == max_var(b) && max_var(b) == m_level) ;
polynomial_ref r(m_pm);
r = resultant(polynomial_ref(a, m_pm), polynomial_ref(b, m_pm), m_level);
TRACE(lws, tout << "resultant of (" << pair.first << "," << pair.second << "):";
::nlsat::display(tout, m_solver, a) << "\n";
::nlsat::display(tout,m_solver, b)<< "\nresultant:"; ::nlsat::display(tout, m_solver, r) << "\n");
if (is_zero(r)) {
SASSERT(same_polynomial_up_to_constant(a, b));
continue;
}
for_each_distinct_factor(r, [this](const polynomial_ref& f) {mk_prop(ord_inv, f);});
if (m_pm.id(a) != m_pm.id(b))
add_ord_inv_resultant(a, b, m_level);
}
}