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

normalize before pushing

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2025-10-18 13:14:22 -07:00
parent b85cba762c
commit c2661e34fc
2 changed files with 36 additions and 11 deletions
Download patch file Download diff file Expand all files Collapse all files

41
src/nlsat/levelwise.cpp
View file

@ -238,12 +238,14 @@ namespace nlsat {
poly* p = m_P[i]; poly* p = m_P[i];
polynomial_ref pref(p, m_pm); polynomial_ref pref(p, m_pm);
for_each_distinct_factor( pref, [&](const polynomial_ref& f) { for_each_distinct_factor( pref, [&](const polynomial_ref& f) {
unsigned level = max_var(f); // Normalize to primitive form for consistent comparison
polynomial_ref prim = to_primitive(f);
unsigned level = max_var(prim);
if (level < m_n) if (level < m_n)
m_Q[level].push(property(prop_enum::sgn_inv, f)); m_Q[level].push(property(prop_enum::sgn_inv, prim));
else if (level == m_n){ else if (level == m_n){
m_Q[level].push(property(prop_enum::an_del, f)); m_Q[level].push(property(prop_enum::an_del, prim));
ps_of_n_level.push_back(f.get()); ps_of_n_level.push_back(prim.get());
} }
else { else {
UNREACHABLE(); UNREACHABLE();
@ -309,7 +311,9 @@ namespace nlsat {
return false; return false;
} }
for_each_distinct_factor(r, [&](const polynomial::polynomial_ref &f) { for_each_distinct_factor(r, [&](const polynomial::polynomial_ref &f) {
m_Q[max_var(f)].push(property(prop_enum::ord_inv, f, m_pm)); // Normalize to primitive form for consistent comparison
polynomial_ref prim = to_primitive(f);
m_Q[max_var(prim)].push(property(prop_enum::ord_inv, prim, m_pm));
}); });
} }
return true; return true;
@ -512,14 +516,29 @@ namespace nlsat {
TRACE(lws, tout << "exit\n";); TRACE(lws, tout << "exit\n";);
} }
// Helper: convert polynomial to its primitive form (content-free version).
// Returns a polynomial_ref to the primitive form of p.
// All polynomials stored in properties will be in primitive form for consistent comparison.
polynomial_ref to_primitive(polynomial_ref const & p) {
if (m_pm.is_zero(p) || m_pm.is_const(p)) {
return p;
}
polynomial_ref result(m_pm);
var x = max_var(p);
m_pm.primitive(p.get(), x, result);
return result;
}
// add a property to m_Q if an equivalent one is not already present. // add a property to m_Q if an equivalent one is not already present.
// Equivalence: same m_prop_tag and same level; require the same poly as well. // Equivalence: same m_prop_tag and same level; polynomials checked for equality
// (polynomials are already in primitive form, so constant multipliers are normalized away).
void add_to_Q_if_new(const property & pr, unsigned level) { void add_to_Q_if_new(const property & pr, unsigned level) {
SASSERT(pr.m_prop_tag != ord_inv || (pr.m_poly && !m_pm.is_zero(pr.m_poly))); SASSERT(pr.m_prop_tag != ord_inv || (pr.m_poly && !m_pm.is_zero(pr.m_poly)));
for (auto const & q : m_Q[level]) { for (auto const & q : m_Q[level]) {
if (q.m_prop_tag != pr.m_prop_tag) continue; if (q.m_prop_tag != pr.m_prop_tag) continue;
if (q.m_poly != pr.m_poly) continue;
if (q.m_root_index != pr.m_root_index) continue; if (q.m_root_index != pr.m_root_index) continue;
if (!m_pm.eq(q.m_poly.get(), pr.m_poly.get())) continue;
TRACE(lws, display(tout << "matched q:", q) << std::endl;); TRACE(lws, display(tout << "matched q:", q) << std::endl;);
return; return;
} }
@ -798,11 +817,15 @@ or
} }
void mk_prop(prop_enum pe, const polynomial_ref& poly) { void mk_prop(prop_enum pe, const polynomial_ref& poly) {
add_to_Q_if_new(property(pe, poly), max_var(poly)); // Normalize polynomial to primitive form before storing in property
polynomial_ref prim = to_primitive(poly);
add_to_Q_if_new(property(pe, prim), max_var(prim));
} }
void mk_prop(prop_enum pe, const polynomial_ref& poly, unsigned level) { void mk_prop(prop_enum pe, const polynomial_ref& poly, unsigned level) {
SASSERT(is_set(level)); SASSERT(is_set(level));
add_to_Q_if_new(property(pe, poly), level); // Normalize polynomial to primitive form before storing in property
polynomial_ref prim = to_primitive(poly);
add_to_Q_if_new(property(pe, prim), level);
} }
void apply_pre_sgn_inv(const property& p) { void apply_pre_sgn_inv(const property& p) {

6
src/nlsat/nlsat_explain.cpp
View file

@ -1225,9 +1225,11 @@ namespace nlsat {
var x = m_todo.extract_max_polys(ps); var x = m_todo.extract_max_polys(ps);
TRACE(nlsat_explain, tout << "m_solver.apply_levelwise():" << m_solver.apply_levelwise() << "\n";); TRACE(nlsat_explain, tout << "m_solver.apply_levelwise():" << m_solver.apply_levelwise() << "\n";);
if (m_solver.apply_levelwise() && levelwise_single_cell(ps, max_x, m_cache)) if (m_solver.apply_levelwise() && levelwise_single_cell(ps, max_x, m_cache)) {
std::cout << "s";
return; return;
}
std::cout << "f";
polynomial_ref_vector samples(m_pm); polynomial_ref_vector samples(m_pm);
if (x < max_x) if (x < max_x)