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 | |
parent | ea4355639142f10a2bc5c1aa6044d9bbc246435b (diff) |
Generalize containsQuantifiers to hasClosure (#3722)
Diffstat (limited to 'src/expr')
-rw-r--r-- | src/expr/node_algorithm.cpp | 37 | ||||
-rw-r--r-- | src/expr/node_algorithm.h | 9 |
2 files changed, 46 insertions, 0 deletions
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 @@ -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 |