From ec9a87976c6e6e102a052aa59350b3f8888bfdfa Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Wed, 4 Mar 2026 12:47:43 -1000 Subject: [PATCH] Add arith.nl.nra_before_lemma_return parameter to try bounded nlsat before returning lemmas 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> --- src/math/lp/nla_core.cpp | 10 ++++++++-- src/params/smt_params_helper.pyg | 1 + 2 files changed, 9 insertions(+), 2 deletions(-) diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp index c7a29e9a7..1c8d2e832 100644 --- a/src/math/lp/nla_core.cpp +++ b/src/math/lp/nla_core.cpp @@ -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()) diff --git a/src/params/smt_params_helper.pyg b/src/params/smt_params_helper.pyg index 451a07964..0f8a7675c 100644 --- a/src/params/smt_params_helper.pyg +++ b/src/params/smt_params_helper.pyg @@ -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'),