diff options
Diffstat (limited to 'src/expr/expr_manager_template.cpp')
-rw-r--r-- | src/expr/expr_manager_template.cpp | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp index 343f060e9..1eabc9f8a 100644 --- a/src/expr/expr_manager_template.cpp +++ b/src/expr/expr_manager_template.cpp @@ -253,6 +253,16 @@ FunctionType ExprManager::mkPredicateType(const std::vector<Type>& sorts) { return Type(d_nodeManager, new TypeNode(d_nodeManager->mkPredicateType(sortNodes))); } +TupleType ExprManager::mkTupleType(const std::vector<Type>& types) { + Assert( types.size() >= 2 ); + NodeManagerScope nms(d_nodeManager); + std::vector<TypeNode> typeNodes; + for (unsigned i = 0, i_end = types.size(); i < i_end; ++ i) { + typeNodes.push_back(*types[i].d_typeNode); + } + return Type(d_nodeManager, new TypeNode(d_nodeManager->mkTupleType(typeNodes))); +} + BitVectorType ExprManager::mkBitVectorType(unsigned size) const { NodeManagerScope nms(d_nodeManager); return Type(d_nodeManager, new TypeNode(d_nodeManager->mkBitVectorType(size))); |