From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Tue, 26 Jun 2018 19:52:34 +0000 (-0500)
Subject:  Do not dagify printing over binders (#2093)
X-Git-Tag: cvc5-1.0.0~4946
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=19442febecd2a14fe9a62a22d6fb174e013ee50e;p=cvc5.git

 Do not dagify printing over binders (#2093)
---

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) {