diff options
Diffstat (limited to 'src/printer/dagification_visitor.cpp')
| -rw-r--r-- | src/printer/dagification_visitor.cpp | 23 |
1 files changed, 14 insertions, 9 deletions
diff --git a/src/printer/dagification_visitor.cpp b/src/printer/dagification_visitor.cpp index 7c0cc3101..202249759 100644 --- a/src/printer/dagification_visitor.cpp +++ b/src/printer/dagification_visitor.cpp @@ -46,20 +46,25 @@ DagificationVisitor::~DagificationVisitor() { } bool DagificationVisitor::alreadyVisited(TNode current, TNode parent) { + Kind ck = current.getKind(); + if (ck == kind::FORALL || ck == kind::EXISTS || ck == kind::LAMBDA + || ck == kind::CHOICE) + { + // for quantifiers, we visit them but we don't recurse on them + visit(current, parent); + return true; + } // don't visit variables, constants, or those exprs that we've // already seen more than the threshold: if we've increased // the count beyond the threshold already, we've done the same // for all subexpressions, so it isn't useful to traverse and // increment again (they'll be dagified anyway). - return current.isVar() || - current.getMetaKind() == kind::metakind::CONSTANT || - current.getNumChildren()==0 || - ( ( current.getKind() == kind::NOT || - current.getKind() == kind::UMINUS ) && - ( current[0].isVar() || - current[0].getMetaKind() == kind::metakind::CONSTANT ) ) || - current.getKind() == kind::SORT_TYPE || - d_nodeCount[current] > d_threshold; + return current.isVar() || current.getMetaKind() == kind::metakind::CONSTANT + || current.getNumChildren() == 0 + || ((ck == kind::NOT || ck == kind::UMINUS) + && (current[0].isVar() + || current[0].getMetaKind() == kind::metakind::CONSTANT)) + || ck == kind::SORT_TYPE || d_nodeCount[current] > d_threshold; } void DagificationVisitor::visit(TNode current, TNode parent) { |