From b61da6fcc041cce5eff4fe40a0bcae5a9f0c10bd Mon Sep 17 00:00:00 2001 From: Arie Gurfinkel Date: Mon, 4 Jun 2018 12:29:18 -0700 Subject: [PATCH] Debug print in org-mode format --- src/muz/spacer/spacer_context.cpp | 13 +++---------- 1 file changed, 3 insertions(+), 10 deletions(-) diff --git a/src/muz/spacer/spacer_context.cpp b/src/muz/spacer/spacer_context.cpp index 511df2383..1268dbede 100644 --- a/src/muz/spacer/spacer_context.cpp +++ b/src/muz/spacer/spacer_context.cpp @@ -911,17 +911,12 @@ void pred_transformer::add_lemma_core(lemma* lemma, bool ground_only) << " " << mk_pp (l, m) << "\n";); STRACE ("spacer.expand-add", - tout << "add-lemma: " << pp_level (lvl) << " " + tout << "** add-lemma: " << pp_level (lvl) << " " << head ()->get_name () << " " << mk_epp (l, m) << "\n"; if (!lemma->is_ground()) { - expr_ref_vector inst(m); - lemma->mk_insts(inst); - for (unsigned i = 0, sz = inst.size(); i < sz; ++i) { - tout << mk_epp(inst.get(i), m) << "\n"; - } - + tout << "Bindings: " << lemma->get_bindings() << "\n"; } tout << "\n"; ); @@ -965,8 +960,6 @@ void pred_transformer::add_lemma_from_child (pred_transformer& child, lemma->mk_insts(inst, l); // -- take ground instance of the current lemma ground_expr(to_quantifier(l)->get_expr(), grnd_lemma, tmp); - STRACE("spacer.expand-add", - tout << "Adding instance: " << mk_epp(grnd_lemma, m) << "\n";); inst.push_back(grnd_lemma); } for (unsigned j=0; j < inst.size(); j++) { @@ -3239,7 +3232,7 @@ lbool context::expand_pob(pob& n, pob_ref_buffer &out) << mk_pp(n.post(), m) << "\n";); STRACE ("spacer.expand-add", - tout << "expand-pob: " << n.pt().head()->get_name() + tout << "** expand-pob: " << n.pt().head()->get_name() << " level: " << n.level() << " depth: " << (n.depth () - m_pob_queue.min_depth ()) << "\n" << mk_epp(n.post(), m) << "\n\n";);