mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-13 01:21:14 +00:00
Code Activity

more param tuning setup

Browse source
This commit is contained in:
Ilana Shapiro 2025-10-28 23:33:42 -07:00
parent 432e2271ff
commit 7c15e63555
2 changed files with 64 additions and 19 deletions
Download patch file Download diff file Expand all files Collapse all files

47
src/smt/smt_parallel.cpp
View file

@ -64,8 +64,47 @@ namespace smt {
namespace smt { namespace smt {
void parallel::param_generator::run() { lbool parallel::param_generator::run_prefix_step() {
IF_VERBOSE(1, verbose_stream() << " Param generator running prefix step\n");
ctx->get_fparams().m_max_conflicts = m_max_prefix_conflicts;
lbool r = l_undef;
try {
r = ctx->check();
} catch (z3_error &err) {
b.set_exception(err.error_code());
} catch (z3_exception &ex) {
b.set_exception(ex.what());
} catch (...) {
b.set_exception("unknown exception");
}
return r;
}
void parallel::param_generator::protocol_iteration() {
IF_VERBOSE(1, verbose_stream() << " Param generator running protocol iteration\n");
ctx->get_fparams().m_max_conflicts = m_max_prefix_conflicts;
lbool r = run_prefix_step();
switch (r) {
case l_undef: {
return;
}
case l_true: {
IF_VERBOSE(1, verbose_stream() << " Param tuning thread found formula sat\n");
model_ref mdl;
ctx->get_model(mdl);
b.set_sat(m_l2g, *mdl);
return;
}
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 tuning thread determined formula unsat\n");
b.set_unsat(m_l2g, unsat_core);
return;
}
}
} }
void parallel::worker::run() { void parallel::worker::run() {
@ -148,8 +187,8 @@ namespace smt {
} }
parallel::param_generator::param_generator(parallel& p) parallel::param_generator::param_generator(parallel& p)
: p(p), b(p.m_batch_manager), m_params(p.ctx.get_fparams()), m_p(p.ctx.get_params()) { : p(p), b(p.m_batch_manager), m_best_param_state(p.ctx.get_fparams()), m_p(p.ctx.get_params()), m_l2g(m, p.ctx.m) {
ctx = alloc(context, m, m_params, m_p); ctx = alloc(context, m, m_best_param_state, m_p);
context::copy(p.ctx, *ctx, true); context::copy(p.ctx, *ctx, true);
// don't share initial units // don't share initial units
ctx->pop_to_base_lvl(); ctx->pop_to_base_lvl();
@ -515,7 +554,7 @@ namespace smt {
threads[i] = std::thread([&, i]() { m_workers[i]->run(); }); threads[i] = std::thread([&, i]() { m_workers[i]->run(); });
} }
// the final thread runs the parameter generator // the final thread runs the parameter generator
threads[num_threads - 1] = std::thread([&]() { m_param_generator.run(); }); threads[num_threads - 1] = std::thread([&]() { m_param_generator.protocol_iteration(); });
// Wait for all threads to finish // Wait for all threads to finish
for (auto &th : threads) for (auto &th : threads)

34
src/smt/smt_parallel.h
View file

@ -109,32 +109,38 @@ namespace smt {
parallel& p; parallel& p;
batch_manager& b; batch_manager& b;
ast_manager m; ast_manager m;
scoped_ptr<context> ctx;
ast_translation m_l2g;
unsigned N = 4; // number of prefix permutation testers unsigned N = 4; // number of prefix permutation testers
unsigned m_max_prefix_conflicts = 1000;
scoped_ptr<context> m_prefix_solver; scoped_ptr<context> m_prefix_solver;
scoped_ptr_vector<context> m_testers; // N testers scoped_ptr_vector<context> m_testers; // N testers
smt_params m_params; smt_params m_best_param_state;
params_ref m_p; params_ref m_p;
scoped_ptr<context> ctx;
private: private:
void init_param_state() { void init_param_state() {
m_params.m_nl_arith_branching = true; m_best_param_state.m_nl_arith_branching = true;
m_params.m_nl_arith_cross_nested = true; m_best_param_state.m_nl_arith_cross_nested = true;
m_params.m_nl_arith_delay = 10; m_best_param_state.m_nl_arith_delay = 10;
m_params.m_nl_arith_expensive_patching = false; m_best_param_state.m_nl_arith_expensive_patching = false;
m_params.m_nl_arith_gb = true; m_best_param_state.m_nl_arith_gb = true;
m_params.m_nl_arith_horner = true; m_best_param_state.m_nl_arith_horner = true;
m_params.m_nl_arith_horner_frequency = 4; m_best_param_state.m_nl_arith_horner_frequency = 4;
m_params.m_nl_arith_optimize_bounds = true; m_best_param_state.m_nl_arith_optimize_bounds = true;
m_params.m_nl_arith_propagate_linear_monomials = true; m_best_param_state.m_nl_arith_propagate_linear_monomials = true;
m_params.m_nl_arith_tangents = true; m_best_param_state.m_nl_arith_tangents = true;
m_params.updt_params(m_p); m_best_param_state.updt_params(m_p);
ctx->updt_params(m_p); ctx->updt_params(m_p);
}; };
public: public:
param_generator(parallel& p); param_generator(parallel& p);
void run(); lbool run_prefix_step();
void protocol_iteration();
void replay_proof_prefixes();
reslimit& limit() { reslimit& limit() {
return m.limit(); return m.limit();