From 658cf36f09b6a2c93d0e6ee0e582509ef4f63c84 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Sat, 13 Sep 2025 15:09:16 -0700 Subject: [PATCH] t Signed-off-by: Lev Nachmanson --- src/nlsat/levelwise.cpp | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) diff --git a/src/nlsat/levelwise.cpp b/src/nlsat/levelwise.cpp index 3a22bc744..35417cb78 100644 --- a/src/nlsat/levelwise.cpp +++ b/src/nlsat/levelwise.cpp @@ -633,13 +633,17 @@ or add_to_Q_if_new(property(prop_enum::an_del, p.poly), m_level); } /* Rule 4.8. Let i ∈ N>0 , R ⊆ Ri - , s ∈ Ri−1 + , s ∈ R_{i−1} , p ∈ Q[x1, . . . , xi ], level(p) = i, and I be a symbolic interval of level i. Assume that p is irreducible, and I = (section, b). 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, ord_inv(resxi (b.p, p))(R) ⊢ sgn_inv(p)(R)*/ - NOT_IMPLEMENTED_YET(); + if (m_I[m_level].section == true) { + NOT_IMPLEMENTED_YET(); + } else { + NOT_IMPLEMENTED_YET(); + } } /*