diff --git a/src/params/smt_parallel_params.pyg b/src/params/smt_parallel_params.pyg index fc6cd8063..d1e2e567d 100644 --- a/src/params/smt_parallel_params.pyg +++ b/src/params/smt_parallel_params.pyg @@ -23,5 +23,6 @@ def_module_params('smt_parallel', ('inprocessing', BOOL, False, 'integrate in-processing as a heuristic simplification'), ('inprocessing_delay', UINT, 0, 'number of undef before invoking simplification'), ('param_tuning', BOOL, False, 'whether to tune params online during solving'), + ('enable_parallel_smt', BOOL, True, 'whether to run the parallel solver (set to FALSE to test param tuning only)'), ('tunable_params', STRING, '', 'comma-separated key=value list for online param tuning, e.g. \"smt.arith.nl.horner=false,smt.arith.nl.delay=8\"') )) \ No newline at end of file diff --git a/src/smt/smt_parallel.cpp b/src/smt/smt_parallel.cpp index 389a3b8b1..12bd54786 100644 --- a/src/smt/smt_parallel.cpp +++ b/src/smt/smt_parallel.cpp @@ -148,7 +148,8 @@ namespace smt { m_param_state = best_param_state; auto p = apply_param_values(m_param_state); b.set_param_state(p); - IF_VERBOSE(1, verbose_stream() << " PARAM TUNER found better param state\n"); + IF_VERBOSE(1, verbose_stream() << " PARAM TUNER found better param state:\n"); + print_param_values(m_param_state); } else { IF_VERBOSE(1, verbose_stream() << " PARAM TUNER retained current param state\n"); @@ -215,33 +216,35 @@ namespace smt { } void parallel::param_generator::protocol_iteration() { - IF_VERBOSE(1, verbose_stream() << " PARAM TUNER running protocol iteration\n"); - - ctx->get_fparams().m_max_conflicts = m_max_prefix_conflicts; - lbool r = run_prefix_step(); + while (!m.limit().is_canceled()) { + IF_VERBOSE(1, verbose_stream() << " PARAM TUNER running protocol iteration\n"); + + ctx->get_fparams().m_max_conflicts = m_max_prefix_conflicts; + lbool r = run_prefix_step(); - if (m.limit().is_canceled()) - return; + if (m.limit().is_canceled()) + return; - switch (r) { - case l_undef: { - replay_proof_prefixes(); - break; - } - case l_true: { - IF_VERBOSE(1, verbose_stream() << " PARAM TUNER found formula sat\n"); - model_ref mdl; - ctx->get_model(mdl); - b.set_sat(m_l2g, *mdl); - break; - } - case l_false: { - expr_ref_vector const &unsat_core = ctx->unsat_core(); - IF_VERBOSE(2, verbose_stream() << " unsat core:\n"; - for (auto c : unsat_core) verbose_stream() << mk_bounded_pp(c, m, 3) << "\n"); - IF_VERBOSE(1, verbose_stream() << " PARAM TUNER determined formula unsat\n"); - b.set_unsat(m_l2g, unsat_core); - break; + switch (r) { + case l_undef: { + replay_proof_prefixes(); + break; + } + case l_true: { + IF_VERBOSE(1, verbose_stream() << " PARAM TUNER found formula sat\n"); + model_ref mdl; + ctx->get_model(mdl); + b.set_sat(m_l2g, *mdl); + break; + } + case l_false: { + expr_ref_vector const &unsat_core = ctx->unsat_core(); + IF_VERBOSE(2, verbose_stream() << " unsat core:\n"; + for (auto c : unsat_core) verbose_stream() << mk_bounded_pp(c, m, 3) << "\n"); + IF_VERBOSE(1, verbose_stream() << " PARAM TUNER determined formula unsat\n"); + b.set_unsat(m_l2g, unsat_core); + break; + } } } } @@ -699,16 +702,19 @@ namespace smt { smt_parallel_params pp(ctx.m_params); m_should_tune_params = pp.param_tuning(); + m_should_run_parallel = pp.enable_parallel_smt(); 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_parallel) { + 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_tune_params) { m_param_generator = alloc(param_generator, *this); @@ -757,13 +763,22 @@ namespace smt { } // Launch threads - vector threads(m_should_tune_params ? num_threads + 1 : num_threads); // +1 for param generator - for (unsigned i = 0; i < num_threads; ++i) { - threads[i] = std::thread([&, i]() { m_workers[i]->run(); }); - } - // the final thread runs the parameter generator - if (m_should_tune_params) { - threads[num_threads] = std::thread([&]() { m_param_generator->protocol_iteration(); }); + // threads must live beyond the branch scope so we declare them here. + vector threads; + if (m_should_run_parallel) { + threads.resize(m_should_tune_params ? num_threads + 1 : num_threads); // +1 for param generator + for (unsigned i = 0; i < num_threads; ++i) { + threads[i] = std::thread([&, i]() { m_workers[i]->run(); }); + } + // the final thread runs the parameter generator + if (m_should_tune_params) { + threads[num_threads] = std::thread([&]() { m_param_generator->protocol_iteration(); }); + } + } else { // just do param tuning (if requested) + if (m_should_tune_params) { + threads.resize(1); + threads[0] = std::thread([&]() { m_param_generator->protocol_iteration(); }); + } } // Wait for all threads to finish diff --git a/src/smt/smt_parallel.h b/src/smt/smt_parallel.h index f0fc43844..9d3c92195 100644 --- a/src/smt/smt_parallel.h +++ b/src/smt/smt_parallel.h @@ -37,6 +37,7 @@ namespace smt { context& ctx; unsigned num_threads; bool m_should_tune_params; + bool m_should_run_parallel; struct shared_clause { unsigned source_worker_id; @@ -73,7 +74,7 @@ namespace smt { obj_hashtable shared_clause_set; // for duplicate filtering on per-thread clause expressions void cancel_background_threads() { - cancel_workers(); + if (p.m_should_run_parallel) cancel_workers(); if (p.m_should_tune_params) cancel_param_generator(); } @@ -147,6 +148,19 @@ namespace smt { params_ref apply_param_values(param_values const &pv); void init_param_state(); param_values mutate_param_state(); + void print_param_values(param_values const &pv) { + for (auto const &kv : pv) { + std::visit([&](auto&& arg) { + using T = std::decay_t; + if constexpr (std::is_same_v) { + IF_VERBOSE(1, verbose_stream() << kv.first << "=" << arg.value << " "); + } else if constexpr (std::is_same_v) { + IF_VERBOSE(1, verbose_stream() << kv.first << "=" << (arg ? "true" : "false") << " "); + } + }, kv.second); + } + IF_VERBOSE(1, verbose_stream() << "\n"); + } public: param_generator(parallel &p);