Do not dagify printing over binders (#2093)

diff --git a/src/printer/dagification_visitor.cpp b/src/printer/dagification_visitor.cpp
index 7c0cc31012e0f5d15df0db4aacee75663158f997..2022497593e7f0310ed1fa734fa47a4d18b72bc4 100644 (file)
--- 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) {