diff --git a/src/smt/smt_parallel.cpp b/src/smt/smt_parallel.cpp index 0e1c10744..4d4bfe4f1 100644 --- a/src/smt/smt_parallel.cpp +++ b/src/smt/smt_parallel.cpp @@ -70,11 +70,14 @@ namespace smt { lbool r = l_undef; try { r = ctx->check(); - } catch (z3_error &err) { + } + catch (z3_error &err) { b.set_exception(err.error_code()); - } catch (z3_exception &ex) { + } + catch (z3_exception &ex) { b.set_exception(ex.what()); - } catch (...) { + } + catch (...) { b.set_exception("unknown exception"); } return r; @@ -128,6 +131,52 @@ namespace smt { return best_param_state_idx; } + void parallel::param_generator::init_param_state() { + // param_descrs smt_desc; + // smt_params_helper::collect_param_descrs(smt_desc); + smt_params_helper smtp(m_p); + m_my_param_state.insert(symbol("smt.arith.nl.branching"), smtp.arith_nl_branching()); + m_my_param_state.insert(symbol("smt.arith.nl.cross_nested"), smtp.arith_nl_cross_nested()); + m_my_param_state.insert(symbol("smt.arith.nl.delay"), smtp.arith_nl_delay()); + m_my_param_state.insert(symbol("smt.arith.nl.expensive_patching"), smtp.arith_nl_expensive_patching()); + m_my_param_state.insert(symbol("smt.arith.nl.gb"), smtp.arith_nl_gb()); + m_my_param_state.insert(symbol("smt.arith.nl.horner"), smtp.arith_nl_horner()); + m_my_param_state.insert(symbol("smt.arith.nl.horner_frequency"), smtp.arith_nl_horner_frequency()); + m_my_param_state.insert(symbol("smt.arith.nl.optimize_bounds"), smtp.arith_nl_optimize_bounds()); + m_my_param_state.insert(symbol("smt.arith.nl.propagate_linear_monomials"), smtp.arith_nl_propagate_linear_monomials()); + m_my_param_state.insert(symbol("smt.arith.nl.tangents"), smtp.arith_nl_tangents()); + }; + + // TODO: this should mutate only one field at a time an mutate it based on m_my_param_state to keep it generic. + + smt_params parallel::param_generator::mutate_param_state() { + smt_params p = m_param_state; + random_gen m_rand; + + auto flip_bool = [&](bool &x) { + if (m_rand(2) == 0) + x = !x; + }; + + auto mutate_uint = [&](unsigned &x, unsigned lo, unsigned hi) { + if ((m_rand() % 2) == 0) + x = lo + (m_rand((hi - lo + 1))); + }; + + flip_bool(p.m_nl_arith_branching); + flip_bool(p.m_nl_arith_cross_nested); + mutate_uint(p.m_nl_arith_delay, 5, 20); + flip_bool(p.m_nl_arith_expensive_patching); + flip_bool(p.m_nl_arith_gb); + flip_bool(p.m_nl_arith_horner); + mutate_uint(p.m_nl_arith_horner_frequency, 2, 6); + flip_bool(p.m_nl_arith_optimize_bounds); + flip_bool(p.m_nl_arith_propagate_linear_monomials); + flip_bool(p.m_nl_arith_tangents); + + return p; + } + 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; @@ -142,6 +191,8 @@ namespace smt { switch (r) { case l_undef: { + // TODO, change from smt_params to a generic param state representation based on params_ref + // only params_ref have effect on updates. smt_params best_param_state = m_param_state; vector candidate_param_states; diff --git a/src/smt/smt_parallel.h b/src/smt/smt_parallel.h index f0a438a47..311589f9b 100644 --- a/src/smt/smt_parallel.h +++ b/src/smt/smt_parallel.h @@ -20,7 +20,7 @@ Revision History: #include "smt/smt_context.h" #include "util/search_tree.h" -// #include "util/util.h" +#include #include #include @@ -127,74 +127,37 @@ namespace smt { // 4. update current configuration with the winner class param_generator { - parallel& p; - batch_manager& b; + parallel &p; + batch_manager &b; ast_manager m; scoped_ptr ctx; ast_translation m_l2g; - - unsigned N = 4; // number of prefix permutations to test (including current) + + unsigned N = 4; // number of prefix permutations to test (including current) unsigned m_max_prefix_conflicts = 1000; - + scoped_ptr m_prefix_solver; scoped_ptr_vector m_param_probe_contexts; smt_params m_param_state; params_ref m_p; - - private: - void init_param_state() { - m_param_state.m_nl_arith_branching = true; - m_param_state.m_nl_arith_cross_nested = true; - m_param_state.m_nl_arith_delay = 10; - m_param_state.m_nl_arith_expensive_patching = false; - m_param_state.m_nl_arith_gb = true; - m_param_state.m_nl_arith_horner = true; - m_param_state.m_nl_arith_horner_frequency = 4; - m_param_state.m_nl_arith_optimize_bounds = true; - m_param_state.m_nl_arith_propagate_linear_monomials = true; - m_param_state.m_nl_arith_tangents = true; - m_param_state.updt_params(m_p); - ctx->updt_params(m_p); - }; + using param_value = std::variant; + symbol_table m_my_param_state; - smt_params mutate_param_state() { - smt_params p = m_param_state; - random_gen m_rand; + private: + void init_param_state(); - auto flip_bool = [&](bool &x) { - if ((m_rand() % 2) == 0) - x = !x; - }; + smt_params mutate_param_state(); - auto mutate_uint = [&](unsigned &x, unsigned lo, unsigned hi) { - if ((m_rand() % 2) == 0) - x = lo + (m_rand() % (hi - lo + 1)); - }; + public: + param_generator(parallel &p); + lbool run_prefix_step(); + void protocol_iteration(); + unsigned replay_proof_prefixes(vector candidate_param_states, unsigned max_conflicts_epsilon); - flip_bool(p.m_nl_arith_branching); - flip_bool(p.m_nl_arith_cross_nested); - mutate_uint(p.m_nl_arith_delay, 5, 20); - flip_bool(p.m_nl_arith_expensive_patching); - flip_bool(p.m_nl_arith_gb); - flip_bool(p.m_nl_arith_horner); - mutate_uint(p.m_nl_arith_horner_frequency, 2, 6); - flip_bool(p.m_nl_arith_optimize_bounds); - flip_bool(p.m_nl_arith_propagate_linear_monomials); - flip_bool(p.m_nl_arith_tangents); - - return p; - } - - public: - param_generator(parallel& p); - lbool run_prefix_step(); - void protocol_iteration(); - unsigned replay_proof_prefixes(vector candidate_param_states, unsigned max_conflicts_epsilon); - - reslimit& limit() { - return m.limit(); - } + reslimit &limit() { + return m.limit(); + } }; class worker {