From c0b6d00e8aa9a19d2cca474aaad9d0fd37af408e Mon Sep 17 00:00:00 2001 From: Nicolas Braud-Santoni Date: Tue, 22 Aug 2017 18:09:38 +0000 Subject: [PATCH] Update debug output --- src/tactic/core/injectivity_tactic.cpp | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) diff --git a/src/tactic/core/injectivity_tactic.cpp b/src/tactic/core/injectivity_tactic.cpp index d8b5e6acf..75685c891 100644 --- a/src/tactic/core/injectivity_tactic.cpp +++ b/src/tactic/core/injectivity_tactic.cpp @@ -157,7 +157,7 @@ class injectivity_tactic : public tactic { for (unsigned i = 0; i < goal->size(); ++i) { func_decl *f, *g; if (!is_axiom(goal->form(i), f, g)) continue; - TRACE("injectivity_finder", tout << "Marking " << f->get_name() << " as injective" << std::endl;); + TRACE("injectivity", tout << "Marking " << f->get_name() << " as injective" << std::endl;); inj_map.insert(f, g); // TODO: Record that g is f's pseudoinverse } @@ -213,7 +213,7 @@ class injectivity_tactic : public tactic { return BR_FAILED; SASSERT(m().get_sort(a->get_arg(0)) == m().get_sort(b->get_arg(0))); - TRACE("injectivity_eq", tout << "Rewriting (= " << mk_ismt2_pp(args[0], m()) << + TRACE("injectivity", tout << "Rewriting (= " << mk_ismt2_pp(args[0], m()) << " " << mk_ismt2_pp(args[1], m()) << ")" << std::endl;); result = m().mk_eq(a->get_arg(0), b->get_arg(0)); result_pr = nullptr; @@ -276,11 +276,9 @@ public: model_converter_ref & mc, proof_converter_ref & pc, expr_dependency_ref & core) { - std::cerr << "injectivity finder: " << m_finder << std::endl; (*m_finder)(g, result, mc, pc, core); for (unsigned i = 0; i < g->size(); ++i) { - std::cerr << "injectivity rewrite " << i << std::endl; expr* curr = g->form(i); expr_ref rw(m_manager); proof_ref pr(m_manager);