From babbe0e30d769b5f68cb3f36820fbb5e176de7c5 Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Thu, 6 Feb 2020 17:30:53 -0600
Subject: Generalize containsQuantifiers to hasClosure (#3722)

---
 src/expr/node_algorithm.cpp | 37 +++++++++++++++++++++++++++++++++++++
 src/expr/node_algorithm.h   |  9 +++++++++
 2 files changed, 46 insertions(+)

(limited to 'src/expr')

diff --git a/src/expr/node_algorithm.cpp b/src/expr/node_algorithm.cpp
index 9721845f7..9619e69d1 100644
--- a/src/expr/node_algorithm.cpp
+++ b/src/expr/node_algorithm.cpp
@@ -229,6 +229,43 @@ bool hasFreeVar(TNode n)
   return getFreeVariables(n, fvs, false);
 }
 
+struct HasClosureTag
+{
+};
+struct HasClosureComputedTag
+{
+};
+/** Attribute true for expressions with closures in them */
+typedef expr::Attribute<HasClosureTag, bool> HasClosureAttr;
+typedef expr::Attribute<HasClosureComputedTag, bool> HasClosureComputedAttr;
+
+bool hasClosure(Node n)
+{
+  if (!n.getAttribute(HasClosureComputedAttr()))
+  {
+    bool hasC = false;
+    if (n.isClosure())
+    {
+      hasC = true;
+    }
+    else
+    {
+      for (auto i = n.begin(); i != n.end() && !hasC; ++i)
+      {
+        hasC = hasClosure(*i);
+      }
+    }
+    if (!hasC && n.hasOperator())
+    {
+      hasC = hasClosure(n.getOperator());
+    }
+    n.setAttribute(HasClosureAttr(), hasC);
+    n.setAttribute(HasClosureComputedAttr(), true);
+    return hasC;
+  }
+  return n.getAttribute(HasClosureAttr());
+}
+
 bool getFreeVariables(TNode n,
                       std::unordered_set<Node, NodeHashFunction>& fvs,
                       bool computeFv)
diff --git a/src/expr/node_algorithm.h b/src/expr/node_algorithm.h
index 03d77a2f9..929e1c5ef 100644
--- a/src/expr/node_algorithm.h
+++ b/src/expr/node_algorithm.h
@@ -69,6 +69,15 @@ bool hasBoundVar(TNode n);
  */
 bool hasFreeVar(TNode n);
 
+/**
+ * Returns true iff the node n contains a closure, that is, a node
+ * whose kind is FORALL, EXISTS, CHOICE, LAMBDA, or any other closure currently
+ * supported.
+ * @param n The node under investigation
+ * @return true iff this node contains a closure.
+ */
+bool hasClosure(Node n);
+
 /**
  * Get the free variables in n, that is, the subterms of n of kind
  * BOUND_VARIABLE that are not bound in n, adds these to fvs.
-- 
cgit v1.2.3