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

neatify

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2025-10-31 00:39:52 -07:00
parent 605a4744c6
commit f0d03e99c4
2 changed files with 60 additions and 63 deletions
Download patch file Download diff file Expand all files Collapse all files

77
src/smt/smt_parallel.cpp
View file

@ -83,17 +83,18 @@ namespace smt {
return r; return r;
} }
std::pair<parallel::param_generator::param_values, bool> parallel::param_generator::replay_proof_prefixes(unsigned max_conflicts_epsilon=200) { void parallel::param_generator::replay_proof_prefixes(unsigned max_conflicts_epsilon=200) {
unsigned conflict_budget = m_max_prefix_conflicts + max_conflicts_epsilon; unsigned conflict_budget = m_max_prefix_conflicts + max_conflicts_epsilon;
param_values best_param_state; param_values best_param_state;
double best_score; double best_score = 0;
bool found_better_params = false; bool found_better_params = false;
for (unsigned i = 0; i < N; ++i) { for (unsigned i = 0; i <= N; ++i) {
IF_VERBOSE(1, verbose_stream() << " PARAM TUNER: replaying proof prefix in param probe context " << i << "\n"); IF_VERBOSE(1, verbose_stream() << " PARAM TUNER: replaying proof prefix in param probe context " << i << "\n");
// copy prefix solver context to a new probe_ctx for next replay with candidate mutation // copy prefix solver context to a new probe_ctx for next replay with candidate mutation
scoped_ptr<context> probe_ctx = alloc(context, m, ctx->get_fparams(), m_p); smt_params smtp(m_p);
scoped_ptr<context> probe_ctx = alloc(context, m, smtp, m_p);
context::copy(*ctx, *probe_ctx, true); context::copy(*ctx, *probe_ctx, true);
// apply a candidate (mutated) param state to probe_ctx // apply a candidate (mutated) param state to probe_ctx
@ -111,23 +112,36 @@ namespace smt {
// replay the cube (negation of the clause) // replay the cube (negation of the clause)
for (expr_ref_vector const& cube : probe_ctx->m_recorded_cubes) { for (expr_ref_vector const& cube : probe_ctx->m_recorded_cubes) {
lbool r = probe_ctx->check(cube.size(), cube.data()); lbool r = probe_ctx->check(cube.size(), cube.data());
unsigned conflicts = probe_ctx->m_stats.m_num_conflicts; unsigned conflicts = probe_ctx->m_stats.m_num_conflicts;
unsigned decisions = probe_ctx->m_stats.m_num_decisions; unsigned decisions = probe_ctx->m_stats.m_num_decisions;
IF_VERBOSE(1, verbose_stream() << " PARAM TUNER " << i << ": cube replay result " << r <<
", conflicts = " << conflicts << ", decisions = " << decisions << "\n");
score += conflicts + decisions; score += conflicts + decisions;
} }
if (i > 0 && score < best_score) { if (i == 0) {
best_score = score;
IF_VERBOSE(1, verbose_stream() << " PARAM TUNER: baseline score = " << best_score << "\n");
}
else if (score < best_score) {
found_better_params = true; found_better_params = true;
best_param_state = mutated_param_state; best_param_state = mutated_param_state;
best_score = score; best_score = score;
} else {
best_score = score;
} }
} }
// NOTE: we either need to apply the best params found that are better than base line
return {best_param_state, found_better_params}; // or, we have to implement a comparison operator for param_values (what would this do?)
// or, we update the param state every single time even if it hasn't changed (what would this do?)
// for now, I went with option 1
if (found_better_params) {
m_param_state = best_param_state;
auto p = apply_param_values(m_param_state);
b.set_param_state(p);
IF_VERBOSE(1, verbose_stream() << " PARAM TUNER found better param state\n");
}
else {
IF_VERBOSE(1, verbose_stream() << " PARAM TUNER retained current param state\n");
}
} }
void parallel::param_generator::init_param_state() { void parallel::param_generator::init_param_state() {
@ -144,9 +158,23 @@ namespace smt {
m_param_state.push_back( m_param_state.push_back(
{symbol("smt.arith.nl.propagate_linear_monomials"), smtp.arith_nl_propagate_linear_monomials()}); {symbol("smt.arith.nl.propagate_linear_monomials"), smtp.arith_nl_propagate_linear_monomials()});
m_param_state.push_back({symbol("smt.arith.nl.tangents"), smtp.arith_nl_tangents()}); m_param_state.push_back({symbol("smt.arith.nl.tangents"), smtp.arith_nl_tangents()});
}; };
params_ref parallel::param_generator::apply_param_values(param_values const &pv) {
params_ref p = m_p;
for (auto const &[k, v] : pv) {
if (std::holds_alternative<unsigned_value>(v)) {
unsigned_value uv = std::get<unsigned_value>(v);
p.set_uint(k, uv.value);
}
else if (std::holds_alternative<bool>(v)) {
bool bv = std::get<bool>(v);
p.set_bool(k, bv);
}
}
return p;
}
parallel::param_generator::param_values parallel::param_generator::mutate_param_state() { parallel::param_generator::param_values parallel::param_generator::mutate_param_state() {
param_values new_param_values(m_param_state); param_values new_param_values(m_param_state);
unsigned index = ctx->get_random_value() % new_param_values.size(); unsigned index = ctx->get_random_value() % new_param_values.size();
@ -161,7 +189,7 @@ namespace smt {
while (new_value == value) { while (new_value == value) {
new_value = lo + ctx->get_random_value() % (hi - lo + 1); new_value = lo + ctx->get_random_value() % (hi - lo + 1);
} }
std::get<unsigned_value>(param.second).value = new_value; std::get_if<unsigned_value>(&param.second)->value = new_value;
} }
return new_param_values; return new_param_values;
} }
@ -174,20 +202,7 @@ namespace smt {
switch (r) { switch (r) {
case l_undef: { case l_undef: {
auto [best_param_state, found_better_params] = replay_proof_prefixes(); replay_proof_prefixes();
// NOTE: we either need to return a pair from replay_proof_prefixes so we can return a boolean flag indicating whether better params were found.
// or, we have to implement a comparison operator for param_values
// or, we update the param state every single time even if it hasn't changed
// for now, I went with option 1
if (found_better_params) {
m_param_state = best_param_state;
auto p = apply_param_values(m_param_state);
b.set_param_state(p);
IF_VERBOSE(1, verbose_stream() << " PARAM TUNER found better param state\n");
} else {
IF_VERBOSE(1, verbose_stream() << " PARAM TUNER retained current param state\n");
}
} }
case l_true: { case l_true: {
IF_VERBOSE(1, verbose_stream() << " PARAM TUNER found formula sat\n"); IF_VERBOSE(1, verbose_stream() << " PARAM TUNER found formula sat\n");
@ -222,9 +237,8 @@ namespace smt {
LOG_WORKER(1, " CUBE SIZE IN MAIN LOOP: " << cube.size() << "\n"); LOG_WORKER(1, " CUBE SIZE IN MAIN LOOP: " << cube.size() << "\n");
// apply current best param state from batch manager // apply current best param state from batch manager
smt_params params = b.get_best_param_state();
params_ref p; params_ref p;
params.updt_params(p); b.get_param_state(p);
ctx->updt_params(p); ctx->updt_params(p);
lbool r = check_cube(cube); lbool r = check_cube(cube);
@ -454,10 +468,9 @@ namespace smt {
} }
} }
// todo make this thread safe by not using reference counts implicit in params ref but instead copying the entire structure. void parallel::batch_manager::get_param_state(params_ref& p) {
params_ref parallel::batch_manager::get_best_param_state() {
std::scoped_lock lock(mux); std::scoped_lock lock(mux);
return m_param_state; p.copy(m_param_state);
} }
void parallel::worker::collect_shared_clauses() { void parallel::worker::collect_shared_clauses() {

38
src/smt/smt_parallel.h
View file

@ -89,9 +89,9 @@ namespace smt {
void set_exception(std::string const& msg); void set_exception(std::string const& msg);
void set_exception(unsigned error_code); void set_exception(unsigned error_code);
void set_param_state(params_ref const& p) { m_param_state.copy(p); } void set_param_state(params_ref const& p) { m_param_state.copy(p); }
void get_param_state(params_ref &p);
void collect_statistics(::statistics& st) const; void collect_statistics(::statistics& st) const;
params_ref get_best_param_state();
bool get_cube(ast_translation& g2l, unsigned id, expr_ref_vector& cube, node*& n); bool get_cube(ast_translation& g2l, unsigned id, expr_ref_vector& cube, node*& n);
void backtrack(ast_translation& l2g, expr_ref_vector const& core, node* n); void backtrack(ast_translation& l2g, expr_ref_vector const& core, node* n);
void split(ast_translation& l2g, unsigned id, node* n, expr* atom); void split(ast_translation& l2g, unsigned id, node* n, expr* atom);
@ -110,6 +110,14 @@ namespace smt {
// 4. update current configuration with the winner // 4. update current configuration with the winner
class param_generator { class param_generator {
struct unsigned_value {
unsigned value;
unsigned min_value;
unsigned max_value;
};
using param_value = std::variant<unsigned_value, bool>;
using param_values = vector<std::pair<symbol, param_value>>;
parallel &p; parallel &p;
batch_manager &b; batch_manager &b;
ast_manager m; ast_manager m;
@ -120,42 +128,18 @@ namespace smt {
unsigned m_max_prefix_conflicts = 1000; unsigned m_max_prefix_conflicts = 1000;
scoped_ptr<context> m_prefix_solver; scoped_ptr<context> m_prefix_solver;
scoped_ptr_vector<context> m_param_probe_contexts;
params_ref m_p; params_ref m_p;
struct unsigned_value {
unsigned value;
unsigned min_value;
unsigned max_value;
};
using param_value = std::variant<unsigned_value, bool>;
using param_values = vector<std::pair<symbol, param_value>>;
param_values m_param_state; param_values m_param_state;
params_ref apply_param_values(param_values const &pv) { params_ref apply_param_values(param_values const &pv);
params_ref p = m_p;
for (auto const& [k, v] : pv) {
if (std::holds_alternative<unsigned_value>(v)) {
unsigned_value uv = std::get<unsigned_value>(v);
p.set_uint(k, uv.value);
} else if (std::holds_alternative<bool>(v)) {
bool bv = std::get<bool>(v);
p.set_bool(k, bv);
}
}
return p;
}
private:
void init_param_state(); void init_param_state();
param_values mutate_param_state(); param_values mutate_param_state();
public: public:
param_generator(parallel &p); param_generator(parallel &p);
lbool run_prefix_step(); lbool run_prefix_step();
void protocol_iteration(); void protocol_iteration();
std::pair<parallel::param_generator::param_values, bool> replay_proof_prefixes(unsigned max_conflicts_epsilon); void replay_proof_prefixes(unsigned max_conflicts_epsilon);
reslimit &limit() { reslimit &limit() {
return m.limit(); return m.limit();