mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-31 11:42:28 +00:00
Code Activity

move to generic state

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2025-10-30 11:45:00 -07:00
parent a74153ffa3
commit d3e2527899
2 changed files with 73 additions and 58 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;
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;
@ -130,6 +133,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;
@ -144,6 +193,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<smt_params> candidate_param_states;

74
src/smt/smt_parallel.h
View file

@ -20,6 +20,7 @@ Revision History:
#include "smt/smt_context.h"
#include "util/search_tree.h"
#include <variant>
// #include "util/util.h"
#include <thread>
#include <mutex>
@ -127,74 +128,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<context> 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<context> m_prefix_solver;
scoped_ptr_vector<context> 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<unsigned, bool, double>;
symbol_table<param_value> 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<smt_params> 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<smt_params> candidate_param_states, unsigned max_conflicts_epsilon);
reslimit& limit() {
return m.limit();
}
reslimit &limit() {
return m.limit();
}
};
class worker {