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

t

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2025-09-08 12:24:47 -10:00
parent 493ce3af2f
commit 8eec2b1932
1 changed files with 10 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

12
src/nlsat/levelwise.cpp
View file

@ -621,9 +621,17 @@ or
add_to_Q_if_new(property(prop_enum::repr,m_pm, m_level - 1)); add_to_Q_if_new(property(prop_enum::repr,m_pm, m_level - 1));
} }
/* Rule 4.6. Let i ∈ N, R ⊆ Ri, s ∈ R_{i−1}, and realRoots(p(s, xi )) = ∅. */
void apply_pre_sgn_inv(const property& p, bool has_repr) { void apply_pre_sgn_inv(const property& p, bool has_repr) {
NOT_IMPLEMENTED_YET(); if (p.level == 0) return; // nothing todo
scoped_anum_vector roots(m_am);
SASSERT(max_var(p.poly) == p.level && p.level == m_level);
m_am.isolate_roots(p.poly, undef_var_assignment(sample(), m_level), roots);
if (roots.size() == 0) {
//Rule 4.6 sample(s)(R), an_del(p)(R) ⊢ sgn_inv(p)(R)
add_to_Q_if_new(property(prop_enum::sample, m_pm, p.level - 1));
add_to_Q_if_new(property(prop_enum::an_del, p.poly, m_pm));
}
} }
/* /*