mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-26 21:16:02 +00:00
Code Activity

fix bug

Browse source
This commit is contained in:
Ilana Shapiro 2025-07-31 13:19:36 -07:00
parent 8a6cbec4f0
commit e6213f8b04
1 changed files with 14 additions and 15 deletions
Download patch file Download diff file Expand all files Collapse all files

29
src/smt/smt_parallel.cpp
View file

@ -139,7 +139,6 @@ namespace smt {
unsigned k = 4; // Get top-k scoring literals unsigned k = 4; // Get top-k scoring literals
ast_manager& m = ctx.get_manager(); ast_manager& m = ctx.get_manager();
// std::cout << ctx.m_bool_var2expr.size() << std::endl; // Prints the size of m_bool_var2expr
// Loop over first 100 Boolean vars // Loop over first 100 Boolean vars
for (bool_var v = 0; v < 100; ++v) { for (bool_var v = 0; v < 100; ++v) {
if (ctx.get_assignment(v) != l_undef) continue; if (ctx.get_assignment(v) != l_undef) continue;
@ -215,15 +214,15 @@ namespace smt {
// Lambda defining the work each SMT thread performs // Lambda defining the work each SMT thread performs
auto worker_thread = [&](int i, expr_ref_vector cube_batch) { auto worker_thread = [&](int i, expr_ref_vector cube_batch) {
try { try {
std::cout << "Starting thread " << i <<"\n";
// Get thread-specific context and AST manager // Get thread-specific context and AST manager
context& pctx = *pctxs[i]; context& pctx = *pctxs[i];
ast_manager& pm = *pms[i]; ast_manager& pm = *pms[i];
// Initialize local assumptions and cube // Initialize local assumptions and cube
expr_ref_vector lasms(pasms[i]); expr_ref_vector lasms(pasms[i]);
expr_ref c(mk_or(cube_batch), pm); expr_ref c = mk_or(cube_batch);
lasms.push_back(c); // <-- add cube to assumptions std::cout << "Thread " << i << " initial cube: " << mk_pp(c, pm) << "\n";
lasms.push_back(c);
// Set the max conflict limit for this thread // Set the max conflict limit for this thread
pctx.get_fparams().m_max_conflicts = std::min(thread_max_conflicts, max_conflicts); pctx.get_fparams().m_max_conflicts = std::min(thread_max_conflicts, max_conflicts);
@ -247,13 +246,13 @@ namespace smt {
if (r == l_undef && pctx.m_num_conflicts >= max_conflicts) if (r == l_undef && pctx.m_num_conflicts >= max_conflicts)
; // no-op, allow loop to continue ; // no-op, allow loop to continue
else if (r == l_undef && pctx.m_num_conflicts >= thread_max_conflicts) else if (r == l_undef && pctx.m_num_conflicts >= thread_max_conflicts)
return r; // quit thread early return; // quit thread early
// If cube was unsat and it's in the core, learn from it. i.e. a thread can be UNSAT because the cube c contradicted F. In this case learn the negation of the cube ¬c // If cube was unsat and it's in the core, learn from it. i.e. a thread can be UNSAT because the cube c contradicted F. In this case learn the negation of the cube ¬c
// TAKE THE INTERSECTION INSTEAD OF CHECKING MEMBERSHIP, SEE WHITEBOARD NOTES // TAKE THE INTERSECTION INSTEAD OF CHECKING MEMBERSHIP, SEE WHITEBOARD NOTES
else if (r == l_false && intersects(cube_batch, pctx.unsat_core())) { // pctx.unsat_core().contains(c)) { THIS IS THE VERSION FOR SINGLE LITERAL CUBES else if (r == l_false && intersects(cube_batch, pctx.unsat_core())) { // pctx.unsat_core().contains(c)) { THIS IS THE VERSION FOR SINGLE LITERAL CUBES
IF_VERBOSE(1, verbose_stream() << "(smt.thread " << i << " :learn " << mk_bounded_pp(c, pm, 3) << ")"); IF_VERBOSE(1, verbose_stream() << "(smt.thread " << i << " :learn " << mk_bounded_pp(c, pm, 3) << ")");
pctx.assert_expr(mk_not(mk_and(pctx.unsat_core()))); pctx.assert_expr(mk_not(mk_and(pctx.unsat_core())));
return r; return;
} }
// Begin thread-safe update of shared result state // Begin thread-safe update of shared result state
@ -270,15 +269,13 @@ namespace smt {
finished_id = i; finished_id = i;
result = r; result = r;
} }
else if (!first) return r; // nothing new to contribute else if (!first) return; // nothing new to contribute
} }
// Cancel limits on other threads now that a result is known // Cancel limits on other threads now that a result is known
for (ast_manager* m : pms) { for (ast_manager* m : pms) {
if (m != &pm) m->limit().cancel(); if (m != &pm) m->limit().cancel();
} }
return r;
} catch (z3_error & err) { } catch (z3_error & err) {
if (finished_id == UINT_MAX) { if (finished_id == UINT_MAX) {
error_code = err.error_code(); error_code = err.error_code();
@ -298,7 +295,6 @@ namespace smt {
done = true; done = true;
} }
} }
return l_undef; // Return undef if an exception occurred
}; };
struct BatchManager { struct BatchManager {
@ -350,7 +346,7 @@ namespace smt {
std::cout << "Top lits:\n"; std::cout << "Top lits:\n";
for (unsigned j = 0; j < top_lits.size(); ++j) { for (unsigned j = 0; j < top_lits.size(); ++j) {
std::cout << " [" << j << "] " << top_lits[j].get() << "\n"; std::cout << " [" << j << "] " << mk_pp(top_lits[j].get(), m) << "\n";
} }
unsigned num_lits = top_lits.size(); unsigned num_lits = top_lits.size();
@ -372,7 +368,7 @@ namespace smt {
std::cout << "Cubes out:\n"; std::cout << "Cubes out:\n";
for (size_t j = 0; j < cube_batch.size(); ++j) { for (size_t j = 0; j < cube_batch.size(); ++j) {
std::cout << " [" << j << "] " << cube_batch[j].get() << "\n"; std::cout << " [" << j << "] " << mk_pp(cube_batch[j].get(), m) << "\n";
} }
return cube_batch; return cube_batch;
@ -398,16 +394,19 @@ namespace smt {
cube_batches.push_back(std::move(batch)); cube_batches.push_back(std::move(batch));
} }
batch_idx = 0; // Reset index for next round
return cube_batches; return cube_batches;
} }
}; };
BatchManager batch_manager(1); BatchManager batch_manager(2);
batch_manager.batches = batch_manager.gen_new_batches(ctx);
// Thread scheduling loop // Thread scheduling loop
while (true) { while (true) {
if (batch_manager.batch_idx >= batch_manager.batches.size()) {
batch_manager.batches = batch_manager.gen_new_batches(ctx);
}
std::vector<std::thread> threads(num_threads); std::vector<std::thread> threads(num_threads);
// Launch threads // Launch threads