From c010a3824462a3559d7246fbad5a6fd637fcfdf0 Mon Sep 17 00:00:00 2001 From: Ilana Shapiro Date: Tue, 26 Aug 2025 19:44:05 -0700 Subject: [PATCH] attempting to add backbone code, it does not work. still debugging the error: ASSERTION VIOLATION File: /home/t-ilshapiro/z3/src/ast/ast.cpp Line: 388 UNEXPECTED CODE WAS REACHED. I left a comment on the line where it's crashing --- src/params/smt_parallel_params.pyg | 1 + src/smt/smt_parallel.cpp | 131 +++++++++++++++++++---------- src/smt/smt_parallel.h | 5 +- 3 files changed, 92 insertions(+), 45 deletions(-) diff --git a/src/params/smt_parallel_params.pyg b/src/params/smt_parallel_params.pyg index 191d3b2ef..e20ca6d11 100644 --- a/src/params/smt_parallel_params.pyg +++ b/src/params/smt_parallel_params.pyg @@ -14,4 +14,5 @@ def_module_params('smt_parallel', ('max_greedy_cubes', UINT, 1000, 'maximum number of cube to greedily share before switching to frugal'), ('num_split_lits', UINT, 2, 'how many literals, k, we split on to create 2^k cubes'), ('frugal_depth_splitting_only', BOOL, False, 'only apply frugal cube strategy, and only on deepest (biggest) cubes from the batch manager'), + ('backbone_detection', BOOL, False, 'apply backbone literal heuristic'), )) diff --git a/src/smt/smt_parallel.cpp b/src/smt/smt_parallel.cpp index 84ea2c1c7..851b5f5cf 100644 --- a/src/smt/smt_parallel.cpp +++ b/src/smt/smt_parallel.cpp @@ -25,6 +25,8 @@ Author: #include "smt/smt_lookahead.h" #include "params/smt_parallel_params.hpp" +#include + #ifdef SINGLE_THREAD namespace smt { @@ -103,6 +105,17 @@ 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))); @@ -139,6 +152,7 @@ namespace smt { m_config.m_max_conflict_mul = pp.max_conflict_mul(); m_config.m_max_greedy_cubes = pp.max_greedy_cubes(); m_config.m_num_split_lits = pp.num_split_lits(); + m_config.m_backbone_detection = pp.backbone_detection(); // don't share initial units ctx->pop_to_base_lvl(); @@ -573,39 +587,53 @@ namespace smt { if (!e) continue; - auto score1 = ctx->m_phase_scores[0][v]; // assigned to true - auto score2 = ctx->m_phase_scores[1][v]; // assigned to false + auto score_pos = ctx->m_phase_scores[0][v]; // assigned to true + auto score_neg = ctx->m_phase_scores[1][v]; // assigned to false ctx->m_phase_scores[0][v] /= 2; // decay the scores ctx->m_phase_scores[1][v] /= 2; - if (score1 == 0 && score2 == 0) + if (score_pos == score_neg) continue; - if (score1 == 0) { - backbone_candidates.push_back(expr_ref(e, m)); - 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 { + score_ratio = score_pos / score_neg; } - if (score2 == 0) { - backbone_candidates.push_back(expr_ref(m.mk_not(e), m)); - continue; + if (score_ratio < 1) { // so score_pos < score_neg + candidate = expr_ref(m.mk_not(e), m); + // score_ratio *= -1; // insert by absolute value } - if (score1 == score2) - continue; + // insert into top_k. linear scan since k is very small + if (top_k.size() < k) { + top_k.push_back({score_ratio, candidate}); + } 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) + if (top_k[i].first < top_k[min_idx].first) + min_idx = i; - if (score1 >= score2) { - double ratio = score1 / score2; -// insert by absolute value - } - else { - double ratio = - score2 / score1; - // insert by absolute value + if (score_ratio > top_k[min_idx].first) { + top_k[min_idx] = {score_ratio, candidate}; + } } } - // post-process top_k to get the top k elements + for (auto& p : top_k) + backbone_candidates.push_back(expr_ref(p.second, m)); + + 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"); + return backbone_candidates; } @@ -614,40 +642,57 @@ namespace smt { // run the solver with a low budget of conflicts // if the unsat core contains a single candidate we have found a backbone literal // - void parallel::worker::test_backbone_candidates(expr_ref_vector const& candidates) { + expr_ref_vector parallel::worker::get_backbones_from_candidates(expr_ref_vector const& candidates) { + expr_ref_vector backbones(m); unsigned sz = asms.size(); - for (expr* e : candidates) - asms.push_back(mk_not(m, e)); + LOG_WORKER(0, "GETTING BACKBONES\n"); - ctx->get_fparams().m_max_conflicts = 100; - lbool r = l_undef; - try { - r = ctx->check(asms.size(), asms.data()); - } - catch (z3_error& err) { - b.set_exception(err.error_code()); - } - catch (z3_exception& ex) { - b.set_exception(ex.what()); - } - catch (...) { - b.set_exception("unknown exception"); - } - asms.shrink(sz); - if (r == l_false) { - auto core = ctx->unsat_core(); - LOG_WORKER(2, " backbone core:\n"; for (auto c : core) verbose_stream() << mk_bounded_pp(c, m, 3) << "\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"); + + ctx->get_fparams().m_max_conflicts = 100; + lbool r = l_undef; + try { + r = ctx->check(asms.size(), asms.data()); + } + catch (z3_error& err) { + b.set_exception(err.error_code()); + } + catch (z3_exception& ex) { + b.set_exception(ex.what()); + } + catch (...) { + b.set_exception("unknown exception"); + } + + asms.shrink(sz); // restore assumptions + + 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"); + } } - // TODO + return backbones; } expr_ref_vector parallel::worker::get_split_atoms() { unsigned k = 2; // auto candidates = ctx->m_pq_scores.get_heap(); - auto candidates = ctx->m_lit_scores; std::vector> top_k; // will hold at most k elements for (bool_var v = 0; v < ctx->get_num_bool_vars(); ++v) { @@ -667,7 +712,7 @@ namespace smt { if (top_k.size() < k) { top_k.push_back({score, e}); } else { - // find the smallest in top_k and replace if we found a new min + // 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) if (top_k[i].first < top_k[min_idx].first) diff --git a/src/smt/smt_parallel.h b/src/smt/smt_parallel.h index 7163f50d9..3f1e64b8f 100644 --- a/src/smt/smt_parallel.h +++ b/src/smt/smt_parallel.h @@ -123,8 +123,9 @@ namespace smt { double m_max_conflict_mul = 1.5; bool m_share_units_initial_only = false; bool m_cube_initial_only = false; - bool m_max_greedy_cubes = 1000; + unsigned m_max_greedy_cubes = 1000; unsigned m_num_split_lits = 2; + bool m_backbone_detection = false; }; unsigned id; // unique identifier for the worker @@ -146,7 +147,7 @@ namespace smt { } // allow for backoff scheme of conflicts within the thread for cube timeouts. expr_ref_vector find_backbone_candidates(); - void test_backbone_candidates(expr_ref_vector const& candidates); + expr_ref_vector get_backbones_from_candidates(expr_ref_vector const& candidates); public: worker(unsigned id, parallel& p, expr_ref_vector const& _asms); void run();