mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 20:18:18 +00:00
Code Activity

refine no-effect predicate to include value of ret

Browse source
This commit is contained in:
Nikolaj Bjorner 2023-12-03 12:41:21 -08:00
parent 9cc2ce42f7
commit 25dd29907b
1 changed files with 7 additions and 10 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

17
src/math/lp/nla_core.cpp
View file

@ -1418,20 +1418,17 @@ void core::patch_monomial(lpvar j) {
void core::patch_monomials_on_to_refine() { void core::patch_monomials_on_to_refine() {
// the rest of the function might change m_to_refine, so have to copy // the rest of the function might change m_to_refine, so have to copy
unsigned_vector to_refine; unsigned_vector to_refine;
for (unsigned j :m_to_refine) { for (unsigned j : m_to_refine)
to_refine.push_back(j); to_refine.push_back(j);
}
unsigned sz = to_refine.size(); unsigned sz = to_refine.size();
unsigned start = random(); 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]); 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() << 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() { void core::patch_monomials() {
@ -1551,7 +1548,7 @@ lbool core::check() {
bool run_horner = need_run_horner(); bool run_horner = need_run_horner();
bool run_bounds = params().arith_nl_branching(); 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()) if (no_effect())
m_monomial_bounds.propagate(); m_monomial_bounds.propagate();
@ -1585,7 +1582,7 @@ lbool core::check() {
if (no_effect()) if (no_effect())
m_divisions.check(); m_divisions.check();
if (no_effect() && ret == l_undef) { if (no_effect()) {
std::function<void(void)> check1 = [&]() { m_order.order_lemma(); }; std::function<void(void)> check1 = [&]() { m_order.order_lemma(); };
std::function<void(void)> check2 = [&]() { m_monotone.monotonicity_lemma(); }; std::function<void(void)> check2 = [&]() { m_monotone.monotonicity_lemma(); };
std::function<void(void)> check3 = [&]() { m_tangents.tangent_lemma(); }; std::function<void(void)> check3 = [&]() { m_tangents.tangent_lemma(); };
@ -1601,7 +1598,7 @@ lbool core::check() {
ret = bounded_nlsat(); ret = bounded_nlsat();
} }
if (no_effect() && params().arith_nl_nra() && ret == l_undef) { if (no_effect() && params().arith_nl_nra()) {
ret = m_nra.check(); ret = m_nra.check();
lp_settings().stats().m_nra_calls++; lp_settings().stats().m_nra_calls++;
} }