mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-12-12 22:56:23 +00:00
Code Activity

normalize polynomials

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2025-12-10 12:09:38 -10:00
parent 653a4ece42
commit 1fe7359c7b
5 changed files with 39 additions and 17 deletions
Download patch file Download diff file Expand all files Collapse all files

10
src/math/polynomial/polynomial_cache.cpp
View file

@ -128,7 +128,7 @@ namespace polynomial {
m_factor_cache.reset(); m_factor_cache.reset();
} }
unsigned pid(polynomial * p) const { return m.id(p); } unsigned pid(const polynomial * p) const { return m.id(p); }
polynomial * mk_unique(polynomial * p) { polynomial * mk_unique(polynomial * p) {
if (m_in_cache.get(pid(p), false)) if (m_in_cache.get(pid(p), false))
@ -141,6 +141,10 @@ namespace polynomial {
return p_prime; return p_prime;
} }
bool contains(const polynomial * p) const {
return m_in_cache.get(pid(p), false);
}
void psc_chain(polynomial * p, polynomial * q, var x, polynomial_ref_vector & S) { void psc_chain(polynomial * p, polynomial * q, var x, polynomial_ref_vector & S) {
p = mk_unique(p); p = mk_unique(p);
q = mk_unique(q); q = mk_unique(q);
@ -213,6 +217,10 @@ namespace polynomial {
return m_imp->mk_unique(p); return m_imp->mk_unique(p);
} }
bool cache::contains(const polynomial * p) const {
return m_imp->contains(p);
}
void cache::psc_chain(polynomial const * p, polynomial const * q, var x, polynomial_ref_vector & S) { void cache::psc_chain(polynomial const * p, polynomial const * q, var x, polynomial_ref_vector & S) {
m_imp->psc_chain(const_cast<polynomial*>(p), const_cast<polynomial*>(q), x, S); m_imp->psc_chain(const_cast<polynomial*>(p), const_cast<polynomial*>(q), x, S);
} }

1
src/math/polynomial/polynomial_cache.h
View file

@ -34,6 +34,7 @@ namespace polynomial {
manager & m() const; manager & m() const;
manager & pm() const { return m(); } manager & pm() const { return m(); }
polynomial * mk_unique(polynomial * p); polynomial * mk_unique(polynomial * p);
bool contains(const polynomial * p) const;
void psc_chain(polynomial const * p, polynomial const * q, var x, polynomial_ref_vector & S); void psc_chain(polynomial const * p, polynomial const * q, var x, polynomial_ref_vector & S);
void factor(polynomial const * p, polynomial_ref_vector & distinct_factors); void factor(polynomial const * p, polynomial_ref_vector & distinct_factors);
void reset(); void reset();

24
src/nlsat/levelwise.cpp
View file

@ -227,7 +227,7 @@ namespace nlsat {
void collect_top_level_properties(todo_set& ps_of_n_level) { void collect_top_level_properties(todo_set& ps_of_n_level) {
for (unsigned i = 0; i < m_P.size(); ++i) { for (unsigned i = 0; i < m_P.size(); ++i) {
polynomial_ref pi(m_P[i], m_pm); polynomial_ref pi(m_P[i], m_pm);
for_each_distinct_factor(pi, [&](const polynomial_ref& f) { for_each_distinct_factor(pi, [&](polynomial_ref f) {
unsigned level = max_var(f); unsigned level = max_var(f);
normalize(f); normalize(f);
if (level < m_n) if (level < m_n)
@ -300,7 +300,7 @@ namespace nlsat {
fail(); fail();
return false; return false;
} }
for_each_distinct_factor(r, [&](const polynomial::polynomial_ref &f) { for_each_distinct_factor(r, [&](polynomial::polynomial_ref f) {
normalize(f); normalize(f);
m_Q[max_var(f)].push(property(prop_enum::ord_inv, f, m_pm)); m_Q[max_var(f)].push(property(prop_enum::ord_inv, f, m_pm));
}); });
@ -501,9 +501,10 @@ namespace nlsat {
TRACE(lws, tout << "exit\n";); TRACE(lws, tout << "exit\n";);
} }
void normalize(polynomial_ref const & p) { void normalize(polynomial_ref & p) {
SASSERT(! (is_zero(p) || is_const(p))); SASSERT(!(is_zero(p) || is_const(p)));
m_todo_set.insert(p); poly* np = m_todo_set.insert(p);
p = np;
} }
@ -560,8 +561,10 @@ namespace nlsat {
} }
} }
// handle sgn_inv(leading_coefficient_{x_{i+1}}(p)) for an_del pre-processing // handle sgn_inv(leading_coefficient_{x_{i+1}}(p)) for an_del pre-processing
void add_sgn_inv_leading_coeff_for(const property& p) { void add_sgn_inv_leading_coeff_for(const property& p) {
TRACE(lws, tout << "p:"; display(tout, p) << "\n";);
poly * pp = p.m_poly.get(); poly * pp = p.m_poly.get();
unsigned lvl = max_var(p.m_poly); unsigned lvl = max_var(p.m_poly);
unsigned deg = m_pm.degree(pp, lvl); unsigned deg = m_pm.degree(pp, lvl);
@ -572,11 +575,12 @@ namespace nlsat {
for (int d = static_cast<int>(deg); d >= 0; --d) { for (int d = static_cast<int>(deg); d >= 0; --d) {
coeff = m_pm.coeff(pp, lvl, d); coeff = m_pm.coeff(pp, lvl, d);
if (!is_const(coeff)) { if (!is_const(coeff)) {
for_each_distinct_factor(coeff, [&](const polynomial::polynomial_ref & f) { for_each_distinct_factor(coeff, [&](polynomial::polynomial_ref f) {
normalize(f); normalize(f);
mk_prop(prop_enum::sgn_inv, f, max_var(f)); mk_prop(prop_enum::sgn_inv, f, max_var(f));
}); });
} }
TRACE(lws, tout << "coeff:" << coeff << "\n";);
if (sign(coeff, sample(), m_am)) if (sign(coeff, sample(), m_am))
return; return;
@ -789,11 +793,11 @@ or
add_to_Q_if_new(property(pe, m_pm), level.val); add_to_Q_if_new(property(pe, m_pm), level.val);
} }
void mk_prop(prop_enum pe, const polynomial_ref& poly) { void mk_prop(prop_enum pe, polynomial_ref poly) {
normalize(poly); normalize(poly);
add_to_Q_if_new(property(pe, poly), max_var(poly)); add_to_Q_if_new(property(pe, poly), max_var(poly));
} }
void mk_prop(prop_enum pe, const polynomial_ref& poly, unsigned level) { void mk_prop(prop_enum pe, polynomial_ref poly, unsigned level) {
SASSERT(is_set(level)); SASSERT(is_set(level));
normalize(poly); normalize(poly);
add_to_Q_if_new(property(pe, poly), level); add_to_Q_if_new(property(pe, poly), level);
@ -840,7 +844,8 @@ or
if (I.l == p.m_poly.get()) { if (I.l == p.m_poly.get()) {
// nothing is added // nothing is added
} else { } else {
polynomial_ref res = resultant(polynomial_ref(I.l, m_pm), p.m_poly, m_level); polynomial_ref res = resultant(I.l, p.m_poly, m_level);
SASSERT(m_todo_set.contains(I.l) && m_todo_set.contains(p.m_poly));
TRACE(lws, TRACE(lws,
tout << "m_level:" << m_level<< "\nresultant of (" << I.l << "," << p.m_poly << "):"; tout << "m_level:" << m_level<< "\nresultant of (" << I.l << "," << p.m_poly << "):";
tout << "\nresultant:"; ::nlsat::display(tout, m_solver, res) << "\n"); tout << "\nresultant:"; ::nlsat::display(tout, m_solver, res) << "\n");
@ -909,6 +914,7 @@ or
void apply_pre(const property& p) { void apply_pre(const property& p) {
TRACE(lws, tout << "apply_pre BEGIN m_Q:"; display(tout) << std::endl; TRACE(lws, tout << "apply_pre BEGIN m_Q:"; display(tout) << std::endl;
display(tout << "pre p:", p) << std::endl;); display(tout << "pre p:", p) << std::endl;);
SASSERT(!p.m_poly || m_todo_set.contains(p.m_poly));
switch (p.m_prop_tag) { switch (p.m_prop_tag) {
case prop_enum::an_del: case prop_enum::an_del:
apply_pre_an_del(p); apply_pre_an_del(p);

15
src/nlsat/nlsat_common.cpp
View file

@ -30,7 +30,7 @@ namespace nlsat {
m_set.reset(); m_set.reset();
} }
void todo_set::insert(poly* p) { poly* todo_set::insert(poly* p) {
pmanager& pm = m_set.m(); pmanager& pm = m_set.m();
polynomial_ref pinned(pm); // keep canonicalized polynomial alive until it is stored polynomial_ref pinned(pm); // keep canonicalized polynomial alive until it is stored
if (m_canonicalize) { if (m_canonicalize) {
@ -47,10 +47,15 @@ namespace nlsat {
} }
p = m_cache.mk_unique(p); p = m_cache.mk_unique(p);
unsigned pid = pm.id(p); unsigned pid = pm.id(p);
if (m_in_set.get(pid, false)) if (!m_in_set.get(pid, false)) {
return; m_in_set.setx(pid, true, false);
m_in_set.setx(pid, true, false); m_set.push_back(p);
m_set.push_back(p); }
return p;
}
bool todo_set::contains(poly* p) const {
return m_cache.contains(p);
} }
bool todo_set::empty() const { return m_set.empty(); } bool todo_set::empty() const { return m_set.empty(); }

4
src/nlsat/nlsat_common.h
View file

@ -32,7 +32,9 @@ namespace nlsat {
todo_set(polynomial::cache& u, bool canonicalize); todo_set(polynomial::cache& u, bool canonicalize);
void reset(); void reset();
void insert(poly* p); // Insert polynomial (canonicalizing if requested) and return the cached representative.
poly* insert(poly* p);
bool contains(poly *) const;
bool empty() const; bool empty() const;
// Return max variable in todo_set // Return max variable in todo_set
var max_var() const; var max_var() const;