diff options
Diffstat (limited to 'src/expr/expr_manager_template.h')
| -rw-r--r-- | src/expr/expr_manager_template.h | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h index 3b5b0e0f4..ab7aeace1 100644 --- a/src/expr/expr_manager_template.h +++ b/src/expr/expr_manager_template.h @@ -211,6 +211,13 @@ public: */ FunctionType mkPredicateType(const std::vector<Type>& sorts); + /** + * Make a tuple type with types from + * <code>types[0..types.size()-1]</code>. <code>types</code> must + * have at least 2 elements. + */ + TupleType mkTupleType(const std::vector<Type>& types); + /** Make a type representing a bit-vector of the given size */ BitVectorType mkBitVectorType(unsigned size) const; |