mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-05 22:06:03 +00:00
Code Activity

merge

Browse source
This commit is contained in:
Ilana Shapiro 2025-10-30 14:40:06 -07:00
commit 20ede9d1b3
2 changed files with 73 additions and 59 deletions
Download patch file Download diff file Expand all files Collapse all files

57
src/smt/smt_parallel.cpp
View file

@ -70,11 +70,14 @@ namespace smt {
lbool r = l_undef; lbool r = l_undef;
try { try {
r = ctx->check(); r = ctx->check();
} catch (z3_error &err) { }
catch (z3_error &err) {
b.set_exception(err.error_code()); b.set_exception(err.error_code());
} catch (z3_exception &ex) { }
catch (z3_exception &ex) {
b.set_exception(ex.what()); b.set_exception(ex.what());
} catch (...) { }
catch (...) {
b.set_exception("unknown exception"); b.set_exception("unknown exception");
} }
return r; return r;
@ -128,6 +131,52 @@ namespace smt {
return best_param_state_idx; 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() { void parallel::param_generator::protocol_iteration() {
IF_VERBOSE(1, verbose_stream() << " PARAM TUNER running protocol iteration\n"); IF_VERBOSE(1, verbose_stream() << " PARAM TUNER running protocol iteration\n");
ctx->get_fparams().m_max_conflicts = m_max_prefix_conflicts; ctx->get_fparams().m_max_conflicts = m_max_prefix_conflicts;
@ -142,6 +191,8 @@ namespace smt {
switch (r) { switch (r) {
case l_undef: { 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; smt_params best_param_state = m_param_state;
vector<smt_params> candidate_param_states; vector<smt_params> candidate_param_states;

71
src/smt/smt_parallel.h
View file

@ -20,7 +20,7 @@ Revision History:
#include "smt/smt_context.h" #include "smt/smt_context.h"
#include "util/search_tree.h" #include "util/search_tree.h"
// #include "util/util.h" #include <variant>
#include <thread> #include <thread>
#include <mutex> #include <mutex>
@ -127,13 +127,13 @@ namespace smt {
// 4. update current configuration with the winner // 4. update current configuration with the winner
class param_generator { class param_generator {
parallel& p; parallel &p;
batch_manager& b; batch_manager &b;
ast_manager m; ast_manager m;
scoped_ptr<context> ctx; scoped_ptr<context> ctx;
ast_translation m_l2g; 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; unsigned m_max_prefix_conflicts = 1000;
scoped_ptr<context> m_prefix_solver; scoped_ptr<context> m_prefix_solver;
@ -141,60 +141,23 @@ namespace smt {
smt_params m_param_state; smt_params m_param_state;
params_ref m_p; params_ref m_p;
private: using param_value = std::variant<unsigned, bool, double>;
void init_param_state() { symbol_table<param_value> m_my_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); private:
ctx->updt_params(m_p); void init_param_state();
};
smt_params mutate_param_state() { smt_params mutate_param_state();
smt_params p = m_param_state;
random_gen m_rand;
auto flip_bool = [&](bool &x) { public:
if ((m_rand() % 2) == 0) param_generator(parallel &p);
x = !x; lbool run_prefix_step();
}; void protocol_iteration();
unsigned replay_proof_prefixes(vector<smt_params> candidate_param_states, unsigned max_conflicts_epsilon);
auto mutate_uint = [&](unsigned &x, unsigned lo, unsigned hi) { reslimit &limit() {
if ((m_rand() % 2) == 0) return m.limit();
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;
}
public:
param_generator(parallel& p);
lbool run_prefix_step();
void protocol_iteration();
unsigned replay_proof_prefixes(vector<smt_params> candidate_param_states, unsigned max_conflicts_epsilon);
reslimit& limit() {
return m.limit();
}
}; };
class worker { class worker {