mirror of
https://github.com/Z3Prover/z3
synced 2026-01-21 17:44:43 +00:00
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 <ilanashapiro@Ilanas-MBP.lan1> Co-authored-by: Ilana Shapiro <ilanashapiro@Ilanas-MacBook-Pro.local>
This commit is contained in:
Ilana Shapiro
GitHub
parent
7c4a22d865
commit
4b8a270901
3 changed files with 111 additions and 12 deletions
|
|
@ -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'),
|
||||
))
|
||||
|
|
@ -64,6 +64,50 @@ namespace smt {
|
|||
|
||||
namespace smt {
|
||||
|
||||
void parallel::sls_worker::run() {
|
||||
ptr_vector<expr> 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<cube_config> *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<unsigned> _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<std::thread> threads(num_threads);
|
||||
for (unsigned i = 0; i < num_threads; ++i) {
|
||||
vector<std::thread> 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();
|
||||
}
|
||||
|
|
|
|||
|
|
@ -20,6 +20,7 @@ Revision History:
|
|||
|
||||
#include "smt/smt_context.h"
|
||||
#include "util/search_tree.h"
|
||||
#include "ast/sls/sls_smt_solver.h"
|
||||
#include <thread>
|
||||
#include <mutex>
|
||||
|
||||
|
|
@ -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<sls::smt_solver> 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<worker> m_workers;
|
||||
scoped_ptr<sls_worker> m_sls_worker;
|
||||
|
||||
public:
|
||||
parallel(context& ctx) :
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue