Add missing utilities for Node-level Datatype API (#3451)

4 files changed, 31 insertions, 1 deletions

diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index d66225961..5223fd02c 100644
--- a/src/expr/node_manager.cpp
+++ b/src/expr/node_manager.cpp
@@ -515,6 +515,14 @@ TypeNode NodeManager::mkConstructorType(const DatatypeConstructor& constructor,
   return mkTypeNode(kind::CONSTRUCTOR_TYPE, sorts);
 }
 
+TypeNode NodeManager::mkConstructorType(const std::vector<TypeNode>& args,
+                                        TypeNode range)
+{
+  std::vector<TypeNode> sorts = args;
+  sorts.push_back(range);
+  return mkTypeNode(kind::CONSTRUCTOR_TYPE, sorts);
+}
+
 TypeNode NodeManager::TupleTypeCache::getTupleType( NodeManager * nm, std::vector< TypeNode >& types, unsigned index ) {
   if( index==types.size() ){
     if( d_data.isNull() ){
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index a3fd50d8c..8daaa04e6 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -869,6 +869,11 @@ public:
 
   /** Make a type representing a constructor with the given parameterization */
   TypeNode mkConstructorType(const DatatypeConstructor& constructor, TypeNode range);
+  /**
+   * Make a type representing a constructor with the given argument (subfield)
+   * types and return type range.
+   */
+  TypeNode mkConstructorType(const std::vector<TypeNode>& args, TypeNode range);
 
   /** Make a type representing a selector with the given parameterization */
   inline TypeNode mkSelectorType(TypeNode domain, TypeNode range);
diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp
index c827b77fa..0bf86240b 100644
--- a/src/expr/type_node.cpp
+++ b/src/expr/type_node.cpp
@@ -450,6 +450,12 @@ TypeNode TypeNode::instantiateParametricDatatype(
   return nm->mkTypeNode(kind::PARAMETRIC_DATATYPE, paramsNodes);
 }
 
+TypeNode TypeNode::instantiateSortConstructor(
+    const std::vector<TypeNode>& params) const
+{
+  return NodeManager::currentNM()->mkSort(*this, params);
+}
+
 /** Is this an instantiated datatype parameter */
 bool TypeNode::isParameterInstantiatedDatatype(unsigned n) const {
   AssertArgument(getKind() == kind::PARAMETRIC_DATATYPE, *this);
diff --git a/src/expr/type_node.h b/src/expr/type_node.h
index d2197faf8..472d29f5f 100644
--- a/src/expr/type_node.h
+++ b/src/expr/type_node.h
@@ -638,7 +638,7 @@ public:
 
   /**
    * Get instantiated datatype type. The type on which this method is called
-   * should be a parametric datatype whose parameter list is the same list as
+   * should be a parametric datatype whose parameter list is the same size as
    * argument params. This constructs the instantiated version of this
    * parametric datatype, e.g. passing (par (A) (List A)), { Int } ) to this
    * method returns (List Int).
@@ -676,6 +676,17 @@ public:
   /** Is this a sort constructor kind */
   bool isSortConstructor() const;
 
+  /**
+   * Instantiate a sort constructor type. The type on which this method is
+   * called should be a sort constructor type whose parameter list is the
+   * same size as argument params. This constructs the instantiated version of
+   * this sort constructor. For example, this is a sort constructor, e.g.
+   * declared via (declare-sort U 2), then calling this method with
+   * { Int, Int } will generate the instantiated sort (U Int Int).
+   */
+  TypeNode instantiateSortConstructor(
+      const std::vector<TypeNode>& params) const;
+
   /** Get the most general base type of the type */
   TypeNode getBaseType() const;