From 7fd544c108f9fc5a6b4842593597e8fa4a8d11d7 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Mon, 11 Jun 2012 15:36:42 +0000 Subject: [PATCH] fix issue referred to in bug 352 regarding infinite loop between SubstitutionMap (when debugging tag "substitutions" is on) and DagificationVisitor --- src/printer/dagification_visitor.cpp | 29 ++++++++++++++++++++++++++++ 1 file changed, 29 insertions(+) diff --git a/src/printer/dagification_visitor.cpp b/src/printer/dagification_visitor.cpp index da651cd54..81183182d 100644 --- a/src/printer/dagification_visitor.cpp +++ b/src/printer/dagification_visitor.cpp @@ -64,6 +64,16 @@ bool DagificationVisitor::alreadyVisited(TNode current, TNode parent) { } void DagificationVisitor::visit(TNode current, TNode parent) { + +#ifdef CVC4_TRACING +# ifdef CVC4_DEBUG + // turn off dagification for Debug stream while we're doing this work + Node::dag::Scope scopeDebug(Debug.getStream(), false); +# endif /* CVC4_DEBUG */ + // turn off dagification for Trace stream while we're doing this work + Node::dag::Scope scopeTrace(Trace.getStream(), false); +#endif /* CVC4_TRACING */ + if(d_uniqueParent.find(current) != d_uniqueParent.end()) { // we've seen this expr before @@ -99,6 +109,15 @@ void DagificationVisitor::done(TNode node) { d_done = true; +#ifdef CVC4_TRACING +# ifdef CVC4_DEBUG + // turn off dagification for Debug stream while we're doing this work + Node::dag::Scope scopeDebug(Debug.getStream(), false); +# endif /* CVC4_DEBUG */ + // turn off dagification for Trace stream while we're doing this work + Node::dag::Scope scopeTrace(Trace.getStream(), false); +#endif /* CVC4_TRACING */ + // letify subexprs before parents (cascading LETs) std::sort(d_substNodes.begin(), d_substNodes.end()); @@ -132,6 +151,16 @@ const theory::SubstitutionMap& DagificationVisitor::getLets() { Node DagificationVisitor::getDagifiedBody() { AlwaysAssert(d_done, "DagificationVisitor must be used as a visitor before getting the dagified version out!"); + +#ifdef CVC4_TRACING +# ifdef CVC4_DEBUG + // turn off dagification for Debug stream while we're doing this work + Node::dag::Scope scopeDebug(Debug.getStream(), false); +# endif /* CVC4_DEBUG */ + // turn off dagification for Trace stream while we're doing this work + Node::dag::Scope scopeTrace(Trace.getStream(), false); +#endif /* CVC4_TRACING */ + return d_substitutions->apply(d_top); } -- 2.30.2