Merge branch 'master' into fixParseOnlyfixParseOnly

2 files changed, 19 insertions, 0 deletions

diff --git a/src/expr/dtype.cpp b/src/expr/dtype.cpp
index 31a22b44a..fdb397d39 100644
--- a/src/expr/dtype.cpp
+++ b/src/expr/dtype.cpp
@@ -895,6 +895,19 @@ const std::vector<std::shared_ptr<DTypeConstructor> >& DType::getConstructors()
   return d_constructors;
 }
 
+std::unordered_set<TypeNode> DType::getSubfieldTypes() const
+{
+  std::unordered_set<TypeNode> subFieldTypes;
+  for (std::shared_ptr<DTypeConstructor> ctor : d_constructors)
+  {
+    for (size_t i = 0, nargs = ctor->getNumArgs(); i < nargs; i++)
+    {
+      subFieldTypes.insert(ctor->getArgType(i));
+    }
+  }
+  return subFieldTypes;
+}
+
 std::ostream& operator<<(std::ostream& os, const DType& dt)
 {
   // can only output datatypes in the cvc5 native language
diff --git a/src/expr/dtype.h b/src/expr/dtype.h
index a608b9adb..4f54f0af7 100644
--- a/src/expr/dtype.h
+++ b/src/expr/dtype.h
@@ -425,6 +425,12 @@ class DType
   const std::vector<std::shared_ptr<DTypeConstructor> >& getConstructors()
       const;
 
+  /**
+   * Return the subfield types of this datatype. This is the set of all types T
+   * for which there exists an argument to a constructor of type T.
+   */
+  std::unordered_set<TypeNode> getSubfieldTypes() const;
+
   /** prints this datatype to stream */
   void toStream(std::ostream& out) const;