From 63db413a86b3043686ef7be4be0a0c689335154d Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Fri, 5 Sep 2025 10:37:01 -1000 Subject: [PATCH] t Signed-off-by: Lev Nachmanson --- src/nlsat/levelwise.cpp | 28 +++++++++++++++++----------- 1 file changed, 17 insertions(+), 11 deletions(-) diff --git a/src/nlsat/levelwise.cpp b/src/nlsat/levelwise.cpp index 6569a6fd5..2535079b9 100644 --- a/src/nlsat/levelwise.cpp +++ b/src/nlsat/levelwise.cpp @@ -687,17 +687,23 @@ namespace nlsat { void apply_pre(const property& p, bool has_repr) { TRACE(levelwise, tout << "apply_pre BEGIN m_Q:"; display(tout) << std::endl; display(tout << "pre p:", p) << std::endl;); - if (p.prop_tag == prop_enum::an_del) - apply_pre_an_del(p); - else if (p.prop_tag == prop_enum::connected) - apply_pre_connected(p,has_repr); - else if (p.prop_tag == prop_enum::non_null) - apply_pre_non_null(p); - else if (p.prop_tag == prop_enum::an_sub) - apply_pre_an_sub(p); - else - NOT_IMPLEMENTED_YET(); - + switch (p.prop_tag) { + case prop_enum::an_del: + apply_pre_an_del(p); + break; + case prop_enum::connected: + apply_pre_connected(p, has_repr); + break; + case prop_enum::non_null: + apply_pre_non_null(p); + break; + case prop_enum::an_sub: + apply_pre_an_sub(p); + break; + default: + NOT_IMPLEMENTED_YET(); + break; + } TRACE(levelwise, tout << "apply_pre END m_Q:"; display(tout) << std::endl;); } // return an empty vector on failure, otherwise returns the cell representations with intervals