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

adding ir_ord

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2025-10-08 16:46:41 -07:00
parent 49eb5625ca
commit 7f5e7d523c
1 changed files with 42 additions and 22 deletions
Download patch file Download diff file Expand all files Collapse all files

64
src/nlsat/levelwise.cpp
View file

@ -314,7 +314,7 @@ namespace nlsat {
} }
//works on m_level //works on m_level
bool apply_property_rules(prop_enum prop_to_avoid, bool have_representation) { bool apply_property_rules(prop_enum prop_to_avoid) {
SASSERT (!m_fail); SASSERT (!m_fail);
std::vector<property> avoided; std::vector<property> avoided;
auto& q = m_Q[m_level]; auto& q = m_Q[m_level];
@ -324,7 +324,7 @@ namespace nlsat {
avoided.push_back(p); avoided.push_back(p);
continue; continue;
} }
apply_pre(p, have_representation); apply_pre(p);
if (m_fail) break; if (m_fail) break;
} }
if (m_fail) if (m_fail)
@ -409,7 +409,8 @@ namespace nlsat {
// Returns false on failure. // Returns false on failure.
// works on m_level // works on m_level
bool construct_interval() { bool construct_interval() {
if (!apply_property_rules(prop_enum::sgn_inv, false)) { m_E.clear();
if (!apply_property_rules(prop_enum::sgn_inv)) {
return false; return false;
} }
@ -417,7 +418,7 @@ namespace nlsat {
build_representation(); build_representation();
SASSERT(invariant()); SASSERT(invariant());
return apply_property_rules(prop_enum::holds, true); return apply_property_rules(prop_enum::holds);
} }
// 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) {
@ -492,7 +493,7 @@ namespace nlsat {
} }
// Pre-processing for connected(i) (Rule 4.11) // Pre-processing for connected(i) (Rule 4.11)
void apply_pre_connected(const property & p, bool have_representation) { void apply_pre_connected(const property & p) {
// Rule 4.11 special-case: if the connected property refers to level 0 there's nothing to refine // Rule 4.11 special-case: if the connected property refers to level 0 there's nothing to refine
// further; just remove the property from Q and return. // further; just remove the property from Q and return.
if (m_level == 0) { if (m_level == 0) {
@ -502,16 +503,24 @@ namespace nlsat {
// p.level > 0 // p.level > 0
// Rule 4.11 precondition: when processing connected(i) we must ensure the next lower level // Rule 4.11 precondition: when processing connected(i) we must ensure the next lower level
// has connected(i-1) and repr(I,s) available. Add those markers to m_Q so they propagate. // has connected(i-1) and repr(I,s) available.
/*
Let Q := connected(i − 1)(R) ∧ repr(I, s)(R).
Q, I = (sector, l, u), l ̸= −∞, u ̸= ∞, l (≼t) u, add ir_ord(≼, s)
Q, I = (sector, l, u), l= −∞ ∨ u = ∞
Q, I = (section, b) ⊢ connected(i)(R)
*/
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)); mk_prop(prop_enum::repr, level_t(m_level - 1));
if (!have_representation) if (!have_representation())
return; // no change since the cell representation is not available return; // no change since the cell representation is not available
NOT_IMPLEMENTED_YET(); const auto& I = m_I[m_level];
// todo!!!! add missing preconditions TRACE(lws, display(tout << "interval m_I[" << m_level << "]\n", I) << "\n";);
// connected property has been processed SASSERT(I.is_sector());
if (!I.l_inf() && !I.u_inf()) {
mk_prop(ir_ord, level_t(m_level));
}
} }
void apply_pre_non_null(const property& p) { void apply_pre_non_null(const property& p) {
@ -645,7 +654,7 @@ or
} }
} }
void apply_pre_sample(const property& p, bool have_representation) { void apply_pre_sample(const property& p) {
if (m_level == 0) if (m_level == 0)
return; return;
mk_prop(sample_holds, level_t(m_level - 1)); mk_prop(sample_holds, level_t(m_level - 1));
@ -678,7 +687,7 @@ or
add_to_Q_if_new(property(pe, poly, root_index), level); add_to_Q_if_new(property(pe, poly, root_index), level);
} }
void apply_pre_sgn_inv(const property& p, bool have_representation) { 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);
SASSERT(max_var(p.poly) == m_level); SASSERT(max_var(p.poly) == m_level);
@ -742,7 +751,7 @@ or
p(s) ̸= 0, sample(s)(R), sgn_inv(p)(R) ⊢ ord_inv(p)(R) p(s) ̸= 0, sample(s)(R), sgn_inv(p)(R) ⊢ ord_inv(p)(R)
p(s)= 0, sample(s)(R), an_sub(i− 1)(R), connected(i)(R), sgn_inv(p)(R), an_del(p)(R) ⊢ ord_inv(p)(R) p(s)= 0, sample(s)(R), an_sub(i− 1)(R), connected(i)(R), sgn_inv(p)(R), an_del(p)(R) ⊢ ord_inv(p)(R)
*/ */
void apply_pre_ord_inv(const property& p, bool have_representation) { void apply_pre_ord_inv(const property& p) {
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);
@ -758,7 +767,7 @@ or
} }
} }
void apply_pre(const property& p, bool have_representation) { 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;);
switch (p.prop_tag) { switch (p.prop_tag) {
@ -766,7 +775,7 @@ or
apply_pre_an_del(p); apply_pre_an_del(p);
break; break;
case prop_enum::connected: case prop_enum::connected:
apply_pre_connected(p, have_representation); apply_pre_connected(p);
break; break;
case prop_enum::non_null: case prop_enum::non_null:
apply_pre_non_null(p); apply_pre_non_null(p);
@ -780,15 +789,19 @@ or
case prop_enum::holds: case prop_enum::holds:
break; // ignore the bottom of refinement break; // ignore the bottom of refinement
case sample_holds: case sample_holds:
apply_pre_sample(p, have_representation); apply_pre_sample(p);
break; break;
case prop_enum::sgn_inv: case prop_enum::sgn_inv:
apply_pre_sgn_inv(p, have_representation); apply_pre_sgn_inv(p);
break; break;
case prop_enum::ord_inv: case prop_enum::ord_inv:
apply_pre_ord_inv(p, have_representation); apply_pre_ord_inv(p);
break;
case prop_enum::ir_ord:
apply_pre_ir_ord(p);
break; break;
default: default:
display(std::cout << "not impl: p", p);
TRACE(lws, display(tout << "not impl: p", p)); TRACE(lws, display(tout << "not impl: p", p));
NOT_IMPLEMENTED_YET(); NOT_IMPLEMENTED_YET();
break; break;
@ -797,6 +810,12 @@ or
SASSERT(invariant()); SASSERT(invariant());
} }
bool have_representation() const { return m_E.size() > 0; }
void apply_pre_ir_ord(const property&) {
NOT_IMPLEMENTED_YET();
}
bool invariant() { bool invariant() {
for (unsigned i = 0; i < m_Q.size(); i++) { for (unsigned i = 0; i < m_Q.size(); i++) {
auto qv = to_vector(m_Q[i]); auto qv = to_vector(m_Q[i]);
@ -820,8 +839,9 @@ or
if (m_n == 0) return m_I; // we have an empty sample if (m_n == 0) return m_I; // we have an empty sample
m_level = m_n; m_level = m_n;
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
apply_property_rules(prop_enum::_count, false); // reduce the level by one to be consumed by construct_interval SASSERT(m_E.size() == 0);
apply_property_rules(prop_enum::_count); // reduce the level by one to be consumed by construct_interval
while (-- m_level > 0) while (-- m_level > 0)
if (!construct_interval()) if (!construct_interval())
return std::vector<root_function_interval>(); // return empty return std::vector<root_function_interval>(); // return empty