mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-31 19:52:29 +00:00
Code Activity

adjusting verbose msgs

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2012-12-04 11:17:24 -08:00
parent 8191cc1951
commit ff999773b2
2 changed files with 8 additions and 10 deletions
Download patch file Download diff file Expand all files Collapse all files

15
src/smt/smt_model_checker.cpp
View file

@ -312,7 +312,7 @@ namespace smt {
TRACE("model_checker", tout << "MODEL_CHECKER INVOKED\n"; TRACE("model_checker", tout << "MODEL_CHECKER INVOKED\n";
tout << "model:\n"; model_pp(tout, *m_curr_model);); tout << "model:\n"; model_pp(tout, *m_curr_model););
if (m_params.m_mbqi_trace) { if (m_params.m_mbqi_trace) {
verbose_stream() << "[mbqi] started\n"; verbose_stream() << "(smt.mbqi \"started\")\n";
} }
init_aux_context(); init_aux_context();
@ -324,13 +324,12 @@ namespace smt {
quantifier * q = *it; quantifier * q = *it;
if (m_context->is_relevant(q) && m_context->get_assignment(q) == l_true) { if (m_context->is_relevant(q) && m_context->get_assignment(q) == l_true) {
if (m_params.m_mbqi_trace && q->get_qid() != symbol::null) { if (m_params.m_mbqi_trace && q->get_qid() != symbol::null) {
verbose_stream() << "[mbqi] checking: " << q->get_qid() << "\n"; verbose_stream() << "(smt.mbqi :checking " << q->get_qid() << ")\n";
} }
found_relevant = true; found_relevant = true;
if (!check(q)) { if (!check(q)) {
IF_VERBOSE(5, verbose_stream() << "current model does not satisfy: " << q->get_qid() << "\n";); if (m_params.m_mbqi_trace || get_verbosity_level() >= 5) {
if (m_params.m_mbqi_trace) { verbose_stream() << "(smt.mbqi :failed " << q->get_qid() << ")\n";
verbose_stream() << "[mbqi] failed " << q->get_qid() << "\n";
} }
num_failures++; num_failures++;
} }
@ -347,9 +346,9 @@ namespace smt {
m_curr_model->cleanup(); m_curr_model->cleanup();
if (m_params.m_mbqi_trace) { if (m_params.m_mbqi_trace) {
if (num_failures == 0) if (num_failures == 0)
verbose_stream() << "[mbqi] succeeded\n"; verbose_stream() << "(smt.mbqi :succeeded true)\n";
else else
verbose_stream() << "[mbqi] num failures " << num_failures << "\n"; verbose_stream() << "(smt.mbqi :num-failures " << num_failures << ")\n";
} }
return num_failures == 0; return num_failures == 0;
} }
@ -360,7 +359,7 @@ namespace smt {
} }
void model_checker::restart_eh() { void model_checker::restart_eh() {
IF_VERBOSE(100, verbose_stream() << "instantiating new instances...\n";); IF_VERBOSE(100, verbose_stream() << "(smt.mbqi \"instantiating new instances...\")\n";);
assert_new_instances(); assert_new_instances();
reset_new_instances(); reset_new_instances();
} }

3
src/smt/smt_quantifier.cpp
View file

@ -562,7 +562,7 @@ namespace smt {
virtual quantifier_manager::check_model_result virtual quantifier_manager::check_model_result
check_model(proto_model * m, obj_map<enode, app *> const & root2value) { check_model(proto_model * m, obj_map<enode, app *> const & root2value) {
if (m_fparams->m_mbqi) { if (m_fparams->m_mbqi) {
IF_VERBOSE(10, verbose_stream() << "model based quantifier instantiation...\n";); IF_VERBOSE(10, verbose_stream() << "(smt.mbqi)\n";);
if (m_model_checker->check(m, root2value)) { if (m_model_checker->check(m, root2value)) {
return quantifier_manager::SAT; return quantifier_manager::SAT;
} }
@ -594,7 +594,6 @@ namespace smt {
final_check_status final_check_quant() { final_check_status final_check_quant() {
if (use_ematching()) { if (use_ematching()) {
if (m_lazy_matching_idx < m_fparams->m_qi_max_lazy_multipattern_matching) { if (m_lazy_matching_idx < m_fparams->m_qi_max_lazy_multipattern_matching) {
IF_VERBOSE(100, verbose_stream() << "matching delayed multi-patterns... \n";);
m_lazy_mam->rematch(); m_lazy_mam->rematch();
m_context->push_trail(value_trail<context, unsigned>(m_lazy_matching_idx)); m_context->push_trail(value_trail<context, unsigned>(m_lazy_matching_idx));
m_lazy_matching_idx++; m_lazy_matching_idx++;