1 files changed, 19 insertions, 0 deletions
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index dcfb14b7a..baa8de5aa 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -523,6 +523,16 @@ public:
    */
   inline TypeNode mkPredicateType(const std::vector<TypeNode>& sorts);
 
+  /**
+   * Make a tuple type with types from
+   * <code>types</code>. <code>types</code> must have at least two
+   * elements.
+   *
+   * @param types a vector of types
+   * @returns the tuple type (types[0], ..., types[n])
+   */
+  inline TypeNode mkTupleType(const std::vector<TypeNode>& types);
+
   /** Make the type of bitvectors of size <code>size</code> */
   inline TypeNode mkBitVectorType(unsigned size);
 
@@ -714,6 +724,15 @@ NodeManager::mkPredicateType(const std::vector<TypeNode>& sorts) {
   return mkTypeNode(kind::FUNCTION_TYPE, sortNodes);
 }
 
+inline TypeNode NodeManager::mkTupleType(const std::vector<TypeNode>& types) {
+  Assert(types.size() >= 2);
+  std::vector<TypeNode> typeNodes;
+  for (unsigned i = 0; i < types.size(); ++ i) {
+    typeNodes.push_back(types[i]);
+  }
+  return mkTypeNode(kind::TUPLE_TYPE, typeNodes);
+}
+
 inline TypeNode NodeManager::mkBitVectorType(unsigned size) {
   return TypeNode(mkTypeConst<BitVectorSize>(BitVectorSize(size)));
 }