mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-09-12 20:51:27 +00:00
Code Activity

make sure that worker state is properly deallocated

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2025-08-27 12:59:26 -07:00
parent ef8d2020ca
commit 631a3a27cf
2 changed files with 16 additions and 9 deletions
Download patch file Download diff file Expand all files Collapse all files

23
src/smt/smt_parallel.cpp
View file

@ -606,6 +606,8 @@ namespace smt {
double score_ratio = INFINITY; // score_pos / score_neg;
LOG_WORKER(0, " backbone candidate: " << mk_bounded_pp(candidate, m, 3) << " score_pos " << score_pos << " score_neg " << score_neg << "\n");
// if score_neg is zero (and thus score_pos > 0 since at this point score_pos != score_neg)
// then not(e) is a backbone candidate with score_ratio=infinity
if (score_neg == 0) {
@ -641,7 +643,7 @@ namespace smt {
backbone_candidates.push_back(p.second);
for (expr* e : backbone_candidates)
LOG_WORKER(1, " backbone candidate: " << mk_bounded_pp(e, m, 3) << " head size " << ctx->m_lit_scores->size() << " num vars " << ctx->get_num_bool_vars() << "\n");
LOG_WORKER(0, "selected backbone candidate: " << mk_bounded_pp(e, m, 3) << " head size " << ctx->m_lit_scores->size() << " num vars " << ctx->get_num_bool_vars() << "\n");
return backbone_candidates;
}
@ -656,10 +658,9 @@ namespace smt {
unsigned sz = asms.size();
for (expr* e : candidates) {
// push ¬c
expr* not_e = nullptr;
for (expr* e : candidates)
asms.push_back(m.mk_not(e));
LOG_WORKER(1, "PUSHED BACKBONES TO ASMS\n");
ctx->get_fparams().m_max_conflicts = 100;
@ -679,12 +680,18 @@ namespace smt {
asms.shrink(sz); // restore assumptions
LOG_WORKER(0, " BACKBONE CHECK RESULT: " << r << "\n");
if (r == l_false) {
// c must be true in all models → backbone
backbones.push_back(e);
LOG_WORKER(1, "backbone found: " << mk_bounded_pp(e, m, 3) << "\n");
auto core = ctx->unsat_core();
LOG_WORKER(0, "core: " << core << "\n");
if (core.size() == 1) {
expr* e = core.get(0);
backbones.push_back(mk_not(m, e));
}
}
}
return backbones;
}
@ -765,7 +772,7 @@ namespace smt {
struct scoped_clear {
parallel& p;
scoped_clear(parallel& p) : p(p) {}
~scoped_clear() { p.m_workers.clear(); p.m_assumptions_used.reset(); }
~scoped_clear() { p.m_workers.reset(); p.m_assumptions_used.reset(); }
};
scoped_clear clear(*this);

2
src/smt/smt_parallel.h
View file

@ -164,7 +164,7 @@ namespace smt {
obj_hashtable<expr> m_assumptions_used; // assumptions used in unsat cores, to be used in final core
batch_manager m_batch_manager;
ptr_vector<worker> m_workers;
scoped_ptr_vector<worker> m_workers;
public:
parallel(context& ctx) :