Utility function for getting component types (#3703)

1 files changed, 10 insertions, 0 deletions

diff --git a/src/expr/node_algorithm.h b/src/expr/node_algorithm.h
index e5a21d565..03d77a2f9 100644
--- a/src/expr/node_algorithm.h
+++ b/src/expr/node_algorithm.h
@@ -151,6 +151,16 @@ Node substituteCaptureAvoiding(TNode n,
                                std::vector<Node>& src,
                                std::vector<Node>& dest);
 
+/**
+ * Get component types in type t. This adds all types that are subterms of t
+ * when viewed as a term. For example, if t is (Array T1 T2), then
+ * (Array T1 T2), T1 and T2 are component types of t.
+ * @param t The type node under investigation
+ * @param types The set which component types are added to.
+ */
+void getComponentTypes(
+    TypeNode t, std::unordered_set<TypeNode, TypeNodeHashFunction>& types);
+
 }  // namespace expr
 }  // namespace CVC4