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

initial parameter probe thread setup in C++

Browse source
This commit is contained in:
Ilana Shapiro 2025-10-28 17:23:51 -07:00
parent fbed108a7b
commit fd86c779ad
4 changed files with 72 additions and 10 deletions
Download patch file Download diff file Expand all files Collapse all files

10
src/params/theory_arith_params.cpp
View file

@ -22,6 +22,11 @@ Revision History:
void theory_arith_params::updt_params(params_ref const & _p) {
smt_params_helper p(_p);
m_nl_arith_delay = p.arith_nl_delay();
m_nl_arith_expensive_patching = p.arith_nl_expensive_patching();
m_nl_arith_horner = p.arith_nl_horner();
m_nl_arith_horner_frequency = p.arith_nl_horner_frequency();
m_nl_arith_tangents = p.arith_nl_tangents();
m_arith_random_initial_value = p.arith_random_initial_value();
m_arith_random_seed = p.random_seed();
m_arith_mode = static_cast<arith_solver_id>(p.arith_solver());
@ -102,4 +107,9 @@ void theory_arith_params::display(std::ostream & out) const {
DISPLAY_PARAM(m_arith_validate);
DISPLAY_PARAM(m_arith_dump_lemmas);
DISPLAY_PARAM(m_arith_epsilon);
DISPLAY_PARAM(m_nl_arith_delay);
DISPLAY_PARAM(m_nl_arith_expensive_patching);
DISPLAY_PARAM(m_nl_arith_horner);
DISPLAY_PARAM(m_nl_arith_horner_frequency);
DISPLAY_PARAM(m_nl_arith_tangents);
}

5
src/params/theory_arith_params.h
View file

@ -112,6 +112,11 @@ struct theory_arith_params {
bool m_nl_arith_propagate_linear_monomials = true;
bool m_nl_arith_optimize_bounds = true;
bool m_nl_arith_cross_nested = true;
unsigned m_nl_arith_delay = 10;
bool m_nl_arith_expensive_patching = false;
bool m_nl_arith_horner = true;
unsigned m_nl_arith_horner_frequency = 4;
bool m_nl_arith_tangents = true;
theory_arith_params(params_ref const & p = params_ref()) {
updt_params(p);

22
src/smt/smt_parallel.cpp
View file

@ -64,6 +64,10 @@ namespace smt {
namespace smt {
void parallel::param_generator::run() {
}
void parallel::worker::run() {
search_tree::node<cube_config> *node = nullptr;
expr_ref_vector cube(m);
@ -143,6 +147,16 @@ namespace smt {
m_num_initial_atoms = ctx->get_num_bool_vars();
}
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()) {
ctx = alloc(context, m, m_params, m_p);
context::copy(p.ctx, *ctx, true);
// don't share initial units
ctx->pop_to_base_lvl();
init_param_state();
IF_VERBOSE(1, verbose_stream() << "Initialized parameter generator\n");
}
void parallel::worker::share_units() {
// Collect new units learned locally by this worker and send to batch manager
ctx->pop_to_base_lvl();
@ -493,11 +507,15 @@ namespace smt {
for (auto w : m_workers)
sl.push_child(&(w->limit()));
sl.push_child(&(m_param_generator.limit()));
// Launch threads
vector<std::thread> threads(num_threads);
for (unsigned i = 0; i < num_threads; ++i) {
vector<std::thread> threads(num_threads + 1); // +1 for parameter generator
for (unsigned i = 0; i < num_threads - 1; ++i) {
threads[i] = std::thread([&, i]() { m_workers[i]->run(); });
}
// the final thread runs the parameter generator
threads[num_threads - 1] = std::thread([&]() { m_param_generator.run(); });
// Wait for all threads to finish
for (auto &th : threads)

43
src/smt/smt_parallel.h
View file

@ -77,8 +77,6 @@ namespace smt {
w->cancel();
}
void init_parameters_state();
public:
batch_manager(ast_manager& m, parallel& p) : m(m), p(p), m_search_tree(expr_ref(m)) { }
@ -107,11 +105,40 @@ namespace smt {
// 3. pick winner configuration if any are better than current.
// 4. update current configuration with the winner
class parameter_generator_thread {
unsigned N; // number of prefix permutation testers
scoped_ptr<context> prefix_solver;
scoped_ptr_vector<context> testers; // N testers
class param_generator {
parallel& p;
batch_manager& b;
ast_manager m;
unsigned N = 4; // number of prefix permutation testers
scoped_ptr<context> m_prefix_solver;
scoped_ptr_vector<context> m_testers; // N testers
smt_params m_params;
params_ref m_p;
scoped_ptr<context> ctx;
private:
void init_param_state() {
m_params.m_nl_arith_branching = true;
m_params.m_nl_arith_cross_nested = true;
m_params.m_nl_arith_delay = 10;
m_params.m_nl_arith_expensive_patching = false;
m_params.m_nl_arith_gb = true;
m_params.m_nl_arith_horner = true;
m_params.m_nl_arith_horner_frequency = 4;
m_params.m_nl_arith_optimize_bounds = true;
m_params.m_nl_arith_propagate_linear_monomials = true;
m_params.m_nl_arith_tangents = true;
m_params.updt_params(m_p);
ctx->updt_params(m_p);
};
public:
param_generator(parallel& p);
void run();
reslimit& limit() {
return m.limit();
}
};
class worker {
@ -173,6 +200,7 @@ namespace smt {
batch_manager m_batch_manager;
scoped_ptr_vector<worker> m_workers;
param_generator m_param_generator;
public:
parallel(context& ctx) :
@ -180,7 +208,8 @@ namespace smt {
num_threads(std::min(
(unsigned)std::thread::hardware_concurrency(),
ctx.get_fparams().m_threads)),
m_batch_manager(ctx.m, *this) {}
m_batch_manager(ctx.m, *this),
m_param_generator(*this) {}
lbool operator()(expr_ref_vector const& asms);
};