diff --git a/src/math/lp/lar_solver.h b/src/math/lp/lar_solver.h index 73ada4f1dd..1f83e3272c 100644 --- a/src/math/lp/lar_solver.h +++ b/src/math/lp/lar_solver.h @@ -109,6 +109,7 @@ class lar_solver : public column_namer { bool sizes_are_correct() const; bool implied_bound_is_correctly_explained(implied_bound const& be, const vector>& explanation) const; +public: template unsigned calculate_implied_bounds_for_row(unsigned row_index, lp_bound_propagator& bp) { if (A_r().m_rows[row_index].size() > settings().max_row_length_for_bound_propagation || row_has_a_big_num(row_index)) @@ -119,6 +120,7 @@ class lar_solver : public column_namer { zero_of_type>(), bp); } +private: static void clean_popped_elements_for_heap(unsigned n, lpvar_heap& set); static void clean_popped_elements(unsigned n, indexed_uint_set& set); diff --git a/src/math/lp/lp_settings.h b/src/math/lp/lp_settings.h index bc1f2044f5..60fa740c96 100644 --- a/src/math/lp/lp_settings.h +++ b/src/math/lp/lp_settings.h @@ -124,6 +124,7 @@ struct statistics { unsigned m_nla_add_bounds = 0; unsigned m_nla_propagate_bounds = 0; unsigned m_nla_propagate_eq = 0; + unsigned m_nla_propagate_row_bounds = 0; unsigned m_nla_lemmas = 0; unsigned m_nra_calls = 0; unsigned m_nla_bounds_improvements = 0; @@ -173,6 +174,7 @@ struct statistics { st.update("arith-nla-add-bounds", m_nla_add_bounds); st.update("arith-nla-propagate-bounds", m_nla_propagate_bounds); st.update("arith-nla-propagate-eq", m_nla_propagate_eq); + st.update("arith-nla-propagate-row-bounds", m_nla_propagate_row_bounds); st.update("arith-nla-lemmas", m_nla_lemmas); st.update("arith-nra-calls", m_nra_calls); st.update("arith-bounds-improvements", m_nla_bounds_improvements); diff --git a/src/math/lp/monomial_bounds.cpp b/src/math/lp/monomial_bounds.cpp index eab39c9d01..7465f1b593 100644 --- a/src/math/lp/monomial_bounds.cpp +++ b/src/math/lp/monomial_bounds.cpp @@ -11,6 +11,7 @@ #include "math/lp/nla_core.h" #include "math/lp/nla_intervals.h" #include "math/lp/numeric_pair.h" +#include "math/lp/lp_bound_propagator.h" namespace nla { @@ -580,8 +581,8 @@ namespace nla { rational U(dep.upper(range)); if (U.root(p, r) && improves_upper(r)) { auto cmp = dep.upper_is_open(range) ? llc::LT : llc::LE; - propagate_lp_bound(v, cmp, r, dep.get_upper_dep(range)); - tightened = true; + if (propagate_lp_bound(v, cmp, r, dep.get_upper_dep(range))) + tightened = true; } } // Even power, v known non-positive: range.lower gives v <= -root(p, L). @@ -592,8 +593,8 @@ namespace nla { auto cmp = dep.lower_is_open(range) ? llc::LT : llc::LE; u_dependency* d = c().lra.join_deps(dep.get_lower_dep(range), c().lra.get_column_upper_bound_witness(v)); - propagate_lp_bound(v, cmp, -r, d); - tightened = true; + if (propagate_lp_bound(v, cmp, -r, d)) + tightened = true; } } return tightened; @@ -624,8 +625,8 @@ namespace nla { rational L(dep.lower(range)); if (L.root(p, r) && improves_lower(r)) { auto cmp = dep.lower_is_open(range) ? llc::GT : llc::GE; - propagate_lp_bound(v, cmp, r, dep.get_lower_dep(range)); - tightened = true; + if (propagate_lp_bound(v, cmp, r, dep.get_lower_dep(range))) + tightened = true; } } return tightened; @@ -635,8 +636,8 @@ namespace nla { rational U(dep.upper(range)); if (!U.is_neg() && U.root(p, r) && improves_lower(-r)) { auto cmp = dep.upper_is_open(range) ? llc::GT : llc::GE; - propagate_lp_bound(v, cmp, -r, dep.get_upper_dep(range)); - tightened = true; + if (propagate_lp_bound(v, cmp, -r, dep.get_upper_dep(range))) + tightened = true; } } // Even power, v known non-negative: range.lower gives v >= root(p, L). @@ -647,8 +648,8 @@ namespace nla { auto cmp = dep.lower_is_open(range) ? llc::GT : llc::GE; u_dependency* d = c().lra.join_deps(dep.get_lower_dep(range), c().lra.get_column_lower_bound_witness(v)); - propagate_lp_bound(v, cmp, r, d); - tightened = true; + if (propagate_lp_bound(v, cmp, r, d)) + tightened = true; } } return tightened; @@ -657,8 +658,16 @@ namespace nla { /** * Ensure that bounds are integral when the variable is integer. */ - void monomial_bounds::propagate_lp_bound(lpvar v, lp::lconstraint_kind cmp, rational const &q, u_dependency *d) { + bool monomial_bounds::propagate_lp_bound(lpvar v, lp::lconstraint_kind cmp, rational const &q, u_dependency *d) { SASSERT(cmp != llc::EQ && cmp != llc::NE); + // Global cap on derived-bound magnitude. Interval up-propagation can + // double the bit-width of bounds at every propagation round (a product + // bound is the product of factor bounds, which may themselves be + // derived); unchecked this ends in single mpn multiplications so large + // that even the -T watchdog cannot preempt them. + unsigned const max_bits = c().params().arith_nl_propagate_row_bounds_max_bits(); + if (max_bits > 0 && q.bitsize() > max_bits) + return false; if (!c().var_is_int(v)) c().lra.update_column_type_and_bound(v, cmp, q, d); else if (q.is_int()) { @@ -673,6 +682,7 @@ namespace nla { c().lra.update_column_type_and_bound(v, llc::GE, ceil(q), d); else c().lra.update_column_type_and_bound(v, llc::LE, floor(q), d); + return true; } bool monomial_bounds::tighten_lp_bound(dep_interval const &range, lpvar v, unsigned power) { @@ -748,6 +758,156 @@ namespace nla { return propagated; } + namespace { + // Minimal consumer for lar_solver::calculate_implied_bounds_for_row: + // accepts only bounds that improve a column of interest. + struct nl_row_bound_imp { + lp::lar_solver& m_lp; + indexed_uint_set const& m_relevant; + // When false, only bounds for sides the column lacks entirely are + // accepted; when true, improvements of existing bounds also pass. + bool m_allow_improvements = false; + nl_row_bound_imp(lp::lar_solver& l, indexed_uint_set const& r) : m_lp(l), m_relevant(r) {} + lp::lar_solver& lp() { return m_lp; } + const lp::lar_solver& lp() const { return m_lp; } + bool bound_is_interesting(unsigned j, lp::lconstraint_kind kind, const lp::mpq& v) const { + if (!m_relevant.contains(j)) + return false; + switch (kind) { + case lp::lconstraint_kind::GE: + case lp::lconstraint_kind::GT: + if (!m_lp.column_has_lower_bound(j)) + return true; + return m_allow_improvements && v > m_lp.get_lower_bound(j).x; + case lp::lconstraint_kind::LE: + case lp::lconstraint_kind::LT: + if (!m_lp.column_has_upper_bound(j)) + return true; + return m_allow_improvements && v < m_lp.get_upper_bound(j).x; + default: + return false; + } + } + }; + } + + /** + \brief Assert row-implied bounds of nonlinear-relevant columns as LP + column bounds. + + This is the one-sided generalization of propagate_fixed_rows, and the + nla counterpart of theory_arith's implied-bound propagation: solver 2 + asserts a bound derived from a row (say, x <= 2^32 - 1 out of the row + of (< (mod a p) p) once p is fixed at 2^32) directly into its tableau, + where it feeds the interval engine, bounds the monomials containing x, + and lets a plain farkas conflict refute the query without Grobner, + Horner or nlsat. theory_lra only turns implied bounds into literals + when a matching atom exists, so without this pass such bounds never + reach the LP columns and interval propagation of products starves. + + Only columns occurring in a monomial are touched, mirroring + propagate_fixed_rows: the point is enabling nonlinear reasoning, not + general bound strengthening. + */ + bool monomial_bounds::propagate_row_implied_bounds(bool incremental) { + if (!c().params().arith_nl_propagate_row_bounds()) + return false; + auto& lra = c().lra; + + // At a final check, restrict attention to the monomials that are + // violated in the current model: their variables and factors are the + // columns whose missing bounds starve interval propagation, and the + // rows adjacent to those columns are where the bounds are implied + // (e.g. the row of (< (mod a p) p) implies mod <= 2^32 - 1 once p is + // fixed at 2^32). During search (incremental) the trigger is instead + // a column whose bounds changed since the last propagation - the same + // trigger theory_arith uses - and the candidate columns are all + // monomial variables and factors. + indexed_uint_set nl_vars; + indexed_uint_set rows; + if (incremental) { + for (auto const& m : c().emons()) { + nl_vars.insert(m.var()); + for (lpvar k : m.vars()) + nl_vars.insert(k); + } + for (lpvar j : c().m_columns_with_changed_bounds) { + if (j >= lra.column_count()) + continue; + for (auto const& cell : lra.A_r().m_columns[j]) + rows.insert(cell.var()); + } + } + else { + for (lpvar v : c().m_to_refine) { + auto const& m = c().emons()[v]; + nl_vars.insert(m.var()); + for (lpvar k : m.vars()) + nl_vars.insert(k); + } + for (lpvar j : nl_vars) + for (auto const& cell : lra.A_r().m_columns[j]) + rows.insert(cell.var()); + } + if (rows.empty()) + return false; + + // Two escalation levels. Level 1 only fills in sides the columns lack + // altogether - the least invasive repair of starved interval + // propagation, and usually all that effectively-linear problems need. + // Only when that yields nothing does level 2 also assert improvements + // of existing bounds, which drives the full cascade (factor bounds -> + // product bounds -> farkas) at the price of perturbing the search. + nl_row_bound_imp imp(lra, nl_vars); + std_vector ibounds; + bool propagated = false; + for (bool allow_improvements : { false, true }) { + // The incremental variant never escalates: during search only the + // level-1 repairs (missing-side bounds out of fixed-anchored rows) + // are quiet enough to assert on every propagation round. + if (allow_improvements && (incremental || !c().params().arith_nl_propagate_row_bounds_improve())) + break; + imp.m_allow_improvements = allow_improvements; + ibounds.clear(); + lp::lp_bound_propagator bp(imp, ibounds); + bp.init(); + for (unsigned i : rows) { + // At the default level only rows anchored by a fixed column are + // analyzed: a fixed factor (a pow2 constant, a determined + // length) is what turns the row into a bound on the remaining + // nonlinear column - the linearization signature this pass is + // after. Rows without a fixed column mostly contribute noise. + if (!allow_improvements) { + bool has_fixed = false; + for (auto const& cell : lra.get_row(i)) + if (lra.column_is_fixed(cell.var())) { + has_fixed = true; + break; + } + if (!has_fixed) + continue; + } + lra.calculate_implied_bounds_for_row(i, bp); + } + + for (auto const& ib : ibounds) { + lpvar j = ib.m_j; + // For term slack columns m_j is a term index, not a column; + // those never pass the nl_vars filter, but be defensive anyway. + if (j >= lra.column_count() || !nl_vars.contains(j)) + continue; + u_dependency* d = ib.explain_implied(); + if (!propagate_lp_bound(j, ib.kind(), ib.m_bound, d)) + continue; + ++c().lra.settings().stats().m_nla_propagate_row_bounds; + propagated = true; + } + if (propagated) + break; + } + return propagated; + } + // ================================================================ // max_min: incremental LP bound optimization. // diff --git a/src/math/lp/monomial_bounds.h b/src/math/lp/monomial_bounds.h index c88285ff53..030a94187c 100644 --- a/src/math/lp/monomial_bounds.h +++ b/src/math/lp/monomial_bounds.h @@ -22,7 +22,7 @@ namespace nla { bool tighten_lp_lower_bound(dep_interval const& range, lpvar v, unsigned p); bool tighten_lp_bound(dep_interval &mi, lpvar v, unsigned power, dep_interval &product); - void propagate_lp_bound(lpvar v, lp::lconstraint_kind cmp, rational const &q, u_dependency *d); + bool propagate_lp_bound(lpvar v, lp::lconstraint_kind cmp, rational const &q, u_dependency *d); bool should_propagate_lower(dep_interval const& range, lpvar v, unsigned p); @@ -91,6 +91,7 @@ namespace nla { bool propagate_linear_bounds(); bool propagate_changed_bounds(); bool propagate_fixed_rows(); + bool propagate_row_implied_bounds(bool incremental); // Maximize (is_lower == false) or minimize (is_lower == true) column j // over the LP tableau and, if the resulting bound improves j's current diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp index 66224d24ba..4f6f33e228 100644 --- a/src/math/lp/nla_core.cpp +++ b/src/math/lp/nla_core.cpp @@ -45,9 +45,10 @@ core::core(lp::lar_solver& s, params_ref const& p, reslimit & lim) : m_nlsat_delay_bound = lp_settings().nlsat_delay(); lra.m_find_monics_with_changed_bounds_func = [&](const indexed_uint_set& columns_with_changed_bounds) { for (lpvar j : columns_with_changed_bounds) { + m_columns_with_changed_bounds.insert(j); if (is_monic_var(j)) m_monics_with_changed_bounds.insert(j); - for (const auto & m: m_emons.get_use_list(j)) + for (const auto & m: m_emons.get_use_list(j)) m_monics_with_changed_bounds.insert(m.var()); } }; @@ -648,7 +649,7 @@ void core::init_to_refine() { unsigned r = random(), sz = m_emons.number_of_monics(); for (unsigned k = 0; k < sz; ++k) { auto const & m = *(m_emons.begin() + (k + r)% sz); - if (!check_monic(m)) + if (!check_monic(m)) insert_to_refine(m.var()); } @@ -1185,9 +1186,11 @@ void core::patch_monomial(lpvar j) { // We could not patch j, now we try patching the factor variables. TRACE(nla_solver, tout << " trying squares\n";); // handle perfect squares - if ((*m_patched_monic).vars().size() == 2 && (*m_patched_monic).vars()[0] == (*m_patched_monic).vars()[1]) { + if ((*m_patched_monic).vars().size() == 2 && (*m_patched_monic).vars()[0] == (*m_patched_monic).vars()[1]) { rational root; - if (v.is_perfect_square(root)) { + // is_perfect_square multiplies numbers of v's magnitude; on the huge + // values that bound propagation can produce it dominates the run time. + if (v.bitsize() <= 256 && v.is_perfect_square(root)) { m_patched_var = (*m_patched_monic).vars()[0]; if (!var_breaks_correct_monic(m_patched_var) && (try_to_patch(root) || try_to_patch(-root))) { TRACE(nla_solver, tout << "patched square\n";); @@ -1305,14 +1308,24 @@ lbool core::check(unsigned level) { init_to_refine(); patch_monomials(); - set_use_nra_model(false); + set_use_nra_model(false); if (m_to_refine.empty()) - return l_true; + return l_true; init_search(); m_nla_satisfied = false; lbool ret = l_undef; - bool run_grobner = need_run_grobner(); + // Optionally defer the Grobner basis while bound propagation is still + // delivering: solver 2 never reaches its Grobner strategy on + // effectively-linear problems because interval propagation reports + // progress at every call. The deferral cuts Grobner invocations ~7x and + // the seed-tail ~40% on the F* UInt128 family, but it also starves the + // Grobner lemmas that alone close Pulse.Lib.ForEvery-1 (a query solver 2 + // cannot solve at all), so it is opt-in rather than default. + bool bounds_active = m_bounds_progress_since_check > 0 && + params().arith_nl_grobner_defer_on_bounds_progress(); + m_bounds_progress_since_check = 0; + bool run_grobner = need_run_grobner() && !bounds_active; bool run_horner = need_run_horner(); bool run_bounds = params().arith_nl_branching(); @@ -1323,8 +1336,21 @@ lbool core::check(unsigned level) { if (no_effect() && refine_pseudo_linear()) return l_false; - - + + // Pre-empt the lemma machinery when the violated monomials carry the + // effectively-linear signature. The pass itself is the detector: at its + // default level it only asserts bounds for sides a column lacks entirely, + // implied by rows anchored on a fixed column (a pow2 constant, a + // determined length). When such bounds exist - the situation solver 2 + // handles by pure bound propagation - asserting them and letting the + // simplex continue beats deriving Grobner/Horner lemmas over the same + // fixed constants. When the pass asserts nothing, the machinery below + // runs exactly as before. + if (no_effect() && m_monomial_bounds.propagate_row_implied_bounds(false)) { + m_check_feasible = true; + return l_false; + } + { std::function check1 = [&]() { if (no_effect() && run_horner) m_horner.horner_lemmas(); }; std::function check2 = [&]() { if (no_effect() && run_grobner) m_grobner(); }; @@ -1430,10 +1456,15 @@ lbool core::bounded_nlsat() { p.set_uint("max_conflicts", lp_settings().m_max_conflicts); m_nra.updt_params(p); lp_settings().stats().m_nra_calls++; - if (ret == l_undef) - ++m_nlsat_delay_bound; + if (ret == l_undef) { + // Exponential backoff: a query that bounded nlsat cannot decide within + // its conflict budget tends to stay undecidable on the next model as + // well; a linear delay lets the search sink seconds into repeated + // fruitless nlsat calls (each one costs up to 100 conflicts). + m_nlsat_delay_bound = m_nlsat_delay_bound == 0 ? 4 : std::min(2 * m_nlsat_delay_bound, 1u << 20); + } else if (m_nlsat_delay_bound > 0) - m_nlsat_delay_bound /= 2; + m_nlsat_delay_bound /= 2; m_nlsat_delay = m_nlsat_delay_bound; @@ -1545,9 +1576,10 @@ bool core::propagate() { propagated = true; if (m_monomial_bounds.tighten_lp_bounds()) propagated = true; - if (m_monomial_bounds.propagate_changed_bounds()) + if (m_monomial_bounds.propagate_changed_bounds()) propagated = true; m_monics_with_changed_bounds.reset(); + m_columns_with_changed_bounds.reset(); if (propagated) m_check_feasible = true; return propagated; @@ -1556,12 +1588,17 @@ bool core::propagate() { bool core::incremental_propagate() { bool propagated = false; clear(); + if (m_monomial_bounds.propagate_row_implied_bounds(true)) { + propagated = true; + ++m_bounds_progress_since_check; + } if (m_monomial_bounds.propagate_changed_bounds()) propagated = true; m_monics_with_changed_bounds.reset(); + m_columns_with_changed_bounds.reset(); if (propagated) m_check_feasible = true; - return propagated; + return propagated; } /** diff --git a/src/math/lp/nla_core.h b/src/math/lp/nla_core.h index 81976f07a5..eb92641f02 100644 --- a/src/math/lp/nla_core.h +++ b/src/math/lp/nla_core.h @@ -80,6 +80,12 @@ class core { vector m_fixed_equalities; indexed_uint_set m_to_refine; indexed_uint_set m_monics_with_changed_bounds; + indexed_uint_set m_columns_with_changed_bounds; + // Bound-propagation progress (incremental or pre-check) accumulated since + // the last final check; while non-zero, the Grobner basis is deferred, + // mirroring solver 2, whose strategy ladder never advances past interval + // propagation as long as it keeps deriving bounds. + unsigned m_bounds_progress_since_check = 0; tangents m_tangents; basics m_basics; order m_order; diff --git a/src/math/lp/nla_grobner.cpp b/src/math/lp/nla_grobner.cpp index 609edf96c2..58aefb5d06 100644 --- a/src/math/lp/nla_grobner.cpp +++ b/src/math/lp/nla_grobner.cpp @@ -375,6 +375,16 @@ namespace nla { eval.var2val() = [&](unsigned j) { return val(j); }; if (eval(p) == 0) return false; + // Divisibility and quotient branching is effective for small moduli but + // hopeless for huge ones: a residue lemma modulo 2^32 (coefficients of + // that scale typically enter the polynomial by substitution of fixed + // power-of-two constants) refutes just the current model out of billions + // and only churns the search. Skip when any coefficient is that large. + unsigned const max_bits = c().params().arith_nl_grobner_quotient_max_bits(); + if (max_bits > 0) + for (auto const& mn : p) + if (mn.coeff.bitsize() > max_bits) + return false; TRACE(grobner, tout << "propagate_quotients " << p << "\n"); tracked_uint_set nl_vars; rational d(1); @@ -996,6 +1006,16 @@ namespace nla { } } + // A fixed variable is substituted by its value only when the value is small. + // Substituting huge constants (e.g. 2^32 from pow2 tables) drives the basis + // computation into large-coefficient arithmetic; such variables stay symbolic. + bool grobner::fixed_value_is_small(lpvar j) const { + unsigned max_bits = c().params().arith_nl_grobner_subs_fixed_max_bits(); + if (max_bits == 0) + return true; + return lra.column_lower_bound(j).x.bitsize() <= max_bits; + } + const rational& grobner::val_of_fixed_var_with_deps(lpvar j, u_dependency*& dep) { auto* d = lra.get_bound_constraint_witnesses_for_column(j); if (d) @@ -1024,7 +1044,7 @@ namespace nla { dep = zero_dep; return r; } - if (c().params().arith_nl_grobner_subs_fixed() == 1 && c().var_is_fixed(j)) + if (c().params().arith_nl_grobner_subs_fixed() == 1 && c().var_is_fixed(j) && fixed_value_is_small(j)) r *= val_of_fixed_var_with_deps(j, dep); else if (m_config.m_expand_terms && c().lra.column_has_term(j)) r *= pdd_expr(c().lra.get_term(j), dep); diff --git a/src/math/lp/nla_grobner.h b/src/math/lp/nla_grobner.h index 62877836dc..0b796510de 100644 --- a/src/math/lp/nla_grobner.h +++ b/src/math/lp/nla_grobner.h @@ -97,6 +97,7 @@ namespace nla { bool is_solved(dd::pdd const& p, unsigned& v, dd::pdd& r); void add_eq(dd::pdd& p, u_dependency* dep); bool is_pseudo_linear(monic const& m) const; + bool fixed_value_is_small(lpvar j) const; const rational& val_of_fixed_var_with_deps(lpvar j, u_dependency*& dep); dd::pdd pdd_expr(const rational& c, lpvar j, u_dependency*& dep); dd::pdd pdd_expr(lp::lar_term const& t, u_dependency*& dep); diff --git a/src/params/smt_params_helper.pyg b/src/params/smt_params_helper.pyg index 5f65fa6ce2..6b47ad3b2a 100644 --- a/src/params/smt_params_helper.pyg +++ b/src/params/smt_params_helper.pyg @@ -87,11 +87,14 @@ def_module_params(module_name='smt', ('arith.nl.grobner_max_simplified', UINT, 10000, 'grobner\'s maximum number of simplifications'), ('arith.nl.grobner_cnfl_to_report', UINT, 1, 'grobner\'s maximum number of conflicts to report'), ('arith.nl.grobner_propagate_quotients', BOOL, True, 'detect conflicts x*y + z = 0 where x doesn\'t divide z'), + ('arith.nl.grobner_quotient_max_bits', UINT, 0, 'skip quotient/mod-residue lemmas when a polynomial coefficient exceeds this bit-size (0 = no limit); huge moduli make divisibility branching unproductive'), ('arith.nl.grobner_gcd_test', BOOL, True, 'detect gcd conflicts for polynomial powers x^k - y = 0'), ('arith.nl.grobner_exp_delay', BOOL, True, 'use exponential delay between grobner basis attempts'), + ('arith.nl.grobner_defer_on_bounds_progress', BOOL, False, 'defer the grobner basis while nonlinear bound propagation is still making progress between final checks; mirrors the legacy solver, which never reaches grobner while interval propagation delivers; reduces seed-tail latency on effectively-linear problems at the price of starving grobner-dependent queries'), ('arith.nl.grobner_adaptive', BOOL, False, 'scale grobner growth knobs (eqs/size/degree/max_simplified) up on productive runs and down on misses'), ('arith.nl.gr_q', UINT, 10, 'grobner\'s quota'), - ('arith.nl.grobner_subs_fixed', UINT, 1, '0 - no subs, 1 - substitute, 2 - substitute fixed zeros only'), + ('arith.nl.grobner_subs_fixed', UINT, 1, '0 - no subs, 1 - substitute, 2 - substitute fixed zeros only'), + ('arith.nl.grobner_subs_fixed_max_bits', UINT, 0, 'with grobner_subs_fixed=1, substitute a non-zero fixed variable only when the bit-size of its value is at most this bound (0 = no limit); larger fixed values stay symbolic to avoid large-coefficient growth in the basis'), ('arith.nl.grobner_expand_terms', BOOL, True, 'expand terms before computing grobner basis'), ('arith.nl.grobner_perfect_squares', BOOL, True, 'expand perfect squares with Grobner'), ('arith.nl.monomial_sandwich', BOOL, False, 'derive bound on a monomial factor by pairing two LP rows that share the other factor'), @@ -101,7 +104,12 @@ def_module_params(module_name='smt', ('arith.nl.delay', UINT, 10, 'number of calls to final check before invoking bounded nlsat check'), ('arith.nl.propagate_linear_monomials', BOOL, True, 'propagate linear monomials'), ('arith.nl.optimize_bounds', BOOL, True, 'enable bounds optimization'), - ('arith.nl.propagate_fixed_rows', BOOL, False, 'scan LP rows for fixed variables'), + ('arith.nl.propagate_fixed_rows', BOOL, False, 'scan LP rows for fixed variables'), + ('arith.nl.propagate_row_bounds', BOOL, True, 'assert row-implied bounds of variables occurring in nonlinear monomials as LP column bounds; lets interval propagation bound products and linearize without running grobner/horner/nlsat'), + ('arith.nl.propagate_row_bounds_max_bits', UINT, 256, 'do not assert a derived bound whose value exceeds this bit-size; caps the multiplicative growth of derived bounds (0 = no limit)'), + ('arith.nl.propagate_row_bounds_improve', BOOL, False, 'when row-implied bound propagation finds no missing-side bounds, also assert improvements of existing bounds; drives the full bound cascade so the F*-style effectively-linear queries refute without grobner/horner/nlsat, at the price of perturbing searches that were healthy'), + ('arith.nl.linear_probe', BOOL, False, 'before the main SMT search, probe the query with a short bounds-only solver (no grobner/horner/nlsat, row-implied bound propagation with improvements); decides effectively-linear nonlinear queries at a fraction of the cost, falls through to the unchanged main search otherwise'), + ('arith.nl.linear_probe_timeout', UINT, 300, 'wall-clock budget of the bounds-only linear probe, in milliseconds'), ('arith.nl.optimize_bounds_lp_max_vars', UINT, 120, 'skip LP-based nonlinear bounds optimization when the number of candidate monomial variables exceeds this threshold (0 = unlimited)'), ('arith.nl.cross_nested', BOOL, True, 'enable cross-nested consistency checking'), ('arith.nl.log', BOOL, False, 'Log lemmas sent to nra solver'), diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp index 8bb0e00c3b..863e2678a9 100644 --- a/src/smt/smt_solver.cpp +++ b/src/smt/smt_solver.cpp @@ -28,6 +28,8 @@ Notes: #include "params/smt_params_helper.hpp" #include "solver/solver_na2as.h" #include "solver/mus.h" +#include "util/cancel_eh.h" +#include "util/scoped_timer.h" #include @@ -71,12 +73,17 @@ namespace { unsigned m_core_extend_patterns_max_distance; bool m_core_extend_nonlocal_patterns; obj_map m_name2assertion; + // bounds-only linear probe (arith.nl.linear_probe) + expr_ref_vector m_probe_core; + model_ref m_probe_model; + bool m_result_from_probe = false; public: smt_solver(ast_manager & m, params_ref const & p, symbol const & l) : solver_na2as(m), m_smt_params(p), m_context(m, m_smt_params), + m_probe_core(m), m_cuber(nullptr), m_minimizing_core(false), m_core_extend_patterns(false), @@ -163,6 +170,7 @@ namespace { } void assert_expr_core(expr * t) override { + reset_probe(); m_context.assert_expr(t); } void set_phase(expr* e) override { m_context.set_phase(e); } @@ -181,10 +189,12 @@ namespace { } void push_core() override { + reset_probe(); m_context.push(); } void pop_core(unsigned n) override { + reset_probe(); unsigned cur_sz = m_assumptions.size(); if (n > 0 && cur_sz > 0) { unsigned lvl = m_scopes.size(); @@ -202,8 +212,85 @@ namespace { m_context.pop(n); } + void reset_probe() { + m_probe_core.reset(); + m_probe_model = nullptr; + m_result_from_probe = false; + } + + // A short bounds-only probe on a throwaway kernel: solver 6 with the + // nonlinear lemma machinery (Grobner, Horner, nlsat) disabled, so only + // linear reasoning, linearization of fixed-factor monomials and + // row-implied bound tightening act. Effectively-linear queries are + // decided here at a fraction of the cost of the main search and with + // none of its seed variance; anything else fails fast (there is + // nothing expensive left to run) and the main search starts unchanged. + lbool try_nl_linear_probe(unsigned num_assumptions, expr * const * assumptions) { + reset_probe(); + smt_params_helper ph(get_params()); + if (!ph.arith_nl_linear_probe()) + return l_undef; + if (m.proofs_enabled()) + return l_undef; + params_ref pp; + pp.copy(get_params()); + pp.set_bool("arith.nl.linear_probe", false); + pp.set_uint("arith.solver", 6); + pp.set_bool("arith.nl.grobner", false); + pp.set_bool("arith.nl.horner", false); + pp.set_bool("arith.nl.nra", false); + pp.set_bool("arith.nl.nra_check_assignment", false); + pp.set_bool("arith.nl.propagate_row_bounds_improve", true); + + // The probe lives in its own ast_manager: preprocessing inside a + // shared manager would allocate nodes and shift ast identifiers, + // silently changing the tie-breaking of the main search that runs + // after a failed probe. With a separate manager the main search is + // bit-identical to a run without the probe. + // ast_translation's constructor copies the plugin families with + // aligned family ids; the target manager must start bare. + ast_manager pm(PGM_DISABLED); + ast_translation to_probe(m, pm); + scoped_ptr fp = alloc(smt_params, pp); + smt::kernel probe(pm, *fp, pp); + if (m_logic != symbol::null) + probe.set_logic(m_logic); + ptr_vector fmls; + m_context.get_context().get_asserted_formulas(fmls); + for (expr* f : fmls) + probe.assert_expr(to_probe(f)); + expr_ref_vector pas(pm); + for (unsigned i = 0; i < num_assumptions; ++i) + pas.push_back(to_probe(assumptions[i])); + lbool r; + { + cancel_eh eh(pm.limit()); + scoped_timer timer(ph.arith_nl_linear_probe_timeout(), &eh); + r = probe.check(pas.size(), pas.data()); + } + if (r == l_undef) + return l_undef; + ast_translation from_probe(pm, m); + if (r == l_false) { + unsigned sz = probe.get_unsat_core_size(); + for (unsigned i = 0; i < sz; ++i) + m_probe_core.push_back(from_probe(probe.get_unsat_core_expr(i))); + } + else { + model_ref pmdl; + probe.get_model(pmdl); + if (pmdl) + m_probe_model = pmdl->translate(from_probe); + } + m_result_from_probe = true; + return r; + } + lbool check_sat_core2(unsigned num_assumptions, expr * const * assumptions) override { TRACE(solver_na2as, tout << "smt_solver::check_sat_core:\n"; for (unsigned i = 0; i < num_assumptions; ++i) tout << mk_pp(assumptions[i], m) << "\n";); + lbool r = try_nl_linear_probe(num_assumptions, assumptions); + if (r != l_undef) + return r; return m_context.check(num_assumptions, assumptions); } @@ -373,6 +460,10 @@ namespace { }; void get_unsat_core(expr_ref_vector & r) override { + if (m_result_from_probe) { + r.append(m_probe_core); + return; + } unsigned sz = m_context.get_unsat_core_size(); for (unsigned i = 0; i < sz; ++i) { @@ -397,7 +488,10 @@ namespace { } void get_model_core(model_ref & m) override { - m_context.get_model(m); + if (m_result_from_probe) + m = m_probe_model; + else + m_context.get_model(m); } proof * get_proof_core() override { diff --git a/src/smt/tactic/CMakeLists.txt b/src/smt/tactic/CMakeLists.txt index 3b7a719deb..9adfbaa8c6 100644 --- a/src/smt/tactic/CMakeLists.txt +++ b/src/smt/tactic/CMakeLists.txt @@ -1,12 +1,14 @@ z3_add_component(smt_tactic SOURCES ctx_solver_simplify_tactic.cpp + nl_linear_probe_tactic.cpp smt_tactic_core.cpp unit_subsumption_tactic.cpp COMPONENT_DEPENDENCIES smt TACTIC_HEADERS ctx_solver_simplify_tactic.h + nl_linear_probe_tactic.h smt_tactic_core.h unit_subsumption_tactic.h ) diff --git a/src/smt/tactic/nl_linear_probe_tactic.cpp b/src/smt/tactic/nl_linear_probe_tactic.cpp new file mode 100644 index 0000000000..8d72b83773 --- /dev/null +++ b/src/smt/tactic/nl_linear_probe_tactic.cpp @@ -0,0 +1,38 @@ +/*++ +Copyright (c) 2026 Microsoft Corporation + +Module Name: + + nl_linear_probe_tactic.cpp + +Abstract: + + See nl_linear_probe_tactic.h. + +Author: + + Lev Nachmanson (levnach) 2026-08-06 + +--*/ +#include "smt/tactic/nl_linear_probe_tactic.h" +#include "smt/tactic/smt_tactic_core.h" +#include "tactic/tactical.h" + +tactic * mk_nl_linear_probe_tactic(ast_manager & m, params_ref const & p) { + // The probe: solver 6 restricted to its linear machinery. Grobner, + // Horner and nlsat are off; row-implied bound propagation is allowed to + // improve existing bounds, which drives the factor-bounds -> product + // bounds -> farkas cascade to completion on effectively-linear queries. + params_ref probe_p = p; + probe_p.set_uint("arith.solver", 6); + probe_p.set_bool("arith.nl.grobner", false); + probe_p.set_bool("arith.nl.horner", false); + probe_p.set_bool("arith.nl.nra", false); + probe_p.set_bool("arith.nl.nra_check_assignment", false); + probe_p.set_bool("arith.nl.propagate_row_bounds_improve", true); + + unsigned timeout_ms = p.get_uint("probe_timeout", 300); + + return or_else(try_for(using_params(mk_smt_tactic_core(m), probe_p), timeout_ms), + mk_smt_tactic_core(m, p)); +} diff --git a/src/smt/tactic/nl_linear_probe_tactic.h b/src/smt/tactic/nl_linear_probe_tactic.h new file mode 100644 index 0000000000..c1821aca81 --- /dev/null +++ b/src/smt/tactic/nl_linear_probe_tactic.h @@ -0,0 +1,39 @@ +/*++ +Copyright (c) 2026 Microsoft Corporation + +Module Name: + + nl_linear_probe_tactic.h + +Abstract: + + A short bounds-only probe for nonlinear arithmetic followed by the + regular SMT tactic. + + The probe runs the SMT solver with every nonlinear lemma mechanism + disabled (no Grobner, no Horner, no nlsat): only linear reasoning, + linearization of monomials with fixed factors, and row-implied bound + tightening act. On effectively-linear problems - monomials whose + factors are pinned by fixed constants, as in bit-level arithmetic + over power-of-two limbs - this decides the query at a fraction of + the cost and with none of the seed variance of the lemma machinery; + when bound reasoning cannot decide the query the probe fails fast + and the unchanged default SMT tactic runs on a fresh solver. + +Author: + + Lev Nachmanson (levnach) 2026-08-06 + +--*/ +#pragma once + +#include "util/params.h" + +class ast_manager; +class tactic; + +tactic * mk_nl_linear_probe_tactic(ast_manager & m, params_ref const & p = params_ref()); + +/* + ADD_TACTIC("nl-linear-probe", "short bounds-only linear probe for nonlinear arithmetic, falling back to the smt tactic.", "mk_nl_linear_probe_tactic(m, p)") +*/