mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-19 02:42:02 +00:00
Code Activity

update backoff for bounded_nla

Browse source
This commit is contained in:
Nikolaj Bjorner 2023-10-21 19:57:06 -07:00
parent 97058b0d5d
commit 53ce18ef34
2 changed files with 16 additions and 14 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -40,7 +40,7 @@ core::core(lp::lar_solver& s, params_ref const& p, reslimit & lim) :
m_use_nra_model(false), m_use_nra_model(false),
m_nra(s, m_nra_lim, *this) m_nra(s, m_nra_lim, *this)
{ {
m_nlsat_delay = lp_settings().nlsat_delay(); // m_nlsat_delay_bound = lp_settings().nlsat_delay();
lra.m_find_monics_with_changed_bounds_func = [&](const indexed_uint_set& columns_with_changed_bounds) { lra.m_find_monics_with_changed_bounds_func = [&](const indexed_uint_set& columns_with_changed_bounds) {
for (lpvar j : columns_with_changed_bounds) { for (lpvar j : columns_with_changed_bounds) {
if (is_monic_var(j)) if (is_monic_var(j))
@ -1550,7 +1550,7 @@ lbool core::check() {
bool run_grobner = need_run_grobner(); bool run_grobner = need_run_grobner();
bool run_horner = need_run_horner(); bool run_horner = need_run_horner();
bool run_bounded_nlsat = should_run_bounded_nlsat(); bool run_bounded_nlsat = should_run_bounded_nlsat();
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 !done() && m_lemmas.empty() && m_literals.empty() && !m_check_feasible; };
@ -1574,6 +1574,9 @@ lbool core::check() {
if (!m_lemmas.empty() || !m_literals.empty()) if (!m_lemmas.empty() || !m_literals.empty())
return l_false; return l_false;
} }
if (no_effect() && run_bounded_nlsat)
ret = bounded_nlsat();
if (no_effect()) if (no_effect())
m_basics.basic_lemma(true); m_basics.basic_lemma(true);
@ -1584,8 +1587,6 @@ lbool core::check() {
if (no_effect()) if (no_effect())
m_divisions.check(); m_divisions.check();
if (no_effect() && run_bounded_nlsat)
ret = bounded_nlsat();
if (no_effect() && ret == l_undef) { if (no_effect() && ret == l_undef) {
std::function<void(void)> check1 = [&]() { m_order.order_lemma(); }; std::function<void(void)> check1 = [&]() { m_order.order_lemma(); };
@ -1623,9 +1624,9 @@ lbool core::check() {
bool core::should_run_bounded_nlsat() { bool core::should_run_bounded_nlsat() {
if (!params().arith_nl_nra()) if (!params().arith_nl_nra())
return false; return false;
if (m_nlsat_delay > m_nlsat_fails) if (m_nlsat_delay > 0)
++m_nlsat_fails; --m_nlsat_delay;
return m_nlsat_delay <= m_nlsat_fails; return m_nlsat_delay < 5;
} }
lbool core::bounded_nlsat() { lbool core::bounded_nlsat() {
@ -1643,11 +1644,12 @@ lbool core::bounded_nlsat() {
m_nra.updt_params(p); m_nra.updt_params(p);
lp_settings().stats().m_nra_calls++; lp_settings().stats().m_nra_calls++;
if (ret == l_undef) if (ret == l_undef)
++m_nlsat_delay; ++m_nlsat_delay_bound;
else { else if (m_nlsat_delay_bound > 0)
m_nlsat_fails = 0; m_nlsat_delay_bound /= 2;
m_nlsat_delay /= 2;
} m_nlsat_delay = m_nlsat_delay_bound;
if (ret == l_true) if (ret == l_true)
clear(); clear();
return ret; return ret;

4
src/math/lp/nla_core.h
View file

@ -60,8 +60,8 @@ class core {
friend class nra::solver; friend class nra::solver;
friend class divisions; friend class divisions;
unsigned m_nlsat_delay = 50; unsigned m_nlsat_delay = 0;
unsigned m_nlsat_fails = 0; unsigned m_nlsat_delay_bound = 0;
bool should_run_bounded_nlsat(); bool should_run_bounded_nlsat();
lbool bounded_nlsat(); lbool bounded_nlsat();