mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-26 13:06:05 +00:00
Code Activity

turn off logging at level 0 for testing

Browse source
This commit is contained in:
Ilana Shapiro 2025-08-12 16:10:56 -07:00
parent efa52193d7
commit 4bd40e916b
2 changed files with 15 additions and 15 deletions
Download patch file Download diff file Expand all files Collapse all files

24
src/smt/smt_parallel.cpp
View file

@ -54,15 +54,15 @@ namespace smt {
b.set_exception("context cancelled");
return;
}
IF_VERBOSE(0, verbose_stream() << "Worker " << id << " cube: " << mk_bounded_pp(mk_and(cube), m, 3) << "\n");
IF_VERBOSE(1, verbose_stream() << "Worker " << id << " cube: " << mk_bounded_pp(mk_and(cube), m, 3) << "\n");
lbool r = check_cube(cube);
if (m.limit().is_canceled()) {
IF_VERBOSE(0, verbose_stream() << "Worker " << id << " context cancelled\n");
IF_VERBOSE(1, verbose_stream() << "Worker " << id << " context cancelled\n");
return;
}
switch (r) {
case l_undef: {
IF_VERBOSE(0, verbose_stream() << "Worker " << id << " found undef cube\n");
IF_VERBOSE(1, verbose_stream() << "Worker " << id << " found undef cube\n");
// return unprocessed cubes to the batch manager
// add a split literal to the batch manager.
// optionally process other cubes and delay sending back unprocessed cubes to batch manager.
@ -74,7 +74,7 @@ namespace smt {
break;
}
case l_true: {
IF_VERBOSE(0, verbose_stream() << "Worker " << id << " found sat cube\n");
IF_VERBOSE(1, verbose_stream() << "Worker " << id << " found sat cube\n");
model_ref mdl;
ctx->get_model(mdl);
b.set_sat(l2g, *mdl);
@ -86,11 +86,11 @@ namespace smt {
// share with batch manager.
// process next cube.
expr_ref_vector const& unsat_core = ctx->unsat_core();
IF_VERBOSE(0, verbose_stream() << "unsat core: " << unsat_core << "\n");
IF_VERBOSE(1, verbose_stream() << "unsat core: " << unsat_core << "\n");
// If the unsat core only contains assumptions,
// unsatisfiability does not depend on the current cube and the entire problem is unsat.
if (all_of(unsat_core, [&](expr* e) { return asms.contains(e); })) {
IF_VERBOSE(0, verbose_stream() << "Worker " << id << " determined formula unsat\n");
IF_VERBOSE(1, verbose_stream() << "Worker " << id << " determined formula unsat\n");
b.set_unsat(l2g, unsat_core);
return;
}
@ -98,7 +98,7 @@ namespace smt {
if (asms.contains(e))
b.report_assumption_used(l2g, e); // report assumptions used in unsat core, so they can be used in final core
IF_VERBOSE(0, verbose_stream() << "Worker " << id << " found unsat cube\n");
IF_VERBOSE(1, verbose_stream() << "Worker " << id << " found unsat cube\n");
b.collect_clause(l2g, id, mk_not(mk_and(unsat_core)));
break;
}
@ -112,7 +112,7 @@ namespace smt {
ast_translation g2l(p.ctx.m, m);
for (auto e : _asms)
asms.push_back(g2l(e));
IF_VERBOSE(0, verbose_stream() << "Worker " << id << " created with " << asms.size() << " assumptions\n");
IF_VERBOSE(1, verbose_stream() << "Worker " << id << " created with " << asms.size() << " assumptions\n");
m_smt_params.m_preprocess = false;
ctx = alloc(context, m, m_smt_params, p.ctx.get_params());
context::copy(p.ctx, *ctx, true);
@ -151,7 +151,7 @@ namespace smt {
for (expr* e : new_clauses) {
expr_ref local_clause(e, g2l.to()); // e was already translated to the local context in the batch manager!!
ctx->assert_expr(local_clause); // assert the clause in the local context
IF_VERBOSE(0, verbose_stream() << "Worker " << id << " asserting shared clause: " << mk_bounded_pp(local_clause, m, 3) << "\n");
IF_VERBOSE(1, verbose_stream() << "Worker " << id << " asserting shared clause: " << mk_bounded_pp(local_clause, m, 3) << "\n");
}
}
@ -169,7 +169,7 @@ namespace smt {
}
lbool parallel::worker::check_cube(expr_ref_vector const& cube) {
IF_VERBOSE(0, verbose_stream() << "Worker " << id << " checking cube\n";);
IF_VERBOSE(1, verbose_stream() << "Worker " << id << " checking cube\n";);
for (auto& atom : cube)
asms.push_back(atom);
lbool r = l_undef;
@ -188,7 +188,7 @@ namespace smt {
b.set_exception("unknown exception");
}
asms.shrink(asms.size() - cube.size());
IF_VERBOSE(0, verbose_stream() << "Worker " << id << " DONE checking cube " << r << "\n";);
IF_VERBOSE(1, verbose_stream() << "Worker " << id << " DONE checking cube " << r << "\n";);
return r;
}
@ -434,7 +434,7 @@ namespace smt {
if (top_lits.size() >= k)
break;
}
IF_VERBOSE(0, verbose_stream() << "top literals " << top_lits << " head size " << ctx->m_pq_scores.size() << " num vars " << ctx->get_num_bool_vars() << "\n");
IF_VERBOSE(1, verbose_stream() << "top literals " << top_lits << " head size " << ctx->m_pq_scores.size() << " num vars " << ctx->get_num_bool_vars() << "\n");
return top_lits;
}

6
src/smt/smt_parallel.h
View file

@ -55,7 +55,7 @@ namespace smt {
// called from batch manager to cancel other workers if we've reached a verdict
void cancel_workers() {
IF_VERBOSE(0, verbose_stream() << "Canceling workers\n");
IF_VERBOSE(1, verbose_stream() << "Canceling workers\n");
for (auto& w : p.m_workers)
w->cancel();
}
@ -110,11 +110,11 @@ namespace smt {
void collect_shared_clauses(ast_translation& g2l);
void cancel() {
IF_VERBOSE(0, verbose_stream() << "Worker " << id << " canceling\n");
IF_VERBOSE(1, verbose_stream() << "Worker " << id << " canceling\n");
m.limit().cancel();
}
void collect_statistics(::statistics& st) const {
IF_VERBOSE(0, verbose_stream() << "Collecting statistics for worker " << id << "\n");
IF_VERBOSE(1, verbose_stream() << "Collecting statistics for worker " << id << "\n");
ctx->collect_statistics(st);
}
reslimit& limit() {