From d34e563fe48c42aa06eea44191a21dcf29772339 Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Tue, 14 Sep 2021 15:43:47 -0500
Subject: Utilities in preparation for print benchmark utility (#7190)

This adds a few utilities in preparation for the print benchmark utility, which will replace our own dumping infrastructure.
---
 src/expr/dtype.cpp | 13 +++++++++++++
 src/expr/dtype.h   |  6 ++++++
 2 files changed, 19 insertions(+)

(limited to 'src/expr')

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;
 
-- 
cgit v1.2.3