From 6c27140bc9dccce09e00cf990c3fcba5c5837eb8 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Thu, 12 Mar 2026 14:35:52 -1000 Subject: [PATCH] Port throttle and soundness fixes from master - Fix soundness: pop incomplete lemma from m_lemmas on add_lemma failure - Gracefully handle root atoms in add_lemma - Throttle check_assignment with failure counter (decrement on success) - Add arith.nl.nra_check_assignment parameter Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> --- src/math/lp/nla_core.cpp | 6 +- src/math/lp/nla_core.h | 1 + src/math/lp/nra_solver.cpp | 95 ++++++++++++++++++-------------- src/params/smt_params_helper.pyg | 1 + 4 files changed, 62 insertions(+), 41 deletions(-) diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp index cda9a3383..a05975d8a 100644 --- a/src/math/lp/nla_core.cpp +++ b/src/math/lp/nla_core.cpp @@ -1330,10 +1330,14 @@ lbool core::check(unsigned level) { return l_false; } - if (no_effect()) { + if (no_effect() && params().arith_nl_nra_check_assignment() && m_check_assignment_fail_cnt < 10) { scoped_limits sl(m_reslim); sl.push_child(&m_nra_lim); ret = m_nra.check_assignment(); + if (ret != l_true) + ++m_check_assignment_fail_cnt; + else + --m_check_assignment_fail_cnt; } if (no_effect() && should_run_bounded_nlsat()) diff --git a/src/math/lp/nla_core.h b/src/math/lp/nla_core.h index e7484396a..8055c5e93 100644 --- a/src/math/lp/nla_core.h +++ b/src/math/lp/nla_core.h @@ -63,6 +63,7 @@ class core { unsigned m_nlsat_delay = 0; unsigned m_nlsat_delay_bound = 0; + unsigned m_check_assignment_fail_cnt = 0; bool should_run_bounded_nlsat(); lbool bounded_nlsat(); diff --git a/src/math/lp/nra_solver.cpp b/src/math/lp/nra_solver.cpp index 82e4c64d7..b6d22bff5 100644 --- a/src/math/lp/nra_solver.cpp +++ b/src/math/lp/nra_solver.cpp @@ -448,48 +448,63 @@ struct solver::imp { lbool add_lemma(nlsat::literal_vector const &clause) { u_map nl2lp = reverse_lp2nl(); polynomial::manager &pm = m_nlsat->pm(); - nla::lemma_builder lemma(m_nla_core, __FUNCTION__); - for (nlsat::literal l : clause) { - if (m_literal2constraint.get((~l).index(), lp::null_ci) != lp::null_ci) { - auto ci = m_literal2constraint[(~l).index()]; - lp::explanation ex; - ex.push_back(ci); - lemma &= ex; - continue; - } - nlsat::atom *a = m_nlsat->bool_var2atom(l.var()); - SASSERT(!a->is_root_atom()); - SASSERT(a->is_ineq_atom()); - auto &ia = *to_ineq_atom(a); - if (ia.size() != 1) { - return l_undef; // factored polynomials not handled here - } - polynomial::polynomial const *p = ia.p(0); - rational bound(0); - lp::lar_term t; - process_polynomial_check_assignment(p, bound, nl2lp, t); + lbool result = l_false; + { + nla::lemma_builder lemma(m_nla_core, __FUNCTION__); + for (nlsat::literal l : clause) { + if (m_literal2constraint.get((~l).index(), lp::null_ci) != lp::null_ci) { + auto ci = m_literal2constraint[(~l).index()]; + lp::explanation ex; + ex.push_back(ci); + lemma &= ex; + continue; + } + nlsat::atom *a = m_nlsat->bool_var2atom(l.var()); + if (a->is_root_atom()) { + result = l_undef; + break; + } + SASSERT(a->is_ineq_atom()); + auto &ia = *to_ineq_atom(a); + if (ia.size() != 1) { + result = l_undef; // factored polynomials not handled here + break; + } + polynomial::polynomial const *p = ia.p(0); + rational bound(0); + lp::lar_term t; + process_polynomial_check_assignment(p, bound, nl2lp, t); - nla::ineq inq(lp::lconstraint_kind::EQ, t, bound); // initial value overwritten in cases below - switch (a->get_kind()) { - case nlsat::atom::EQ: - inq = nla::ineq(l.sign() ? lp::lconstraint_kind::NE : lp::lconstraint_kind::EQ, t, bound); - break; - case nlsat::atom::LT: - inq = nla::ineq(l.sign() ? lp::lconstraint_kind::GE : lp::lconstraint_kind::LT, t, bound); - break; - case nlsat::atom::GT: - inq = nla::ineq(l.sign() ? lp::lconstraint_kind::LE : lp::lconstraint_kind::GT, t, bound); - break; - default: - UNREACHABLE(); - return l_undef; + nla::ineq inq(lp::lconstraint_kind::EQ, t, bound); // initial value overwritten in cases below + switch (a->get_kind()) { + case nlsat::atom::EQ: + inq = nla::ineq(l.sign() ? lp::lconstraint_kind::NE : lp::lconstraint_kind::EQ, t, bound); + break; + case nlsat::atom::LT: + inq = nla::ineq(l.sign() ? lp::lconstraint_kind::GE : lp::lconstraint_kind::LT, t, bound); + break; + case nlsat::atom::GT: + inq = nla::ineq(l.sign() ? lp::lconstraint_kind::LE : lp::lconstraint_kind::GT, t, bound); + break; + default: + UNREACHABLE(); + result = l_undef; + break; + } + if (result == l_undef) + break; + if (m_nla_core.ineq_holds(inq)) { + result = l_undef; + break; + } + lemma |= inq; } - if (m_nla_core.ineq_holds(inq)) - return l_undef; - lemma |= inq; - } - this->m_nla_core.m_check_feasible = true; - return l_false; + if (result == l_false) + this->m_nla_core.m_check_feasible = true; + } // lemma_builder destructor runs here + if (result == l_undef) + m_nla_core.m_lemmas.pop_back(); // discard incomplete lemma + return result; } diff --git a/src/params/smt_params_helper.pyg b/src/params/smt_params_helper.pyg index 451a07964..7ea231f55 100644 --- a/src/params/smt_params_helper.pyg +++ b/src/params/smt_params_helper.pyg @@ -60,6 +60,7 @@ def_module_params(module_name='smt', ('arith.solver', UINT, 6, 'arithmetic solver: 0 - no solver, 1 - bellman-ford based solver (diff. logic only), 2 - simplex based solver, 3 - floyd-warshall based solver (diff. logic only) and no theory combination 4 - utvpi, 5 - infinitary lra, 6 - lra solver'), ('arith.nl', BOOL, True, '(incomplete) nonlinear arithmetic support based on Groebner basis and interval propagation, relevant only if smt.arith.solver=2'), ('arith.nl.nra', BOOL, True, 'call nra_solver when incremental linearization does not produce a lemma, this option is ignored when arith.nl=false, relevant only if smt.arith.solver=6'), + ('arith.nl.nra_check_assignment', BOOL, True, 'call check_assignment in nra_solver to verify current assignment against nlsat constraints'), ('arith.nl.branching', BOOL, True, 'branching on integer variables in non linear clusters'), ('arith.nl.expensive_patching', BOOL, False, 'use the expensive of monomials'), ('arith.nl.rounds', UINT, 1024, 'threshold for number of (nested) final checks for non linear arithmetic, relevant only if smt.arith.solver=2'),