Utility function for getting component types (#3703)

diff --git a/src/expr/node_algorithm.cpp b/src/expr/node_algorithm.cpp
index eda4dadd27c05504023cc798d3abca18a828028c..9721845f7f99f53d20b0dcf578ac45629c692842 100644 (file)
--- a/src/expr/node_algorithm.cpp
+++ b/src/expr/node_algorithm.cpp
@@ -18,6 +18,7 @@
 #include "expr/node_algorithm.h"
 
 #include "expr/attribute.h"
+#include "expr/dtype.h"
 
 namespace CVC4 {
 namespace expr {
@@ -522,5 +523,27 @@ Node substituteCaptureAvoiding(TNode n,
   return visited[n];
 }
 
+void getComponentTypes(
+    TypeNode t, std::unordered_set<TypeNode, TypeNodeHashFunction>& types)
+{
+  std::vector<TypeNode> toProcess;
+  toProcess.push_back(t);
+  do
+  {
+    TypeNode curr = toProcess.back();
+    toProcess.pop_back();
+    // if not already visited
+    if (types.find(t) == types.end())
+    {
+      types.insert(t);
+      // get component types from the children
+      for (unsigned i = 0, nchild = t.getNumChildren(); i < nchild; i++)
+      {
+        toProcess.push_back(t[i]);
+      }
+    }
+  } while (!toProcess.empty());
+}
+
 }  // namespace expr
 }  // namespace CVC4

diff --git a/src/expr/node_algorithm.h b/src/expr/node_algorithm.h
index e5a21d5652f25bf687f5418238b4e368e19b3b43..03d77a2f9557facf5f00b46049ee7c2c4bdf6be0 100644 (file)
--- 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