From 4b8a27090109b51023b29c756b9822f5ee89418a Mon Sep 17 00:00:00 2001 From: Ilana Shapiro Date: Tue, 20 Jan 2026 12:52:00 -0800 Subject: [PATCH] Add SLS tactic as a separate worker thread (#8263) * setting up sls tactic thread * finish the new threading setup, need to add the tactic * add sls thread, it compiles but crashes * it runs but there is some infinite recursion issue with the SLS thread * debug code * fix SLS * update SLS to notify batch manager * clean up imports * add sls param, fix collect sls statistics, clean up other params * clean up code * handle the case when the SLS thread is canceled by another worker but the tactic is still running internally (don't throw an error in this case) * let SLS worker take a stab at all LIA problems, even those with unsupported DISTINCT terms, but don't error on unsupported problems, just return * fix bug when sls is false --------- Co-authored-by: Ilana Shapiro Co-authored-by: Ilana Shapiro --- src/params/smt_parallel_params.pyg | 3 +- src/smt/smt_parallel.cpp | 84 ++++++++++++++++++++++++++---- src/smt/smt_parallel.h | 36 ++++++++++++- 3 files changed, 111 insertions(+), 12 deletions(-) diff --git a/src/params/smt_parallel_params.pyg b/src/params/smt_parallel_params.pyg index b69e6dd32..2dfebd2fc 100644 --- a/src/params/smt_parallel_params.pyg +++ b/src/params/smt_parallel_params.pyg @@ -2,5 +2,6 @@ def_module_params('smt_parallel', export=True, description='Experimental parameters for parallel solving', params=( - ('inprocessing', BOOL, True, 'integrate in-processing as a heuristic simplification'), + ('inprocessing', BOOL, False, 'integrate in-processing as a heuristic simplification'), + ('sls', BOOL, False, 'add sls-tactic as a separate worker thread outside the search tree parallelism'), )) \ No newline at end of file diff --git a/src/smt/smt_parallel.cpp b/src/smt/smt_parallel.cpp index 178bbcf3d..c71c84d12 100644 --- a/src/smt/smt_parallel.cpp +++ b/src/smt/smt_parallel.cpp @@ -64,6 +64,50 @@ namespace smt { namespace smt { + void parallel::sls_worker::run() { + ptr_vector assertions; + p.ctx.get_assertions(assertions); + for (expr* e : assertions) + m_sls->assert_expr(m_g2l(e)); + + lbool res = l_undef; + try { + if (!m.inc()) + return; + res = m_sls->check(); + } catch (z3_exception& ex) { + // Cancellation is normal in portfolio mode + if (m.limit().is_canceled()) { + IF_VERBOSE(1, verbose_stream() << "SLS worker canceled\n"); + return; + } + + if (strstr(ex.what(), "unsupported for sls") != nullptr) { + IF_VERBOSE(1, verbose_stream() << "SLS opted out: " << ex.what() << "\n"); + return; + } + + // Anything else is a real error + IF_VERBOSE(1, verbose_stream() << "SLS threw exception: " << ex.what() << "\n"); + b.set_exception(ex.what()); + return; + } + + if (res == l_true) { + model_ref mdl = m_sls->get_model(); + b.set_sat(m_l2g, *mdl); + } + } + + void parallel::sls_worker::cancel() { + IF_VERBOSE(1, verbose_stream() << " SLS WORKER cancelling\n"); + m.limit().cancel(); + } + + void parallel::sls_worker::collect_statistics(::statistics &st) const { + m_sls->collect_statistics(st); + } + void parallel::worker::run() { search_tree::node *node = nullptr; expr_ref_vector cube(m); @@ -151,6 +195,13 @@ namespace smt { m_config.m_inprocessing = pp.inprocessing(); } + parallel::sls_worker::sls_worker(parallel& p) + : p(p), b(p.m_batch_manager), m(), m_g2l(p.ctx.m, m), m_l2g(m, p.ctx.m) { + IF_VERBOSE(1, verbose_stream() << "Initialized SLS portfolio thread\n"); + m_params.append(p.ctx.m_params); + m_sls = alloc(sls::smt_solver, m, m_params); + } + void parallel::worker::share_units() { // Collect new units learned locally by this worker and send to batch manager @@ -281,7 +332,7 @@ namespace smt { SASSERT(p.ctx.m_unsat_core.empty()); for (auto e : m_search_tree.get_core_from_root()) p.ctx.m_unsat_core.push_back(e); - cancel_workers(); + cancel_background_threads(); } } @@ -389,7 +440,7 @@ namespace smt { return; m_state = state::is_sat; p.ctx.set_model(m.translate(l2g)); - cancel_workers(); + cancel_background_threads(); } void parallel::batch_manager::set_unsat(ast_translation &l2g, expr_ref_vector const &unsat_core) { @@ -403,7 +454,7 @@ namespace smt { SASSERT(p.ctx.m_unsat_core.empty()); for (expr *e : unsat_core) p.ctx.m_unsat_core.push_back(l2g(e)); - cancel_workers(); + cancel_background_threads(); } void parallel::batch_manager::set_exception(unsigned error_code) { @@ -413,7 +464,7 @@ namespace smt { return; m_state = state::is_exception_code; m_exception_code = error_code; - cancel_workers(); + cancel_background_threads(); } void parallel::batch_manager::set_exception(std::string const &msg) { @@ -423,7 +474,7 @@ namespace smt { return; m_state = state::is_exception_msg; m_exception_msg = msg; - cancel_workers(); + cancel_background_threads(); } lbool parallel::batch_manager::get_result() const { @@ -487,6 +538,7 @@ namespace smt { } lbool parallel::operator()(expr_ref_vector const &asms) { + IF_VERBOSE(1, verbose_stream() << "Parallel SMT with " << num_threads << " threads\n";); ast_manager &m = ctx.m; if (m.has_trace_stream()) @@ -497,26 +549,38 @@ namespace smt { scoped_clear(parallel &p) : p(p) {} ~scoped_clear() { p.m_workers.reset(); + p.m_sls_worker = nullptr; } }; scoped_clear clear(*this); m_batch_manager.initialize(); m_workers.reset(); + + smt_parallel_params pp(ctx.m_params); + m_should_run_sls = pp.sls(); + scoped_limits sl(m.limit()); flet _nt(ctx.m_fparams.m_threads, 1); SASSERT(num_threads > 1); for (unsigned i = 0; i < num_threads; ++i) m_workers.push_back(alloc(worker, i, *this, asms)); - for (auto w : m_workers) sl.push_child(&(w->limit())); + if (m_should_run_sls) { + m_sls_worker = alloc(sls_worker, *this); + sl.push_child(&(m_sls_worker->limit())); + } // Launch threads - vector threads(num_threads); - for (unsigned i = 0; i < num_threads; ++i) { + vector threads; + threads.resize(m_should_run_sls ? num_threads + 1 : num_threads); // +1 for sls worker + for (unsigned i = 0; i < num_threads; ++i) threads[i] = std::thread([&, i]() { m_workers[i]->run(); }); - } + + // the final thread runs the sls worker + if (m_should_run_sls) + threads[num_threads] = std::thread([&]() { m_sls_worker->run(); }); // Wait for all threads to finish for (auto &th : threads) @@ -525,6 +589,8 @@ namespace smt { for (auto w : m_workers) w->collect_statistics(ctx.m_aux_stats); m_batch_manager.collect_statistics(ctx.m_aux_stats); + if (m_should_run_sls) + m_sls_worker->collect_statistics(ctx.m_aux_stats); return m_batch_manager.get_result(); } diff --git a/src/smt/smt_parallel.h b/src/smt/smt_parallel.h index 007ab090a..c49b42521 100644 --- a/src/smt/smt_parallel.h +++ b/src/smt/smt_parallel.h @@ -20,6 +20,7 @@ Revision History: #include "smt/smt_context.h" #include "util/search_tree.h" +#include "ast/sls/sls_smt_solver.h" #include #include @@ -35,6 +36,7 @@ namespace smt { class parallel { context& ctx; unsigned num_threads; + bool m_should_run_sls = false; struct shared_clause { unsigned source_worker_id; @@ -77,6 +79,16 @@ namespace smt { w->cancel(); } + void cancel_sls_worker() { + IF_VERBOSE(1, verbose_stream() << "Canceling SLS worker\n"); + p.m_sls_worker->cancel(); + } + + void cancel_background_threads() { + cancel_workers(); + if (p.m_should_run_sls) cancel_sls_worker(); + } + void init_parameters_state(); public: @@ -108,8 +120,8 @@ namespace smt { bool m_share_units_relevant_only = true; bool m_share_units_initial_only = true; double m_max_conflict_mul = 1.5; - bool m_cube_initial_only = true; - bool m_inprocessing = true; + bool m_inprocessing = false; + bool m_sls = false; unsigned m_inprocessing_delay = 1; unsigned m_max_cube_depth = 20; unsigned m_max_conflicts = UINT_MAX; @@ -158,8 +170,28 @@ namespace smt { }; + class sls_worker { + parallel &p; + batch_manager &b; + ast_manager m; + ast_translation m_g2l, m_l2g; + scoped_ptr m_sls; + params_ref m_params; + + public: + sls_worker(parallel &p); + void cancel(); + void run(); + void collect_statistics(::statistics& st) const; + + reslimit &limit() { + return m.limit(); + } + }; + batch_manager m_batch_manager; scoped_ptr_vector m_workers; + scoped_ptr m_sls_worker; public: parallel(context& ctx) :