From 25dd29907b652bd22d2470bc0ca918c4d15a0b70 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 3 Dec 2023 12:41:21 -0800 Subject: [PATCH] refine no-effect predicate to include value of ret --- src/math/lp/nla_core.cpp | 17 +++++++---------- 1 file changed, 7 insertions(+), 10 deletions(-) diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp index 570f51cc5..96f1b4a30 100644 --- a/src/math/lp/nla_core.cpp +++ b/src/math/lp/nla_core.cpp @@ -1418,20 +1418,17 @@ void core::patch_monomial(lpvar j) { void core::patch_monomials_on_to_refine() { // the rest of the function might change m_to_refine, so have to copy unsigned_vector to_refine; - for (unsigned j :m_to_refine) { + for (unsigned j : m_to_refine) to_refine.push_back(j); - } unsigned sz = to_refine.size(); unsigned start = random(); - for (unsigned i = 0; i < sz; i++) { + for (unsigned i = 0; i < sz && !m_to_refine.empty(); i++) patch_monomial(to_refine[(start + i) % sz]); - if (m_to_refine.size() == 0) - break; - } + TRACE("nla_solver", tout << "sz = " << sz << ", m_to_refine = " << m_to_refine.size() << - (sz > m_to_refine.size()? " less" : "same" ) << "\n";); + (sz > m_to_refine.size()? " less" : " same" ) << "\n";); } void core::patch_monomials() { @@ -1551,7 +1548,7 @@ lbool core::check() { bool run_horner = need_run_horner(); bool run_bounds = params().arith_nl_branching(); - auto no_effect = [&]() { return !done() && m_lemmas.empty() && m_literals.empty() && !m_check_feasible; }; + auto no_effect = [&]() { return ret == l_undef && !done() && m_lemmas.empty() && m_literals.empty() && !m_check_feasible; }; if (no_effect()) m_monomial_bounds.propagate(); @@ -1585,7 +1582,7 @@ lbool core::check() { if (no_effect()) m_divisions.check(); - if (no_effect() && ret == l_undef) { + if (no_effect()) { std::function check1 = [&]() { m_order.order_lemma(); }; std::function check2 = [&]() { m_monotone.monotonicity_lemma(); }; std::function check3 = [&]() { m_tangents.tangent_lemma(); }; @@ -1601,7 +1598,7 @@ lbool core::check() { ret = bounded_nlsat(); } - if (no_effect() && params().arith_nl_nra() && ret == l_undef) { + if (no_effect() && params().arith_nl_nra()) { ret = m_nra.check(); lp_settings().stats().m_nra_calls++; }