mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-09-08 02:31:24 +00:00
Code Activity

attempting to add backbone code, it does not work. still debugging the error: ASSERTION VIOLATION

Browse source 
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
This commit is contained in:
Ilana Shapiro 2025-08-26 19:44:05 -07:00
parent 307a8c5932
commit c010a38244
3 changed files with 92 additions and 45 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/params/smt_parallel_params.pyg
View file

@ -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'),
))

131
src/smt/smt_parallel.cpp
View file

@ -25,6 +25,8 @@ Author:
#include "smt/smt_lookahead.h"
#include "params/smt_parallel_params.hpp"
#include <cmath>
#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<std::pair<double, expr*>> 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)

5
src/smt/smt_parallel.h
View file

@ -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();