From 6cb86db68e8a6b3d8a55151c5c214656c76f3bc3 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Tue, 2 Sep 2025 12:16:02 -1000 Subject: [PATCH] t Signed-off-by: Lev Nachmanson --- src/nlsat/levelwise.cpp | 16 +++++++++++----- 1 file changed, 11 insertions(+), 5 deletions(-) diff --git a/src/nlsat/levelwise.cpp b/src/nlsat/levelwise.cpp index 00ed363dd..eb1351afd 100644 --- a/src/nlsat/levelwise.cpp +++ b/src/nlsat/levelwise.cpp @@ -514,10 +514,7 @@ namespace nlsat { return ret; } - void apply_pre(const property& p) { - TRACE(levelwise, display(tout << "property p:", p) << std::endl;); - - if (p.prop_tag == prop_enum::an_del) { + void apply_pre_an_del(const property& p) { if (!p.poly) { TRACE(levelwise, tout << "apply_pre: an_del with null poly -> fail" << std::endl;); m_fail = true; @@ -532,6 +529,7 @@ namespace nlsat { if (coeffs_are_zeroes_on_sample(p.poly, m_pm, sample(), m_am)) { TRACE(levelwise, tout << "Rule 4.1: polynomial nullified at sample -> failing" << std::endl;); m_fail = true; + NOT_IMPLEMENTED_YET(); return; } @@ -625,7 +623,15 @@ namespace nlsat { }), m_Q.end()); TRACE(levelwise, tout << "apply_pre: an_del processed and removed from m_Q" << std::endl;); - return; + } + + void apply_pre(const property& p) { + TRACE(levelwise, display(tout << "property p:", p) << std::endl;); + + if (p.prop_tag == prop_enum::an_del) { + apply_pre_an_del(p); + } else { + NOT_IMPLEMENTED_YET(); } } // return an empty vector on failure, otherwise returns the cell representations with intervals