diff options
author | Mathias Preiner <mathias.preiner@gmail.com> | 2019-09-04 11:13:18 -0700 |
---|---|---|
committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-09-04 13:13:18 -0500 |
commit | 599e788f249e478b5817b6cf45584d8e43458df4 (patch) | |
tree | 244bf957d7c7bb6c1b4a09296f075c443e4cdbf3 /src/printer/dagification_visitor.cpp | |
parent | 054ed31cd3ff5a24322c465189879374dee0b1ca (diff) |
Fix DAGification for printer. (#3233)
Diffstat (limited to 'src/printer/dagification_visitor.cpp')
-rw-r--r-- | src/printer/dagification_visitor.cpp | 7 |
1 files changed, 6 insertions, 1 deletions
diff --git a/src/printer/dagification_visitor.cpp b/src/printer/dagification_visitor.cpp index a024c97a7..67c5aa7e5 100644 --- a/src/printer/dagification_visitor.cpp +++ b/src/printer/dagification_visitor.cpp @@ -106,7 +106,12 @@ void DagificationVisitor::visit(TNode current, TNode parent) { TNode& uniqueParent = d_uniqueParent[current]; - if(!uniqueParent.isNull() && uniqueParent != parent) { + // We restrict this optimization to nodes with arity 1 since otherwise we + // may run into issues with tree traverals. Without this restriction + // dumping regress3/pp-regfile increases the file size by a factor of 5000. + if (!uniqueParent.isNull() + && (uniqueParent != parent || parent.getNumChildren() > 1)) + { // there is not a unique parent for this expr, mark it uniqueParent = TNode::null(); } |