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

use a large delay for nlsat

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-03-14 19:14:44 -07:00
parent 155738088f
commit 845ba7a11e
2 changed files with 10 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -1518,7 +1518,7 @@ lbool core::check(vector<lemma>& l_vec) {
ret = bounded_nlsat(); ret = bounded_nlsat();
if (l_vec.empty() && !done()) { if (l_vec.empty() && !done() && ret == l_undef) {
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(); };
@ -1529,10 +1529,9 @@ lbool core::check(vector<lemma>& l_vec) {
{ 1, check3 }}; { 1, check3 }};
check_weighted(3, checks); check_weighted(3, checks);
if (!conflict_found() && m_nla_settings.run_nra() && should_run_bounded_nlsat() && unsigned num_calls = lp_settings().stats().m_nla_calls;
lp_settings().stats().m_nla_calls > 500) { if (!conflict_found() && m_nla_settings.run_nra() && num_calls % 50 == 0 && num_calls > 500)
ret = bounded_nlsat(); ret = bounded_nlsat();
}
} }
if (l_vec.empty() && !done() && m_nla_settings.run_nra() && ret == l_undef) { if (l_vec.empty() && !done() && m_nla_settings.run_nra() && ret == l_undef) {
@ -1555,6 +1554,8 @@ lbool core::check(vector<lemma>& l_vec) {
} }
bool core::should_run_bounded_nlsat() { bool core::should_run_bounded_nlsat() {
if (!m_nla_settings.run_nra())
return false;
if (m_nlsat_delay > m_nlsat_fails) if (m_nlsat_delay > m_nlsat_fails)
++m_nlsat_fails; ++m_nlsat_fails;
return m_nlsat_delay <= m_nlsat_fails; return m_nlsat_delay <= m_nlsat_fails;
@ -1570,11 +1571,14 @@ lbool core::bounded_nlsat() {
m_nra.updt_params(p); m_nra.updt_params(p);
m_stats.m_nra_calls++; m_stats.m_nra_calls++;
if (ret == l_undef) if (ret == l_undef)
++m_nlsat_delay; ++m_nlsat_delay;
else { else {
m_nlsat_fails = 0; m_nlsat_fails = 0;
m_nlsat_delay /= 2; m_nlsat_delay /= 2;
} }
if (ret == l_true) {
m_lemma_vec->reset();
}
return ret; return ret;
} }

2
src/smt/params/smt_params_helper.pyg
View file

@ -71,7 +71,7 @@ def_module_params(module_name='smt',
('arith.nl.grobner_cnfl_to_report', UINT, 1, 'grobner\'s maximum number of conflicts to report'), ('arith.nl.grobner_cnfl_to_report', UINT, 1, 'grobner\'s maximum number of conflicts to report'),
('arith.nl.gr_q', UINT, 10, 'grobner\'s quota'), ('arith.nl.gr_q', UINT, 10, 'grobner\'s quota'),
('arith.nl.grobner_subs_fixed', UINT, 2, '0 - no subs, 1 - substitute, 2 - substitute fixed zeros only'), ('arith.nl.grobner_subs_fixed', UINT, 2, '0 - no subs, 1 - substitute, 2 - substitute fixed zeros only'),
('arith.nl.delay', UINT, 100, 'number of calls to final check before invoking bounded nlsat check'), ('arith.nl.delay', UINT, 500, 'number of calls to final check before invoking bounded nlsat check'),
('arith.propagate_eqs', BOOL, True, 'propagate (cheap) equalities'), ('arith.propagate_eqs', BOOL, True, 'propagate (cheap) equalities'),
('arith.propagation_mode', UINT, 1, '0 - no propagation, 1 - propagate existing literals, 2 - refine finite bounds'), ('arith.propagation_mode', UINT, 1, '0 - no propagation, 1 - propagate existing literals, 2 - refine finite bounds'),
('arith.reflect', BOOL, True, 'reflect arithmetical operators to the congruence closure'), ('arith.reflect', BOOL, True, 'reflect arithmetical operators to the congruence closure'),