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

@@ -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 {
     }
 
 }
-

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;

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<bool(lpvar)> m_relevant;
     vector<lemma>            m_lemmas;
     vector<ineq>             m_literals;

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'), 

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) {

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 <atomic>
 #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<solver>          m_solver1;
     ref<solver>          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);
     }

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);
 }

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