diff options
Diffstat (limited to 'src/expr/node_manager.h')
| -rw-r--r-- | src/expr/node_manager.h | 24 |
1 files changed, 2 insertions, 22 deletions
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index 1ae9f1e8e..45c9afbde 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -756,7 +756,7 @@ public: * @param types a vector of types * @returns the tuple type (types[0], ..., types[n]) */ - inline TypeNode mkTupleType(const std::vector<TypeNode>& types); + TypeNode mkTupleType(const std::vector<TypeNode>& types); /** * Make a record type with the description from rec. @@ -764,7 +764,7 @@ public: * @param rec a description of the record * @returns the record type */ - inline TypeNode mkRecordType(const Record& rec); + TypeNode mkRecordType(const Record& rec); /** * Make a symbolic expression type with types from @@ -839,12 +839,6 @@ public: throw(TypeCheckingExceptionPrivate); /** - * Given a tuple or record type, get the internal datatype used for - * it. Makes the DatatypeType if necessary. - */ - TypeNode getDatatypeForTupleRecord(TypeNode tupleRecordType); - - /** * Get the type for the given node and optionally do type checking. * * Initial type computation will be near-constant time if @@ -1063,20 +1057,6 @@ NodeManager::mkPredicateType(const std::vector<TypeNode>& sorts) { return mkTypeNode(kind::FUNCTION_TYPE, sortNodes); } -inline TypeNode NodeManager::mkTupleType(const std::vector<TypeNode>& types) { - std::vector<TypeNode> typeNodes; - for (unsigned i = 0; i < types.size(); ++ i) { - CheckArgument(!types[i].isFunctionLike(), types, - "cannot put function-like types in tuples"); - typeNodes.push_back(types[i]); - } - return mkTypeNode(kind::TUPLE_TYPE, typeNodes); -} - -inline TypeNode NodeManager::mkRecordType(const Record& rec) { - return mkTypeConst(rec); -} - inline TypeNode NodeManager::mkSExprType(const std::vector<TypeNode>& types) { std::vector<TypeNode> typeNodes; for (unsigned i = 0; i < types.size(); ++ i) { |