diff --git a/src/smt/smt_parallel.cpp b/src/smt/smt_parallel.cpp index 59c01a30d..c0c1f067f 100644 --- a/src/smt/smt_parallel.cpp +++ b/src/smt/smt_parallel.cpp @@ -83,17 +83,18 @@ namespace smt { return r; } - std::pair parallel::param_generator::replay_proof_prefixes(unsigned max_conflicts_epsilon=200) { + void parallel::param_generator::replay_proof_prefixes(unsigned max_conflicts_epsilon=200) { unsigned conflict_budget = m_max_prefix_conflicts + max_conflicts_epsilon; param_values best_param_state; - double best_score; + double best_score = 0; bool found_better_params = false; - for (unsigned i = 0; i < N; ++i) { + for (unsigned i = 0; i <= N; ++i) { IF_VERBOSE(1, verbose_stream() << " PARAM TUNER: replaying proof prefix in param probe context " << i << "\n"); // copy prefix solver context to a new probe_ctx for next replay with candidate mutation - scoped_ptr probe_ctx = alloc(context, m, ctx->get_fparams(), m_p); + smt_params smtp(m_p); + scoped_ptr probe_ctx = alloc(context, m, smtp, m_p); context::copy(*ctx, *probe_ctx, true); // apply a candidate (mutated) param state to probe_ctx @@ -110,24 +111,37 @@ namespace smt { // replay the cube (negation of the clause) for (expr_ref_vector const& cube : probe_ctx->m_recorded_cubes) { - lbool r = probe_ctx->check(cube.size(), cube.data()); - + lbool r = probe_ctx->check(cube.size(), cube.data()); unsigned conflicts = probe_ctx->m_stats.m_num_conflicts; unsigned decisions = probe_ctx->m_stats.m_num_decisions; - + IF_VERBOSE(1, verbose_stream() << " PARAM TUNER " << i << ": cube replay result " << r << + ", conflicts = " << conflicts << ", decisions = " << decisions << "\n"); score += conflicts + decisions; } - if (i > 0 && score < best_score) { - found_better_params = true; - best_param_state = mutated_param_state; + if (i == 0) { best_score = score; - } else { + IF_VERBOSE(1, verbose_stream() << " PARAM TUNER: baseline score = " << best_score << "\n"); + } + else if (score < best_score) { + found_better_params = true; + best_param_state = mutated_param_state; best_score = score; } } - - return {best_param_state, found_better_params}; + // NOTE: we either need to apply the best params found that are better than base line + // or, we have to implement a comparison operator for param_values (what would this do?) + // or, we update the param state every single time even if it hasn't changed (what would this do?) + // for now, I went with option 1 + if (found_better_params) { + 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"); + } + else { + IF_VERBOSE(1, verbose_stream() << " PARAM TUNER retained current param state\n"); + } } void parallel::param_generator::init_param_state() { @@ -144,9 +158,23 @@ namespace smt { m_param_state.push_back( {symbol("smt.arith.nl.propagate_linear_monomials"), smtp.arith_nl_propagate_linear_monomials()}); m_param_state.push_back({symbol("smt.arith.nl.tangents"), smtp.arith_nl_tangents()}); - }; + params_ref parallel::param_generator::apply_param_values(param_values const &pv) { + params_ref p = m_p; + for (auto const &[k, v] : pv) { + if (std::holds_alternative(v)) { + unsigned_value uv = std::get(v); + p.set_uint(k, uv.value); + } + else if (std::holds_alternative(v)) { + bool bv = std::get(v); + p.set_bool(k, bv); + } + } + return p; + } + parallel::param_generator::param_values parallel::param_generator::mutate_param_state() { param_values new_param_values(m_param_state); unsigned index = ctx->get_random_value() % new_param_values.size(); @@ -161,7 +189,7 @@ namespace smt { while (new_value == value) { new_value = lo + ctx->get_random_value() % (hi - lo + 1); } - std::get(param.second).value = new_value; + std::get_if(¶m.second)->value = new_value; } return new_param_values; } @@ -174,20 +202,7 @@ namespace smt { switch (r) { case l_undef: { - auto [best_param_state, found_better_params] = replay_proof_prefixes(); - - // NOTE: we either need to return a pair from replay_proof_prefixes so we can return a boolean flag indicating whether better params were found. - // or, we have to implement a comparison operator for param_values - // or, we update the param state every single time even if it hasn't changed - // for now, I went with option 1 - if (found_better_params) { - 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"); - } else { - IF_VERBOSE(1, verbose_stream() << " PARAM TUNER retained current param state\n"); - } + replay_proof_prefixes(); } case l_true: { IF_VERBOSE(1, verbose_stream() << " PARAM TUNER found formula sat\n"); @@ -222,9 +237,8 @@ namespace smt { LOG_WORKER(1, " CUBE SIZE IN MAIN LOOP: " << cube.size() << "\n"); // apply current best param state from batch manager - smt_params params = b.get_best_param_state(); params_ref p; - params.updt_params(p); + b.get_param_state(p); ctx->updt_params(p); lbool r = check_cube(cube); @@ -454,10 +468,9 @@ namespace smt { } } - // todo make this thread safe by not using reference counts implicit in params ref but instead copying the entire structure. - params_ref parallel::batch_manager::get_best_param_state() { + void parallel::batch_manager::get_param_state(params_ref& p) { std::scoped_lock lock(mux); - return m_param_state; + p.copy(m_param_state); } void parallel::worker::collect_shared_clauses() { diff --git a/src/smt/smt_parallel.h b/src/smt/smt_parallel.h index fab6029ab..e0ecb874a 100644 --- a/src/smt/smt_parallel.h +++ b/src/smt/smt_parallel.h @@ -89,9 +89,9 @@ namespace smt { void set_exception(std::string const& msg); void set_exception(unsigned error_code); void set_param_state(params_ref const& p) { m_param_state.copy(p); } - void collect_statistics(::statistics& st) const; - - params_ref get_best_param_state(); + void get_param_state(params_ref &p); + void collect_statistics(::statistics& st) const; + bool get_cube(ast_translation& g2l, unsigned id, expr_ref_vector& cube, node*& n); void backtrack(ast_translation& l2g, expr_ref_vector const& core, node* n); void split(ast_translation& l2g, unsigned id, node* n, expr* atom); @@ -110,6 +110,14 @@ namespace smt { // 4. update current configuration with the winner class param_generator { + struct unsigned_value { + unsigned value; + unsigned min_value; + unsigned max_value; + }; + using param_value = std::variant; + using param_values = vector>; + parallel &p; batch_manager &b; ast_manager m; @@ -120,42 +128,18 @@ namespace smt { unsigned m_max_prefix_conflicts = 1000; scoped_ptr m_prefix_solver; - scoped_ptr_vector m_param_probe_contexts; params_ref m_p; - - struct unsigned_value { - unsigned value; - unsigned min_value; - unsigned max_value; - }; - using param_value = std::variant; - using param_values = vector>; param_values m_param_state; - params_ref apply_param_values(param_values const &pv) { - params_ref p = m_p; - for (auto const& [k, v] : pv) { - if (std::holds_alternative(v)) { - unsigned_value uv = std::get(v); - p.set_uint(k, uv.value); - } else if (std::holds_alternative(v)) { - bool bv = std::get(v); - p.set_bool(k, bv); - } - } - return p; - } - - private: + params_ref apply_param_values(param_values const &pv); void init_param_state(); - param_values mutate_param_state(); public: param_generator(parallel &p); lbool run_prefix_step(); void protocol_iteration(); - std::pair replay_proof_prefixes(unsigned max_conflicts_epsilon); + void replay_proof_prefixes(unsigned max_conflicts_epsilon); reslimit &limit() { return m.limit();