mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-03-07 05:44:51 +00:00
Code Activity

Throttle early bounded_nlsat to fire every arith.nl.delay NLA calls

Browse source 
The unconditional early call drained rlimit budget on QF_NIA problems
where nlsat returns l_undef. Only try early nlsat every arith.nl.delay
(default 10) NLA calls, combined with the existing exponential backoff.
This preserves the benefit for stuck QF_NRA problems while reducing
overhead on problems where the lemma pipeline is effective.

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
This commit is contained in:
Lev Nachmanson 2026-03-04 13:51:56 -10:00
parent ec9a87976c
commit 73988d7c12
1 changed files with 4 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -1328,7 +1328,10 @@ lbool core::check(unsigned level) {
if (lp_settings().get_cancel_flag())
return l_undef;
if (params().arith_nl_nra_before_lemma_return() && should_run_bounded_nlsat()) {
if (params().arith_nl_nra_before_lemma_return()
&& lp_settings().stats().m_nla_calls > 0
&& lp_settings().stats().m_nla_calls % params().arith_nl_delay() == 0
&& should_run_bounded_nlsat()) {
ret = bounded_nlsat();
if (ret == l_true)
return l_true;