From 98bb6245ca74b76025d7e2a6300aaec6dfb20f90 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Fri, 7 Aug 2026 06:43:27 -0700 Subject: [PATCH] Add linprobe mode: short monomial linearization probe before SMT Introduce an optional "linprobe" pre-solving phase that runs a short, time-bounded SMT check restricted to linear monomial bound propagation before falling back to the full solver. - nla_core: add m_linprobe flag driven by arith.nl.linprobe_mode; in linprobe mode use monomial_bounds::propagate_linear_bounds instead of propagate_changed_bounds. - monomial_bounds: honor the resource limit inside the linear-bound and LP-row propagation loops so the probe can be interrupted. - theory_lra: return FC_CONTINUE when NLA made progress in linprobe mode, and bail out early when the context became inconsistent. - smt_tactic: wrap the SMT tactic in a new linprobe_tactic that first runs a time-bounded probe with non-linear features disabled and falls back to the regular tactic on failure; user-propagator callbacks disable the probe. - combined_solver: try the same bounded probe on solver1 before the normal path, and track whether user-propagator callbacks are registered. - smt_params_helper: add the arith.nl.linprobe parameter. - test: cover linprobe propagation of newly linear monomials. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> --- src/math/lp/monomial_bounds.cpp | 6 +- src/math/lp/nla_core.cpp | 9 +- src/math/lp/nla_core.h | 1 + src/params/smt_params_helper.pyg | 1 + src/smt/theory_lra.cpp | 6 +- src/solver/combined_solver.cpp | 46 +++++++ src/tactic/smtlogics/smt_tactic.cpp | 203 +++++++++++++++++++++++++++- src/test/monomial_bounds.cpp | 32 +++++ 8 files changed, 297 insertions(+), 7 deletions(-) diff --git a/src/math/lp/monomial_bounds.cpp b/src/math/lp/monomial_bounds.cpp index eab39c9d01..7fe1877fa2 100644 --- a/src/math/lp/monomial_bounds.cpp +++ b/src/math/lp/monomial_bounds.cpp @@ -22,6 +22,7 @@ namespace nla { if (add_lemma()) break; } + } bool monomial_bounds::is_too_big(mpq const &q) const { @@ -218,6 +219,8 @@ namespace nla { bool monomial_bounds::propagate_linear_bounds() { bool propagated = false; for (auto& mm : c().emons()) { + if (!c().reslim().inc()) + break; //if (!c().is_monic_var(v)) // continue; monic &m = c().emon(mm.var()); @@ -727,6 +730,8 @@ namespace nla { bool propagated = false; for (unsigned i = 0; i < lra.row_count(); ++i) { + if (!c().reslim().inc()) + break; if (lra.get_row(i).size() > 32) continue; lpvar free_j; @@ -1126,4 +1131,3 @@ namespace nla { } } - diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp index 66224d24ba..3d495bd519 100644 --- a/src/math/lp/nla_core.cpp +++ b/src/math/lp/nla_core.cpp @@ -27,6 +27,7 @@ core::core(lp::lar_solver& s, params_ref const& p, reslimit & lim) : lra(s), m_reslim(lim), m_params(p), + m_linprobe(p.get_bool("arith.nl.linprobe_mode", false)), m_tangents(this), m_basics(this), m_order(this), @@ -54,6 +55,7 @@ core::core(lp::lar_solver& s, params_ref const& p, reslimit & lim) : } void core::updt_params(params_ref const& p) { + m_linprobe = p.get_bool("arith.nl.linprobe_mode", false); m_grobner.updt_params(p); } @@ -1545,8 +1547,13 @@ bool core::propagate() { propagated = true; if (m_monomial_bounds.tighten_lp_bounds()) propagated = true; - if (m_monomial_bounds.propagate_changed_bounds()) + if (m_linprobe) { + if (m_monomial_bounds.propagate_linear_bounds()) + propagated = true; + } + else if (m_monomial_bounds.propagate_changed_bounds()) { propagated = true; + } m_monics_with_changed_bounds.reset(); if (propagated) m_check_feasible = true; diff --git a/src/math/lp/nla_core.h b/src/math/lp/nla_core.h index 81976f07a5..27d6152e40 100644 --- a/src/math/lp/nla_core.h +++ b/src/math/lp/nla_core.h @@ -73,6 +73,7 @@ class core { lp::lar_solver& lra; reslimit& m_reslim; smt_params_helper m_params; + bool m_linprobe; std::function m_relevant; vector m_lemmas; vector m_literals; diff --git a/src/params/smt_params_helper.pyg b/src/params/smt_params_helper.pyg index 5f65fa6ce2..6c27870e18 100644 --- a/src/params/smt_params_helper.pyg +++ b/src/params/smt_params_helper.pyg @@ -99,6 +99,7 @@ def_module_params(module_name='smt', ('arith.nl.monomial_binomial_sign', BOOL, False, 'derive bound on a binomial-monomial factor anchored on the current LP value of the monomial; replaces order_lemma_on_binomial_sign with a deterministic factor bound conditioned on a one-sided snapshot of the monomial value'), ('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.linprobe', BOOL, True, 'run a short monomial linearization probe before the SMT tactic'), ('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'), diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index 4b9a9646fb..9f2de32739 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -1745,9 +1745,13 @@ public: IF_VERBOSE(12, verbose_stream() << "final-check " << lp().get_status() << "\n"); lbool is_sat = l_true; SASSERT(lp().ax_is_correct()); - propagate_nla(); + bool const nla_progress = propagate_nla(); if (!lp().is_feasible() || lp().has_changed_columns()) is_sat = make_feasible(); + if (ctx().inconsistent()) + return FC_CONTINUE; + if (nla_progress && is_sat == l_true && ctx().get_params().get_bool("arith.nl.linprobe_mode", false)) + return FC_CONTINUE; final_check_status st = FC_DONE; bool int_undef = false; switch (is_sat) { diff --git a/src/solver/combined_solver.cpp b/src/solver/combined_solver.cpp index f324b64b29..e37268ea67 100644 --- a/src/solver/combined_solver.cpp +++ b/src/solver/combined_solver.cpp @@ -21,11 +21,14 @@ Notes: #include "util/scoped_timer.h" #include "util/common_msgs.h" #include "ast/ast_pp.h" +#include "params/smt_params_helper.hpp" #include "solver/solver.h" #include "solver/combined_solver_params.hpp" #include #define PS_VB_LVL 15 +static constexpr unsigned linprobe_timeout_ms = 100; + /** \brief Implementation of the solver API that combines two given solvers. @@ -56,6 +59,7 @@ private: bool m_inc_mode; bool m_check_sat_executed; bool m_use_solver1_results; + bool m_has_callbacks; ref m_solver1; ref m_solver2; // We delay sending assertions to solver 2 @@ -114,6 +118,28 @@ private: } } + lbool try_linprobe(unsigned num_assumptions, expr* const* assumptions) { + if (m_has_callbacks || !smt_params_helper(get_params()).arith_nl_linprobe()) + return l_undef; + + IF_VERBOSE(PS_VB_LVL, verbose_stream() << "(combined-solver \"using linprobe\")\n";); + m_use_solver1_results = true; + aux_timeout_eh eh(m_solver1.get()); + lbool r = l_undef; + try { + scoped_timer timer(linprobe_timeout_ms, &eh); + r = m_solver1->check_sat_core(num_assumptions, assumptions); + } + catch (z3_exception&) { + if (!eh.m_canceled) + throw; + } + if (r != l_undef && !eh.m_canceled) + return r; + m_use_solver1_results = false; + return l_undef; + } + public: combined_solver(solver * s1, solver * s2, params_ref const & p): solver(s1->get_manager()) { @@ -123,6 +149,7 @@ public: m_inc_mode = false; m_check_sat_executed = false; m_use_solver1_results = true; + m_has_callbacks = false; } solver* translate(ast_manager& m, params_ref const& p) override { @@ -133,6 +160,7 @@ public: r->m_inc_mode = m_inc_mode; r->m_check_sat_executed = m_check_sat_executed; r->m_use_solver1_results = m_use_solver1_results; + r->m_has_callbacks = m_has_callbacks; return r; } @@ -212,6 +240,12 @@ public: m_check_sat_executed = true; m_use_solver1_results = false; + if (m_inc_mode || get_num_assumptions() != 0 || num_assumptions > 0 || m_ignore_solver1) { + lbool const r = try_linprobe(num_assumptions, assumptions); + if (r != l_undef) + return r; + } + if (get_num_assumptions() != 0 || num_assumptions > 0 || // assumptions were provided m_ignore_solver1) { @@ -352,6 +386,7 @@ public: void register_on_clause(void* ctx, user_propagator::on_clause_eh_t& on_clause) override { switch_inc_mode(); + m_has_callbacks = true; m_solver2->register_on_clause(ctx, on_clause); } @@ -361,46 +396,57 @@ public: user_propagator::pop_eh_t& pop_eh, user_propagator::fresh_eh_t& fresh_eh) override { switch_inc_mode(); + m_has_callbacks = true; m_solver2->user_propagate_init(ctx, push_eh, pop_eh, fresh_eh); } void user_propagate_register_fixed(user_propagator::fixed_eh_t& fixed_eh) override { + m_has_callbacks = true; m_solver2->user_propagate_register_fixed(fixed_eh); } void user_propagate_register_final(user_propagator::final_eh_t& final_eh) override { + m_has_callbacks = true; m_solver2->user_propagate_register_final(final_eh); } void user_propagate_register_eq(user_propagator::eq_eh_t& eq_eh) override { + m_has_callbacks = true; m_solver2->user_propagate_register_eq(eq_eh); } void user_propagate_register_diseq(user_propagator::eq_eh_t& diseq_eh) override { + m_has_callbacks = true; m_solver2->user_propagate_register_diseq(diseq_eh); } void user_propagate_register_on_binding(user_propagator::binding_eh_t& binding_eh) override { + m_has_callbacks = true; m_solver2->user_propagate_register_on_binding(binding_eh); } void user_propagate_register_expr(expr* e) override { + m_has_callbacks = true; m_solver2->user_propagate_register_expr(e); } void user_propagate_register_created(user_propagator::created_eh_t& r) override { + m_has_callbacks = true; m_solver2->user_propagate_register_created(r); } void user_propagate_register_decide(user_propagator::decide_eh_t& r) override { + m_has_callbacks = true; m_solver2->user_propagate_register_decide(r); } void user_propagate_clear() override { + m_has_callbacks = false; m_solver2->user_propagate_clear(); } void user_propagate_initialize_value(expr* var, expr* value) override { + m_has_callbacks = true; m_solver1->user_propagate_initialize_value(var, value); m_solver2->user_propagate_initialize_value(var, value); } diff --git a/src/tactic/smtlogics/smt_tactic.cpp b/src/tactic/smtlogics/smt_tactic.cpp index 7bae01a810..3f61985a1a 100644 --- a/src/tactic/smtlogics/smt_tactic.cpp +++ b/src/tactic/smtlogics/smt_tactic.cpp @@ -16,12 +16,194 @@ Author: --*/ #include "params/sat_params.hpp" +#include "params/smt_params_helper.hpp" #include "solver/solver2tactic.h" #include "solver/solver.h" #include "smt/tactic/smt_tactic_core.h" #include "sat/tactic/sat_tactic.h" +#include "tactic/tactical.h" -tactic * mk_smt_tactic(ast_manager & m, params_ref const & p) { +namespace { + +constexpr unsigned linprobe_timeout_ms = 100; + +params_ref probe_params(params_ref const& p) { + params_ref r = p; + r.set_bool("auto_config", false); + r.set_bool("parallel.enable", false); + r.set_uint("arith.solver", 6); + r.set_bool("arith.nl.linprobe", true); + r.set_bool("arith.nl.linprobe_mode", true); + r.set_bool("arith.nl.propagate_fixed_rows", true); + r.set_bool("arith.nl.propagate_linear_monomials", true); + r.set_bool("arith.nl.optimize_bounds", false); + r.set_bool("arith.nl.grobner", false); + r.set_bool("arith.nl.horner", false); + r.set_bool("arith.nl.cross_nested", false); + r.set_bool("arith.nl.nra", false); + r.set_bool("arith.nl.nra_check_assignment", false); + r.set_bool("arith.nl.branching", false); + r.set_bool("arith.nl.order", false); + r.set_bool("arith.nl.tangents", false); + r.set_bool("arith.nl.monomial_sandwich", false); + r.set_bool("arith.nl.monomial_binomial_sign", false); + r.set_bool("candidate_models", false); + r.set_bool("fail_if_inconclusive", true); + return r; +} + +params_ref fallback_params(params_ref const& p) { + params_ref r = p; + r.set_bool("arith.nl.linprobe", false); + r.set_bool("arith.nl.linprobe_mode", false); + return r; +} + +class linprobe_tactic : public tactic { + tactic_ref m_probe; + tactic_ref m_fallback; + params_ref m_params; + bool m_has_callbacks = false; + +public: + linprobe_tactic(tactic* probe, tactic* fallback, params_ref const& p): + m_probe(probe), + m_fallback(fallback), + m_params(p) { + updt_params(p); + } + + char const* name() const override { return "linprobe"; } + + void operator()(goal_ref const& in, goal_ref_buffer& result) override { + if (!smt_params_helper(m_params).arith_nl_linprobe() || m_has_callbacks) { + (*m_fallback)(in, result); + return; + } + + goal orig(*in); + try { + (*m_probe)(in, result); + return; + } + catch (tactic_exception&) { + result.reset(); + in->reset_all(); + in->copy_from(orig); + } + (*m_fallback)(in, result); + } + + void updt_params(params_ref const& p) override { + m_params.copy(p); + m_probe->updt_params(probe_params(p)); + m_fallback->updt_params(fallback_params(p)); + } + + void collect_param_descrs(param_descrs& r) override { + m_fallback->collect_param_descrs(r); + } + + void collect_statistics(statistics& st) const override { + m_probe->collect_statistics(st); + m_fallback->collect_statistics(st); + } + + void reset_statistics() override { + m_probe->reset_statistics(); + m_fallback->reset_statistics(); + } + + void cleanup() override { + m_probe->cleanup(); + m_fallback->cleanup(); + } + + void reset() override { + m_probe->reset(); + m_fallback->reset(); + } + + void set_logic(symbol const& l) override { + m_probe->set_logic(l); + m_fallback->set_logic(l); + } + + void set_progress_callback(progress_callback* callback) override { + m_probe->set_progress_callback(callback); + m_fallback->set_progress_callback(callback); + } + + tactic* translate(ast_manager& m) override { + return alloc(linprobe_tactic, m_probe->translate(m), m_fallback->translate(m), m_params); + } + + void register_on_clause(void* ctx, user_propagator::on_clause_eh_t& on_clause) override { + m_has_callbacks = true; + m_fallback->register_on_clause(ctx, on_clause); + } + + void user_propagate_init( + void* ctx, + user_propagator::push_eh_t& push_eh, + user_propagator::pop_eh_t& pop_eh, + user_propagator::fresh_eh_t& fresh_eh) override { + m_has_callbacks = true; + m_fallback->user_propagate_init(ctx, push_eh, pop_eh, fresh_eh); + } + + void user_propagate_register_fixed(user_propagator::fixed_eh_t& fixed_eh) override { + m_has_callbacks = true; + m_fallback->user_propagate_register_fixed(fixed_eh); + } + + void user_propagate_register_final(user_propagator::final_eh_t& final_eh) override { + m_has_callbacks = true; + m_fallback->user_propagate_register_final(final_eh); + } + + void user_propagate_register_eq(user_propagator::eq_eh_t& eq_eh) override { + m_has_callbacks = true; + m_fallback->user_propagate_register_eq(eq_eh); + } + + void user_propagate_register_diseq(user_propagator::eq_eh_t& diseq_eh) override { + m_has_callbacks = true; + m_fallback->user_propagate_register_diseq(diseq_eh); + } + + void user_propagate_register_on_binding(user_propagator::binding_eh_t& binding_eh) override { + m_has_callbacks = true; + m_fallback->user_propagate_register_on_binding(binding_eh); + } + + void user_propagate_register_expr(expr* e) override { + m_has_callbacks = true; + m_fallback->user_propagate_register_expr(e); + } + + void user_propagate_register_created(user_propagator::created_eh_t& created_eh) override { + m_has_callbacks = true; + m_fallback->user_propagate_register_created(created_eh); + } + + void user_propagate_register_decide(user_propagator::decide_eh_t& decide_eh) override { + m_has_callbacks = true; + m_fallback->user_propagate_register_decide(decide_eh); + } + + void user_propagate_clear() override { + m_has_callbacks = false; + m_fallback->user_propagate_clear(); + } + + void user_propagate_initialize_value(expr* var, expr* value) override { + m_has_callbacks = true; + m_fallback->user_propagate_initialize_value(var, value); + } +}; + +tactic* mk_raw_smt_tactic(ast_manager& m, params_ref const& p) { sat_params sp(p); if (sp.smt()) return mk_solver2tactic(mk_smt2_solver(m, p)); @@ -30,7 +212,20 @@ tactic * mk_smt_tactic(ast_manager & m, params_ref const & p) { return mk_smt_tactic_core(m, p); } -tactic * mk_smt_tactic_using(ast_manager& m, bool auto_config, params_ref const& p) { - sat_params sp(p); - return sp.euf() ? mk_sat_tactic(m, p) : mk_smt_tactic_core_using(m, auto_config, p); +tactic* mk_linprobe_tactic(ast_manager& m, params_ref const& p) { + params_ref pp = probe_params(p); + tactic* probe = try_for(mk_smt_tactic_core(m, pp), linprobe_timeout_ms); + return alloc(linprobe_tactic, probe, mk_raw_smt_tactic(m, p), p); +} + +} + +tactic * mk_smt_tactic(ast_manager & m, params_ref const & p) { + return mk_linprobe_tactic(m, p); +} + +tactic * mk_smt_tactic_using(ast_manager& m, bool auto_config, params_ref const& p) { + params_ref q = p; + q.set_bool("auto_config", auto_config); + return using_params(mk_linprobe_tactic(m, q), q); } diff --git a/src/test/monomial_bounds.cpp b/src/test/monomial_bounds.cpp index 0583ab5230..6c35edeb96 100644 --- a/src/test/monomial_bounds.cpp +++ b/src/test/monomial_bounds.cpp @@ -167,12 +167,44 @@ void test_monomial_bounds_linear_case() { VERIFY(result != l_false); // Should be consistent } +bool propagate_new_linear_monomial(bool linprobe) { + lp::lar_solver s; + reslimit rl; + params_ref p; + p.set_bool("arith.nl.linprobe_mode", linprobe); + + lpvar x = s.add_var(0, true); + lpvar y = s.add_var(1, true); + lpvar xy = s.add_var(2, true); + + nla::core nla_solver(s, p, rl); + lpvar vars[] = { x, y }; + nla_solver.add_monic(xy, 2, vars); + + VERIFY(!nla_solver.propagate()); + + s.add_var_bound(x, lp::lconstraint_kind::GE, rational(2)); + s.add_var_bound(x, lp::lconstraint_kind::LE, rational(2)); + s.set_column_value_test(x, lp::impq(rational(2))); + s.set_column_value_test(y, lp::impq(rational(3))); + s.set_column_value_test(xy, lp::impq(rational(0))); + + return nla_solver.propagate(); +} + +void test_monomial_bounds_linprobe() { + std::cout << "test_monomial_bounds_linprobe\n"; + VERIFY(!propagate_new_linear_monomial(false)); + VERIFY(propagate_new_linear_monomial(true)); +} + void test_monomial_bounds() { test_monomial_bounds_basic(); test_monomial_bounds_propagation(); test_monomial_bounds_intervals(); test_monomial_bounds_power(); test_monomial_bounds_linear_case(); + test_monomial_bounds_linprobe(); } } // namespace nla