mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-08 17:01:55 +00:00
Code Activity

ignore holds properties

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2025-09-06 10:28:44 -10:00
parent 1e42f3f5a0
commit 1a89063bb9
1 changed files with 8 additions and 11 deletions
Download patch file Download diff file Expand all files Collapse all files

19
src/nlsat/levelwise.cpp
View file

@ -98,12 +98,11 @@ namespace nlsat {
// Helper to print out m_Q // Helper to print out m_Q
std::ostream& display(std::ostream& out) { std::ostream& display(std::ostream& out) {
out << "m_Q: [\n"; out << "[\n";
for (auto &q: m_Q) { for (auto &q: m_Q) {
auto q_dump = to_vector(q); auto q_dump = to_vector(q);
for (const auto& pr : q_dump) { for (const auto& pr : q_dump) {
display(out, pr); display(out, pr) << "\n";
out << "\n";
} }
} }
out << "]\n"; out << "]\n";
@ -294,8 +293,10 @@ namespace nlsat {
auto& q = m_Q[m_level]; auto& q = m_Q[m_level];
while(!q.empty()) { while(!q.empty()) {
property p = pop(q); property p = pop(q);
if (p.prop_tag == prop_to_avoid) if (p.prop_tag == prop_to_avoid) {
avoided.push_back(p); avoided.push_back(p);
continue;
}
apply_pre(p, has_repr); apply_pre(p, has_repr);
if (m_fail) break; if (m_fail) break;
} }
@ -372,13 +373,7 @@ namespace nlsat {
} }
build_representation(); build_representation();
// apply post-processing that may rely on the representation being present return apply_property_rules(prop_enum::holds, true);
if (!apply_property_rules(prop_enum(prop_enum::holds), true))
return true;
SASSERT(m_Q[m_level].empty());
return m_fail;
} }
// Extracted helper: handle ord_inv(discriminant_{x_{i+1}}(p)) for an_del pre-processing // Extracted helper: 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) {
@ -631,6 +626,8 @@ 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
default: default:
TRACE(levelwise, display(tout << "not impl: p", p)); TRACE(levelwise, display(tout << "not impl: p", p));
NOT_IMPLEMENTED_YET(); NOT_IMPLEMENTED_YET();