mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-14 14:55:25 +00:00
Code Activity

disable pre-processing during cubing

Browse source
This commit is contained in:
Nikolaj Bjorner 2025-07-31 20:58:58 -07:00
parent 2d876d5af1
commit 89cc9bd333
2 changed files with 13 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

9
src/smt/smt_lookahead.cpp
View file

@ -72,9 +72,14 @@ namespace smt {
svector<bool_var> vars;
for (bool_var v = 0; v < static_cast<bool_var>(sz); ++v) {
expr* b = ctx.bool_var2expr(v);
if (b && ctx.get_assignment(v) == l_undef) {
if (!b)
continue;
if (ctx.get_assignment(v) != l_undef)
continue;
if (m.is_and(b) || m.is_or(b) || m.is_not(b) || m.is_ite(b) || m.is_implies(b) || m.is_iff(b) || m.is_xor(b))
continue; // do not choose connectives
vars.push_back(v);
}
}
compare comp(ctx);
std::sort(vars.begin(), vars.end(), comp);

6
src/smt/smt_parallel.cpp
View file

@ -77,13 +77,16 @@ namespace smt {
throw default_exception("trace streams have to be off in parallel mode");
params_ref params = ctx.get_params();
for (unsigned i = 0; i < num_threads; ++i) {
smt_params.push_back(ctx.get_fparams());
smt_params.back().m_preprocess = false;
}
for (unsigned i = 0; i < num_threads; ++i) {
ast_manager* new_m = alloc(ast_manager, m, true);
pms.push_back(new_m);
pctxs.push_back(alloc(context, *new_m, smt_params[i], ctx.get_params()));
pctxs.push_back(alloc(context, *new_m, smt_params[i], params));
context& new_ctx = *pctxs.back();
context::copy(ctx, new_ctx, true);
new_ctx.set_random_seed(i + ctx.get_fparams().m_random_seed);
@ -108,6 +111,7 @@ namespace smt {
for (unsigned i = 0; i < num_threads; ++i) unit_lim.push_back(0);
std::function<void(void)> collect_units = [&,this]() {
//return; -- has overhead
for (unsigned i = 0; i < num_threads; ++i) {
context& pctx = *pctxs[i];
pctx.pop_to_base_lvl();