diff options
Diffstat (limited to 'src/expr/expr_manager_template.cpp')
| -rw-r--r-- | src/expr/expr_manager_template.cpp | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp index d499b8bb7..d69dc73f9 100644 --- a/src/expr/expr_manager_template.cpp +++ b/src/expr/expr_manager_template.cpp @@ -661,6 +661,14 @@ SetType ExprManager::mkSetType(Type elementType) const { return SetType(Type(d_nodeManager, new TypeNode(d_nodeManager->mkSetType(*elementType.d_typeNode)))); } +SequenceType ExprManager::mkSequenceType(Type elementType) const +{ + NodeManagerScope nms(d_nodeManager); + return SequenceType(Type( + d_nodeManager, + new TypeNode(d_nodeManager->mkSequenceType(*elementType.d_typeNode)))); +} + DatatypeType ExprManager::mkDatatypeType(Datatype& datatype, uint32_t flags) { // Not worth a special implementation; this doesn't need to be fast |