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

diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index d66225961bfa7bb602f84616a7b7e06d5b1f90ec..5223fd02c06e7297324a1aa144a58a400e637acb 100644 (file)
--- 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 a3fd50d8cc6f22f85617588cc613e160b29b079b..8daaa04e6d6d2407c9421bb7407f9804ed620747 100644 (file)
--- 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 c827b77fa449b7943c45aebbf5266d257c787088..0bf86240b42571c90b1b6bb319ec4a62b1e6cdf9 100644 (file)
--- 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 d2197faf89eef669fcca4c4d8e09821d1f0ed908..472d29f5f6485b3709d4ff4f5d824cb023b8ec58 100644 (file)
--- 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;