mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-09-10 11:41:25 +00:00
Code Activity

t

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2025-09-02 14:27:54 -10:00
parent 1f5fa63030
commit bce5ad38a9
1 changed files with 10 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

16
src/nlsat/levelwise.cpp
View file

@ -527,13 +527,7 @@ namespace nlsat {
build_representation(i, ret); build_representation(i, ret);
apply_property_rules(i, prop_enum(prop_enum::holds)); apply_property_rules(i, prop_enum(prop_enum::holds));
// Rule 1.1 precondition: when descending to level i-1, ensure m_Q contains // (moved Rule 1.1 precondition handling into apply_pre_connected)
// connected(i-1) and repr(I,s) so they are available for the next iteration.
if (i > 0) {
polynomial_ref empty(m_pm);
add_to_Q_if_new(property(prop_enum::connected, empty, /*level*/ i - 1));
add_to_Q_if_new(property(prop_enum::repr, empty, /*level*/ i - 1));
}
ret.Q = m_Q; ret.Q = m_Q;
ret.fail = m_fail; ret.fail = m_fail;
@ -637,7 +631,15 @@ namespace nlsat {
return; return;
} }
// Rule 1.1 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.
if (p.level > 0) {
polynomial_ref empty(m_pm);
add_to_Q_if_new(property(prop_enum::connected, empty, /*level*/ p.level - 1));
add_to_Q_if_new(property(prop_enum::repr, empty, /*level*/ p.level - 1));
}
// todo!!!! add missing preconditions
// connected property has been processed // connected property has been processed
erase_from_Q(p); erase_from_Q(p);
} }