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

Add arith.nl.nra_before_lemma_return parameter to try bounded nlsat before returning lemmas

Browse source 
When monomial_bounds.propagate() generates interval-refinement lemmas,
bounded_nlsat() was blocked by the no_effect() gate and never reached.
This caused timeouts on QF_NRA/QF_NIRA/QF_UFNRA problems that nlsat
can solve directly via cylindrical algebraic decomposition.

The new parameter (default true) moves the bounded_nlsat() call before
the early lemma return, allowing nlsat a chance to solve the problem.
Set to false to restore the old behavior.

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
This commit is contained in:
Lev Nachmanson 2026-03-04 12:47:43 -10:00
parent d40c4721d8
commit ec9a87976c
2 changed files with 9 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -1327,12 +1327,18 @@ 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()) {
ret = bounded_nlsat();
if (ret == l_true)
return l_true;
}
if (!m_lemmas.empty() || !m_literals.empty() || m_check_feasible)
return l_false;
}
if (no_effect() && should_run_bounded_nlsat())
if (!params().arith_nl_nra_before_lemma_return() && no_effect() && should_run_bounded_nlsat())
ret = bounded_nlsat();
if (no_effect())

1
src/params/smt_params_helper.pyg
View file

@ -86,6 +86,7 @@ def_module_params(module_name='smt',
('arith.nl.grobner_expand_terms', BOOL, True, 'expand terms before computing grobner basis'),
('arith.nl.reduce_pseudo_linear', BOOL, True, 'create incremental linearization axioms for pseudo-linear monomials'),
('arith.nl.delay', UINT, 10, 'number of calls to final check before invoking bounded nlsat check'),
('arith.nl.nra_before_lemma_return', BOOL, True, 'try bounded nlsat before returning lemmas from monomial bounds propagation'),
('arith.nl.propagate_linear_monomials', BOOL, True, 'propagate linear monomials'),
('arith.nl.optimize_bounds', BOOL, True, 'enable bounds optimization'),
('arith.nl.cross_nested', BOOL, True, 'enable cross-nested consistency checking'),