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)));