mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-26 09:24:36 +00:00
Code Activity

process level 0 as well

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2025-10-11 13:55:54 -07:00
parent 81dec49492
commit 77490399a9
1 changed files with 30 additions and 34 deletions
Download patch file Download diff file Expand all files Collapse all files

64
src/nlsat/levelwise.cpp
View file

@ -24,7 +24,6 @@ namespace nlsat {
an_sub, an_sub,
sample_holds, sample_holds,
repr, repr,
holds,
_count _count
}; };
@ -272,12 +271,13 @@ namespace nlsat {
// find first index where roots[idx].val >= y_val // find first index where roots[idx].val >= y_val
size_t idx = 0; size_t idx = 0;
while (idx < roots.size() && m_am.compare(roots[idx].val, y_val) < 0) ++idx; while (idx < roots.size() && m_am.compare(roots[idx].val, y_val) < 0) ++idx;
if (idx < roots.size() && m_am.compare(roots[idx].val, y_val) == 0) { if (idx < roots.size() && m_am.compare(roots[idx].val, y_val) == 0) {
TRACE(lws, tout << "exact match at idx=" << idx << ", it's a section\n";);
auto const& ire = roots[idx].ire; auto const& ire = roots[idx].ire;
I.section = true; I.section = true;
I.l = ire.p; I.l_index = ire.i; I.l = ire.p; I.l_index = ire.i;
I.u = nullptr; I.u_index = -1; // the section is defined by the I.l I.u = nullptr; I.u_index = -1; // the section is defined by the I.l
TRACE(lws, tout << "section bound -> p="; if (I.l) m_pm.display(tout, I.l); tout << ", index=" << I.l_index << "\n";);
return; return;
} }
@ -412,7 +412,7 @@ namespace nlsat {
build_representation(); build_representation();
SASSERT(invariant()); SASSERT(invariant());
return apply_property_rules(prop_enum::holds); return apply_property_rules(prop_enum::_count);
} }
// handle ord_inv(discriminant_{x_{i+1}}(p)) for an_del pre-processing // 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) {
@ -563,7 +563,7 @@ namespace nlsat {
continue; continue;
for_first_distinct_factor(coeff, [&](const polynomial::polynomial_ref & f) { for_first_distinct_factor(coeff, [&](const polynomial::polynomial_ref & f) {
mk_prop(prop_enum::sgn_inv, f, -1, max_var(f)); mk_prop(prop_enum::sgn_inv, f);
}); });
return true; return true;
} }
@ -601,9 +601,8 @@ namespace nlsat {
} }
// If discriminant is non-constant, add sign-invariance requirement for it // If discriminant is non-constant, add sign-invariance requirement for it
if (!is_const(disc)) { if (!is_const(disc)) {
unsigned lvl = max_var(disc);
for_each_distinct_factor(disc, [&](const polynomial::polynomial_ref & f) { for_each_distinct_factor(disc, [&](const polynomial::polynomial_ref & f) {
mk_prop(prop_enum::sgn_inv, f, /*s_idx*/ -1, lvl); mk_prop(prop_enum::sgn_inv, f);
}); });
} }
@ -621,7 +620,7 @@ namespace nlsat {
} }
/* /*
Rule 4.13 Rule 4.13 : the precondition holds by construction
The property repr(I, s) holds on R if and only if I.l ∈ irExpr(I.l.p, s) (if I.l ̸= −∞), I.u ∈ irExpr(I.u.p, s) The property repr(I, s) holds on R if and only if I.l ∈ irExpr(I.l.p, s) (if I.l ̸= −∞), I.u ∈ irExpr(I.u.p, s)
(if I.u ̸= ∞) respectively I.b ∈ irExpr(I.b.p, s) and one of the following holds: (if I.u ̸= ∞) respectively I.b ∈ irExpr(I.b.p, s) and one of the following holds:
• I = (sector, l, u), dom(θl,s ) ∩ dom(θu,s ) ⊇ R ↓[i−1] and R = {(r, r′) | r ∈ R ↓[i−1], r′ ∈ (θl,s (r), θu,s (r))}; • I = (sector, l, u), dom(θl,s ) ∩ dom(θu,s ) ⊇ R ↓[i−1] and R = {(r, r′) | r ∈ R ↓[i−1], r′ ∈ (θl,s (r), θu,s (r))};
@ -635,16 +634,19 @@ or
void apply_pre_repr(const property& p) { void apply_pre_repr(const property& p) {
const auto& I = m_I[m_level]; const auto& I = m_I[m_level];
TRACE(lws, display(tout << "interval m_I[" << m_level << "]\n", I) << "\n";); TRACE(lws, display(tout << "interval m_I[" << m_level << "]\n", I) << "\n";);
mk_prop(prop_enum::holds, level_t(m_level - 1));
mk_prop(sample_holds, level_t(m_level - 1)); mk_prop(sample_holds, level_t(m_level - 1));
if (I.is_section()) { if (I.is_section()) {
NOT_IMPLEMENTED_YET(); /*sample(s)(R), holds(I)(R), I = (section, b), an_del(b.p)(R) */
mk_prop(an_del, I.l);
} else { } else {
/* sample(s)(R), holds(I)(R), I = (sector, l, u), l= −∞ ∨ an_del(l.p)(R), u = ∞ ∨ an_del(u.p)(R*/
SASSERT(I.is_sector()); SASSERT(I.is_sector());
if (!I.l_inf() || !I.u_inf()) {
NOT_IMPLEMENTED_YET(); if (!I.l_inf())
} mk_prop(an_del, I.l);
} if (!I.u_inf())
mk_prop(an_del, I.u);
}
} }
void apply_pre_sample(const property& p) { void apply_pre_sample(const property& p) {
@ -660,7 +662,7 @@ or
}; };
void mk_prop(prop_enum pe, level_t level) { void mk_prop(prop_enum pe, level_t level) {
SASSERT(level.val != static_cast<unsigned>(-1)); if ((int)level.val == -1) return; // ignore this property
SASSERT(pe != ord_inv); SASSERT(pe != ord_inv);
add_to_Q_if_new(property(pe, m_pm), level.val); add_to_Q_if_new(property(pe, m_pm), level.val);
} }
@ -675,11 +677,6 @@ or
add_to_Q_if_new(property(pe, poly), level); add_to_Q_if_new(property(pe, poly), level);
} }
void mk_prop(prop_enum pe, const polynomial_ref& poly, unsigned root_index, unsigned level) {
SASSERT(poly || pe != ord_inv);
add_to_Q_if_new(property(pe, poly, root_index), level);
}
void apply_pre_sgn_inv(const property& p) { void apply_pre_sgn_inv(const property& p) {
SASSERT(is_irreducible(p.poly)); SASSERT(is_irreducible(p.poly));
scoped_anum_vector roots(m_am); scoped_anum_vector roots(m_am);
@ -706,7 +703,7 @@ or
*/ */
mk_prop(prop_enum::an_sub, level_t(m_level - 1)); mk_prop(prop_enum::an_sub, level_t(m_level - 1));
mk_prop(prop_enum::connected, level_t(m_level - 1)); mk_prop(prop_enum::connected, level_t(m_level - 1));
mk_prop(prop_enum::repr, level_t(m_level - 1)); // is it correct? mk_prop(prop_enum::repr, level_t(m_level - 1));
mk_prop(prop_enum::an_del, polynomial_ref(m_I[m_level].l, m_pm)); mk_prop(prop_enum::an_del, polynomial_ref(m_I[m_level].l, m_pm));
if (I.l == p.poly.get()) { if (I.l == p.poly.get()) {
// nothing is added // nothing is added
@ -748,15 +745,14 @@ or
SASSERT(p.prop_tag == prop_enum::ord_inv && is_irreducible(p.poly)); SASSERT(p.prop_tag == prop_enum::ord_inv && is_irreducible(p.poly));
unsigned level = max_var(p.poly); unsigned level = max_var(p.poly);
auto sign_on_sample = sign(p.poly, sample(), m_am); auto sign_on_sample = sign(p.poly, sample(), m_am);
mk_prop(sample_holds, level_t(level));
if (sign_on_sample) { if (sign_on_sample) {
mk_prop(sample_holds, level_t(level));
mk_prop(prop_enum::sgn_inv, p.poly); mk_prop(prop_enum::sgn_inv, p.poly);
} else { // sign is zero } else { // sign is zero
mk_prop(sample_holds, level_t(level));
mk_prop(prop_enum::an_sub, level_t(level - 1)); mk_prop(prop_enum::an_sub, level_t(level - 1));
mk_prop(prop_enum::connected, level_t(level)); mk_prop(prop_enum::connected, level_t(level));
mk_prop(prop_enum::sgn_inv, p.poly, p.s_idx, level); mk_prop(prop_enum::sgn_inv, p.poly);
mk_prop(prop_enum::an_del, p.poly, p.s_idx, level); mk_prop(prop_enum::an_del, p.poly);
} }
} }
@ -779,8 +775,6 @@ or
case prop_enum::repr: case prop_enum::repr:
apply_pre_repr(p); apply_pre_repr(p);
break; break;
case prop_enum::holds:
break; // ignore the bottom of refinement
case sample_holds: case sample_holds:
apply_pre_sample(p); apply_pre_sample(p);
break; break;
@ -810,10 +804,11 @@ or
Assume that ξ.p is irreducible for all ξ ∈ dom(≼), and that ≼ matches s. Assume that ξ.p is irreducible for all ξ ∈ dom(≼), and that ≼ matches s.
sample(s)(R), an_sub(i)(R), connected(i)(R), ∀ξ ∈ dom(≼). an_del(ξ.p)(R), ∀(ξ,ξ′) ∈≼. ord_inv(resx_{i+1} (ξ.p, ξ′.p))(R) ⊢ ir_ord(≼, s)(R) sample(s)(R), an_sub(i)(R), connected(i)(R), ∀ξ ∈ dom(≼). an_del(ξ.p)(R), ∀(ξ,ξ′) ∈≼. ord_inv(resx_{i+1} (ξ.p, ξ′.p))(R) ⊢ ir_ord(≼, s)(R)
*/ */
if (m_level > 0) {
mk_prop(sample_holds, level_t(m_level -1 )); mk_prop(sample_holds, level_t(m_level -1 ));
mk_prop(an_sub, level_t(m_level - 1)); mk_prop(an_sub, level_t(m_level - 1));
mk_prop(connected, level_t(m_level - 1)); mk_prop(connected, level_t(m_level - 1));
}
for (unsigned i = 0; i + 1 < m_E.size(); i++) { for (unsigned i = 0; i + 1 < m_E.size(); i++) {
SASSERT(max_var(m_E[i].ire.p) == max_var(m_E[i + 1].ire.p)); SASSERT(max_var(m_E[i].ire.p) == max_var(m_E[i + 1].ire.p));
SASSERT(max_var(m_E[i].ire.p) == m_level); SASSERT(max_var(m_E[i].ire.p) == m_level);
@ -850,11 +845,13 @@ or
init_properties(); // initializes m_Q as a queue of properties on levels <= m_n init_properties(); // initializes m_Q as a queue of properties on levels <= m_n
SASSERT(m_E.size() == 0); SASSERT(m_E.size() == 0);
apply_property_rules(prop_enum::_count); // reduce the level by one to be consumed by construct_interval apply_property_rules(prop_enum::_count); // reduce the level from m_n to m_n - 1 to be consumed by construct_interval
while (-- m_level > 0) SASSERT(m_level == m_n);
do { // m_level changes from m_n - 1 to 0
m_level--;
if (m_fail || !construct_interval()) if (m_fail || !construct_interval())
return std::vector<root_function_interval>(); // return empty return std::vector<root_function_interval>(); // return empty
} while (m_level != 0);
return m_I; // the order of intervals is reversed return m_I; // the order of intervals is reversed
} }
@ -870,7 +867,6 @@ or
case prop_enum::an_sub: return "an_sub"; case prop_enum::an_sub: return "an_sub";
case sample_holds: return "sample"; case sample_holds: return "sample";
case prop_enum::repr: return "repr"; case prop_enum::repr: return "repr";
case prop_enum::holds: return "holds";
case prop_enum::_count: return "_count"; case prop_enum::_count: return "_count";
} }
return "?"; return "?";