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.h | 9 +++++++++
 1 file changed, 9 insertions(+)

(limited to 'src/expr/node_algorithm.h')

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