mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-25 15:09:32 +00:00
Code Activity

patch fix for default manager construction so it can be used to create the param tuning context without segfault

Browse source
This commit is contained in:
Ilana Shapiro 2025-11-03 10:47:58 -08:00
parent 06e195fb01
commit 5127569aaf
2 changed files with 6 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/smt/smt_parallel.cpp
View file

@ -317,7 +317,11 @@ namespace smt {
}
parallel::param_generator::param_generator(parallel& p)
: p(p), b(p.m_batch_manager), m_p(p.ctx.get_params()), m_l2g(m, p.ctx.m) {
: b(p.m_batch_manager), m_p(p.ctx.get_params()), m_l2g(m, p.ctx.m) {
// patch fix so that ctx = alloc(context, m, p.ctx.get_fparams(), m_p); doesn't crash due to some issue with default construction of m
ast_translation m_g2l(p.ctx.m, m);
m_g2l(p.ctx.m.mk_true());
ctx = alloc(context, m, p.ctx.get_fparams(), m_p);
context::copy(p.ctx, *ctx, true);
// don't share initial units

3
src/smt/smt_parallel.h
View file

@ -118,11 +118,9 @@ namespace smt {
using param_value = std::variant<unsigned_value, bool>;
using param_values = vector<std::pair<symbol, param_value>>;
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 m_max_prefix_conflicts = 1000;
@ -131,6 +129,7 @@ namespace smt {
vector<expr_ref_vector> m_recorded_cubes;
params_ref m_p;
param_values m_param_state;
ast_translation m_l2g;
params_ref apply_param_values(param_values const &pv);
void init_param_state();