mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-09-29 20:59:01 +00:00
Code Activity

debug the backbone crash (it was references not being counted)

Browse source
This commit is contained in:
Ilana Shapiro 2025-08-27 10:08:48 -07:00
parent 04ef9dc655
commit 44e3f22c8b
1 changed files with 25 additions and 33 deletions
Download patch file Download diff file Expand all files Collapse all files

58
src/smt/smt_parallel.cpp
View file

@ -77,6 +77,16 @@ namespace smt {
auto split_atoms = get_split_atoms();
b.return_cubes(m_l2g, returned_cubes, split_atoms);
}
if (m_config.m_backbone_detection) {
expr_ref_vector backbone_candidates = find_backbone_candidates();
expr_ref_vector backbones = get_backbones_from_candidates(backbone_candidates);
if (!backbones.empty()) { // QUESTION: how do we avoid splitting on backbones????
for (expr* bb : backbones) {
ctx->assert_expr(bb); // local pruning
b.collect_clause(m_l2g, id, bb); // share globally // QUESTION: gatekeep this behind share_units param????
}
}
}
update_max_thread_conflicts();
break;
}
@ -105,17 +115,6 @@ namespace smt {
if (asms.contains(e))
b.report_assumption_used(m_l2g, e); // report assumptions used in unsat core, so they can be used in final core
if (m_config.m_backbone_detection) {
expr_ref_vector backbone_candidates = find_backbone_candidates();
expr_ref_vector backbones = get_backbones_from_candidates(backbone_candidates);
if (!backbones.empty()) { // QUESTION: how do we avoid splitting on backbones????
for (expr* bb : backbones) {
ctx->assert_expr(bb); // local pruning
b.collect_clause(m_l2g, id, bb); // share globally // QUESTION: gatekeep this behind share_units param????
}
}
}
LOG_WORKER(1, " found unsat cube\n");
if (m_config.m_share_conflicts)
b.collect_clause(m_l2g, id, mk_not(mk_and(unsat_core)));
@ -586,13 +585,14 @@ namespace smt {
// Find backbone candidates based on the current state of the worker
unsigned k = 5;
svector<std::pair<double, expr*>> top_k; // will hold at most k elements
vector<std::pair<double, expr_ref>> top_k; // will hold at most k elements
expr_ref candidate(m);
for (bool_var v = 0; v < ctx->get_num_bool_vars(); ++v) {
if (ctx->get_assignment(v) != l_undef)
continue;
expr* e = ctx->bool_var2expr(v);
if (!e)
candidate = ctx->bool_var2expr(v);
if (!candidate)
continue;
auto score_pos = ctx->m_phase_scores[0][v]; // assigned to true
@ -605,25 +605,26 @@ namespace smt {
continue;
double score_ratio = INFINITY; // score_pos / score_neg;
expr_ref candidate = expr_ref(e, m);
// 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) {
candidate = expr_ref(m.mk_not(e), m);
} else {
candidate = mk_not(candidate);
}
else {
score_ratio = score_pos / score_neg;
}
if (score_ratio < 1) { // so score_pos < score_neg
candidate = expr_ref(m.mk_not(e), m);
candidate = mk_not(candidate);
// score_ratio *= -1; // insert by absolute value
}
// insert into top_k. linear scan since k is very small
if (top_k.size() < k) {
top_k.push_back({score_ratio, candidate});
} else {
}
else {
// find the smallest in top_k and replace if we found a new element bigger than the min
size_t min_idx = 0;
for (size_t i = 1; i < k; ++i)
@ -637,10 +638,10 @@ namespace smt {
}
for (auto& p : top_k)
backbone_candidates.push_back(expr_ref(p.second, m));
backbone_candidates.push_back(p.second);
for (expr* e : backbone_candidates)
LOG_WORKER(0, " 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(1, " 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;
}
@ -654,21 +655,12 @@ namespace smt {
expr_ref_vector backbones(m);
unsigned sz = asms.size();
LOG_WORKER(0, "GETTING BACKBONES\n");
for (expr* e : candidates) {
// push ¬c
expr* not_e = nullptr;
if (m.is_bool(e)) { // IT CRASHES ON THIS LINE?????
LOG_WORKER(0, "candidate IS Bool: " << mk_bounded_pp(e, m, 3) << "\n");
not_e = m.mk_not(e);
} else {
// e is a theory atom represented in the SAT solver
LOG_WORKER(0, "candidate is NOT Bool: " << mk_bounded_pp(e, m, 3) << "\n");
}
LOG_WORKER(0, "NEGATED BACKBONE\n");
asms.push_back(not_e);
LOG_WORKER(0, "PUSHED BACKBONES TO ASMS\n");
asms.push_back(m.mk_not(e));
LOG_WORKER(1, "PUSHED BACKBONES TO ASMS\n");
ctx->get_fparams().m_max_conflicts = 100;
lbool r = l_undef;
@ -690,7 +682,7 @@ namespace smt {
if (r == l_false) {
// c must be true in all models → backbone
backbones.push_back(e);
LOG_WORKER(0, "backbone found: " << mk_bounded_pp(e, m, 3) << "\n");
LOG_WORKER(1, "backbone found: " << mk_bounded_pp(e, m, 3) << "\n");
}
}