diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-02-06 17:30:53 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-02-06 17:30:53 -0600 |
| commit | babbe0e30d769b5f68cb3f36820fbb5e176de7c5 (patch) | |
| tree | 3b0195271c8fdf233836ccd726e4f2c6cd03865c /src/expr/node_algorithm.h | |
| parent | ea4355639142f10a2bc5c1aa6044d9bbc246435b (diff) | |
Generalize containsQuantifiers to hasClosure (#3722)
Diffstat (limited to 'src/expr/node_algorithm.h')
| -rw-r--r-- | src/expr/node_algorithm.h | 9 |
1 files changed, 9 insertions, 0 deletions
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 @@ -70,6 +70,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. * @param n The node under investigation |