From ad278c5fdcada72909fd7af68c393e22be6ef094 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Fri, 22 May 2026 08:53:07 -0700 Subject: [PATCH] remove an option and cache expansion sizes Signed-off-by: Lev Nachmanson --- src/math/lp/nra_solver.cpp | 45 +++++++++++--------------------- src/params/smt_params_helper.pyg | 1 - 2 files changed, 15 insertions(+), 31 deletions(-) diff --git a/src/math/lp/nra_solver.cpp b/src/math/lp/nra_solver.cpp index 743d2cd65..fe787d5e9 100644 --- a/src/math/lp/nra_solver.cpp +++ b/src/math/lp/nra_solver.cpp @@ -419,40 +419,25 @@ struct solver::imp { statistics &st = m_nla_core.lp_settings().stats().m_st; - // Choose the falsified constraint to send to NLSAT according to - // arith.nl.nra_check_assignment_pick. In both modes we visit COI - // constraints in an order that lets us stop at the first - // falsified one rather than evaluating every constraint. - // - // 0 - sort COI constraints by ascending substitution-expansion - // size (a structural, model-independent measure that acts - // as a cheap LRA-side proxy for the lowest-degree-in-max- - // var heuristic of nlsat::solver::check(rvalues, clause)). - // The first falsified one we hit therefore has the minimum - // expansion size among all falsified candidates. - // - // 1 - Fisher-Yates shuffle the COI constraints and pick the - // first falsified one. Restricted to the falsified subset - // a uniform permutation induces a uniform first-element - // distribution, so the picked constraint is uniformly - // random among falsified. + // Sort COI constraints by ascending substitution-expansion size + // (a structural, model-independent measure that acts as a cheap + // LRA-side proxy for the lowest-degree-in-max-var heuristic of + // nlsat::solver::check(rvalues, clause)). The first falsified + // constraint we hit therefore has the minimum expansion size + // among all falsified candidates. Cache the expansion size for + // each constraint up front so the comparator is O(1). svector coi_constraints; for (auto ci : m_coi.constraints()) coi_constraints.push_back(ci); - unsigned pick_mode = m_nla_core.params().arith_nl_nra_check_assignment_pick(); - if (pick_mode == 1) { - for (unsigned i = coi_constraints.size(); i-- > 1; ) { - unsigned j = m_nla_core.random() % (i + 1); - std::swap(coi_constraints[i], coi_constraints[j]); - } - } - else { - std::stable_sort(coi_constraints.begin(), coi_constraints.end(), - [&](lp::constraint_index a, lp::constraint_index b) { - return constraint_expansion_size(a) < constraint_expansion_size(b); - }); - } + u_map expansion_size_cache; + for (auto ci : coi_constraints) + expansion_size_cache.insert(ci, constraint_expansion_size(ci)); + + std::stable_sort(coi_constraints.begin(), coi_constraints.end(), + [&](lp::constraint_index a, lp::constraint_index b) { + return expansion_size_cache[a] < expansion_size_cache[b]; + }); u_map sub_cache; lp::constraint_index best = lp::null_ci; diff --git a/src/params/smt_params_helper.pyg b/src/params/smt_params_helper.pyg index 204bc0e80..6c8ce796d 100644 --- a/src/params/smt_params_helper.pyg +++ b/src/params/smt_params_helper.pyg @@ -63,7 +63,6 @@ def_module_params(module_name='smt', ('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.nra_check_assignment_max_fail', UINT, 7, 'maximum consecutive check_assignment failures before disabling it'), - ('arith.nl.nra_check_assignment_pick', UINT, 0, 'falsified-literal selection in check_assignment: 0 - minimal degree (size) of the max variable (default), 1 - random'), ('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'),