diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-06-11 15:36:42 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-06-11 15:36:42 +0000 |
commit | 7fd544c108f9fc5a6b4842593597e8fa4a8d11d7 (patch) | |
tree | 85b15c3482d2e834bcbe61dc9f89e6fefc3575af /src/printer | |
parent | aabd0696722250f02e878943f534fd41c49ef5dd (diff) |
fix issue referred to in bug 352 regarding infinite loop between SubstitutionMap (when debugging tag "substitutions" is on) and DagificationVisitor
Diffstat (limited to 'src/printer')
-rw-r--r-- | src/printer/dagification_visitor.cpp | 29 |
1 files changed, 29 insertions, 0 deletions
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); } |