diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-11-11 13:02:55 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2019-11-11 13:02:55 -0600 |
commit | 9a8710033aeec9de6c0f249b517d98dfc4ffc367 (patch) | |
tree | d8a474f5cbb0aa470b46795ee653cbbf66ecbf64 /src | |
parent | fcaf464a7f6281d882eb7790b5901a3797e861dc (diff) |
Add missing utilities for Node-level Datatype API (#3451)
Diffstat (limited to 'src')
-rw-r--r-- | src/expr/node_manager.cpp | 8 | ||||
-rw-r--r-- | src/expr/node_manager.h | 5 | ||||
-rw-r--r-- | src/expr/type_node.cpp | 6 | ||||
-rw-r--r-- | src/expr/type_node.h | 13 |
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; |