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-18 14:40:55 -07:00
parent 88e86af2c6
commit 0274982adb
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

@ -652,9 +652,17 @@ or
Let Q := an_sub(i − 1)(R) ∧ connected(i − 1)(R) ∧ repr(I, s)(R) ∧ an_del(b.p)(R). Let Q := an_sub(i − 1)(R) ∧ connected(i − 1)(R) ∧ repr(I, s)(R) ∧ an_del(b.p)(R).
Q, b.p= p ⊢ sgn_inv(p)(R) Q, b.p= p ⊢ sgn_inv(p)(R)
Q, b.p ̸= p, ord_inv(resxi (b.p, p))(R) ⊢ sgn_inv(p)(R)*/ Q, b.p ̸= p, ord_inv(resxi (b.p, p))(R) ⊢ sgn_inv(p)(R)*/
if (m_I[m_level].section == true) { const auto &I = m_I[m_level];
if (I.section == true) {
mk_prop(prop_enum::an_sub, m_level - 1); mk_prop(prop_enum::an_sub, m_level - 1);
NOT_IMPLEMENTED_YET(); mk_prop(prop_enum::connected, m_level - 1);
mk_prop(prop_enum::repr, m_level - 1); // is it correct?
mk_prop(prop_enum::an_del, polynomial_ref(m_I[m_level].l, m_pm));
if (I.l == p.poly.get()) {
// nothing is added
} else {
mk_prop(prop_enum::ord_inv, resultant(polynomial_ref(I.l, m_pm), p.poly, m_level));
}
} else { } else {
NOT_IMPLEMENTED_YET(); NOT_IMPLEMENTED_YET();
} }