From e62d4e9d50ad91d0ba940dd95d2fb4c377b8c954 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Wed, 4 Mar 2026 14:47:29 -1000 Subject: [PATCH] Gate early bounded_nlsat on real monomials, remove parameter Only call bounded_nlsat before the lemma return when the to-refine set contains real (non-integer) monomials. Integer NLA problems are better served by the lemma pipeline; calling nlsat drains the rlimit budget without benefit. For real NLA (QF_NRA, QF_UFNRA, QF_NIRA with reals), nlsat via CAD is the right approach when bounds propagation is not converging. Remove the arith.nl.nra_before_lemma_return parameter since the has_real_monomial() gate is precise enough. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> --- src/math/lp/nla_core.cpp | 14 +++++++++----- src/math/lp/nla_core.h | 1 + src/params/smt_params_helper.pyg | 1 - 3 files changed, 10 insertions(+), 6 deletions(-) diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp index a306c024a..a883de0a8 100644 --- a/src/math/lp/nla_core.cpp +++ b/src/math/lp/nla_core.cpp @@ -1328,10 +1328,7 @@ lbool core::check(unsigned level) { if (lp_settings().get_cancel_flag()) return l_undef; - 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()) { + if (has_real_monomial() && should_run_bounded_nlsat()) { ret = bounded_nlsat(); if (ret == l_true) return l_true; @@ -1341,7 +1338,7 @@ lbool core::check(unsigned level) { return l_false; } - if (!params().arith_nl_nra_before_lemma_return() && no_effect() && should_run_bounded_nlsat()) + if (no_effect() && should_run_bounded_nlsat()) ret = bounded_nlsat(); if (no_effect()) @@ -1404,6 +1401,13 @@ bool core::should_run_bounded_nlsat() { return m_nlsat_delay < 2; } +bool core::has_real_monomial() const { + for (lpvar j : m_to_refine) + if (!var_is_int(j)) + return true; + return false; +} + lbool core::bounded_nlsat() { params_ref p; lbool ret; diff --git a/src/math/lp/nla_core.h b/src/math/lp/nla_core.h index 5ccbc17e0..1916847b0 100644 --- a/src/math/lp/nla_core.h +++ b/src/math/lp/nla_core.h @@ -65,6 +65,7 @@ class core { unsigned m_nlsat_delay_bound = 0; bool should_run_bounded_nlsat(); + bool has_real_monomial() const; lbool bounded_nlsat(); var_eqs m_evars; diff --git a/src/params/smt_params_helper.pyg b/src/params/smt_params_helper.pyg index 0f8a7675c..451a07964 100644 --- a/src/params/smt_params_helper.pyg +++ b/src/params/smt_params_helper.pyg @@ -86,7 +86,6 @@ 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'),