From 6d604b0a79c0b92bbfedf1b6b6410886c639fa18 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Thu, 4 Sep 2025 16:49:15 -1000 Subject: [PATCH] t Signed-off-by: Lev Nachmanson --- src/nlsat/levelwise.cpp | 23 ++++------------------- 1 file changed, 4 insertions(+), 19 deletions(-) diff --git a/src/nlsat/levelwise.cpp b/src/nlsat/levelwise.cpp index b4cd8be07..4cd9461fe 100644 --- a/src/nlsat/levelwise.cpp +++ b/src/nlsat/levelwise.cpp @@ -628,14 +628,7 @@ namespace nlsat { for (unsigned i = 0; i < factors.distinct_factors(); ++i) { polynomial_ref f(m_pm); f = factors[i]; - auto it = std::find_if(m_Q.begin(), m_Q.end(), [f](const property & q) { - return - (q.prop_tag == prop_enum::sgn_inv_irreducible || q.prop_tag == prop_enum::sgn_inv_reducible) && q.poly == f; - }); - if (it != m_Q.end()) //already asserted - return true; - - m_Q.push_back(property(prop_enum::sgn_inv_reducible, f, m_pm)); + add_to_Q_if_new(property(prop_enum::sgn_inv_reducible, f, m_pm)); } erase_from_Q(p); return true; @@ -687,12 +680,8 @@ namespace nlsat { } void apply_pre(const property& p, bool has_repr) { - TRACE(levelwise, - tout << "apply_pre BEGIN m_Q:"; - print_m_Q(tout); - tout << std::endl; - ); - TRACE(levelwise, display(tout << "property p:", p) << std::endl;); + TRACE(levelwise, tout << "apply_pre BEGIN m_Q:"; print_m_Q(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) @@ -701,11 +690,7 @@ namespace nlsat { apply_pre_non_null(p); else NOT_IMPLEMENTED_YET(); - TRACE(levelwise, - tout << "apply_pre END m_Q:"; - print_m_Q(tout); - tout << std::endl; - ); + TRACE(levelwise, tout << "apply_pre END m_Q:"; print_m_Q(tout) << std::endl;); } // return an empty vector on failure, otherwise returns the cell representations with intervals std::vector single_cell() {