mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
change verbosity level
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
c14c778735
commit
af5d989d6c
|
@ -65,7 +65,7 @@ namespace opt {
|
|||
for (unsigned i = 0; i < ans.size(); ++i) {
|
||||
tout << mk_pp(ans[i].get(), m) << "\n";
|
||||
});
|
||||
IF_VERBOSE(0, verbose_stream() << "(maxsat.core sat with lower bound: " << ans.size() << "\n";);
|
||||
IF_VERBOSE(1, verbose_stream() << "(maxsat.core sat with lower bound: " << ans.size() << "\n";);
|
||||
if (ans.size() > m_answer.size()) {
|
||||
m_answer.reset();
|
||||
m_answer.append(ans);
|
||||
|
@ -92,7 +92,7 @@ namespace opt {
|
|||
core_vars.insert(get_not(core[i]));
|
||||
block_vars.remove(core[i]);
|
||||
}
|
||||
IF_VERBOSE(0, verbose_stream() << "(maxsat.core unsat (core size = " << core.size() << ")\n";);
|
||||
IF_VERBOSE(1, verbose_stream() << "(maxsat.core unsat (core size = " << core.size() << ")\n";);
|
||||
if (core.empty()) {
|
||||
m_upper = m_answer.size();
|
||||
return l_true;
|
||||
|
|
|
@ -149,7 +149,7 @@ namespace opt {
|
|||
}
|
||||
|
||||
lbool step() {
|
||||
IF_VERBOSE(0, verbose_stream() << "(opt.max_sat step " << m_soft.size() + 2 - m_upper_size << ")\n";);
|
||||
IF_VERBOSE(1, verbose_stream() << "(opt.max_sat step " << m_soft.size() + 2 - m_upper_size << ")\n";);
|
||||
expr_ref_vector assumptions(m), block_vars(m);
|
||||
for (unsigned i = 0; i < m_soft.size(); ++i) {
|
||||
assumptions.push_back(m.mk_not(m_aux[i].get()));
|
||||
|
@ -187,7 +187,7 @@ namespace opt {
|
|||
// ++i;
|
||||
//}
|
||||
|
||||
IF_VERBOSE(0, verbose_stream() << "(opt.max_sat unsat-core of size " << core.size() << ")\n";);
|
||||
IF_VERBOSE(1, verbose_stream() << "(opt.max_sat unsat-core of size " << core.size() << ")\n";);
|
||||
}
|
||||
else {
|
||||
s().get_unsat_core(core);
|
||||
|
@ -214,7 +214,7 @@ namespace opt {
|
|||
}
|
||||
SASSERT (!block_vars.empty());
|
||||
assert_at_most_one(block_vars);
|
||||
IF_VERBOSE(0, verbose_stream() << "(opt.max_sat # of non-blocked soft constraints: " << m_soft.size() - block_vars.size() << ")\n";);
|
||||
IF_VERBOSE(1, verbose_stream() << "(opt.max_sat # of non-blocked soft constraints: " << m_soft.size() - block_vars.size() << ")\n";);
|
||||
return l_false;
|
||||
}
|
||||
|
||||
|
@ -264,7 +264,7 @@ namespace opt {
|
|||
m_s->assert_expr(current_solver.get_assertion(i));
|
||||
}
|
||||
m_use_new_bv_solver = true;
|
||||
IF_VERBOSE(0, verbose_stream() << "Force to use the new BV solver." << std::endl;);
|
||||
IF_VERBOSE(1, verbose_stream() << "Force to use the new BV solver." << std::endl;);
|
||||
}
|
||||
}
|
||||
|
||||
|
|
|
@ -61,7 +61,6 @@ namespace opt {
|
|||
});
|
||||
|
||||
DEBUG_CODE(if (is_sat == l_true) {
|
||||
IF_VERBOSE(0, verbose_stream() << "validating assignment\n";);
|
||||
m_s->push();
|
||||
commit_assignment();
|
||||
VERIFY(l_true == m_s->check_sat(0,0));
|
||||
|
|
|
@ -1046,14 +1046,10 @@ namespace smt {
|
|||
|
||||
resolve_conflict(c);
|
||||
|
||||
#if 1
|
||||
justification* js = 0;
|
||||
ctx.mk_clause(lits.size(), lits.c_ptr(), js, CLS_AUX_LEMMA, 0);
|
||||
IF_VERBOSE(2, ctx.display_literals_verbose(verbose_stream(),
|
||||
lits.size(), lits.c_ptr());
|
||||
IF_VERBOSE(2, ctx.display_literals_verbose(verbose_stream(), lits.size(), lits.c_ptr());
|
||||
verbose_stream() << "\n";);
|
||||
// ctx.mk_th_axiom(get_id(), lits.size(), lits.c_ptr());
|
||||
#endif
|
||||
}
|
||||
|
||||
void theory_pb::set_mark(bool_var v, unsigned idx) {
|
||||
|
|
Loading…
Reference in a new issue