From 4ec832c590a807989bc69785a3c1950edc3697c4 Mon Sep 17 00:00:00 2001 From: Ilana Shapiro Date: Thu, 13 Nov 2025 13:14:45 -0800 Subject: [PATCH] fix bug about param protocol iteration only happening once, and add new user param to toggle for only running param tuning thread without parallel solving (just to test if it's finding good settings) --- src/params/smt_parallel_params.pyg | 1 + src/smt/smt_parallel.cpp | 93 +++++++++++++++++------------- src/smt/smt_parallel.h | 16 ++++- 3 files changed, 70 insertions(+), 40 deletions(-) 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);