diff options
Diffstat (limited to 'src/expr/expr_manager_template.cpp')
-rw-r--r-- | src/expr/expr_manager_template.cpp | 28 |
1 files changed, 14 insertions, 14 deletions
diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp index eadbb73a2..9b8511de9 100644 --- a/src/expr/expr_manager_template.cpp +++ b/src/expr/expr_manager_template.cpp @@ -115,22 +115,22 @@ ExprManager::~ExprManager() { BooleanType ExprManager::booleanType() const { NodeManagerScope nms(d_nodeManager); - return Type(d_nodeManager, new TypeNode(d_nodeManager->booleanType())); + return BooleanType(Type(d_nodeManager, new TypeNode(d_nodeManager->booleanType()))); } KindType ExprManager::kindType() const { NodeManagerScope nms(d_nodeManager); - return Type(d_nodeManager, new TypeNode(d_nodeManager->kindType())); + return KindType(Type(d_nodeManager, new TypeNode(d_nodeManager->kindType()))); } RealType ExprManager::realType() const { NodeManagerScope nms(d_nodeManager); - return Type(d_nodeManager, new TypeNode(d_nodeManager->realType())); + return RealType(Type(d_nodeManager, new TypeNode(d_nodeManager->realType()))); } IntegerType ExprManager::integerType() const { NodeManagerScope nms(d_nodeManager); - return Type(d_nodeManager, new TypeNode(d_nodeManager->integerType())); + return IntegerType(Type(d_nodeManager, new TypeNode(d_nodeManager->integerType()))); } Expr ExprManager::mkExpr(Kind kind, const Expr& child1) { @@ -285,7 +285,7 @@ Expr ExprManager::mkExpr(Expr opExpr, const std::vector<Expr>& children) { /** Make a function type from domain to range. */ FunctionType ExprManager::mkFunctionType(const Type& domain, const Type& range) { NodeManagerScope nms(d_nodeManager); - return Type(d_nodeManager, new TypeNode(d_nodeManager->mkFunctionType(*domain.d_typeNode, *range.d_typeNode))); + return FunctionType(Type(d_nodeManager, new TypeNode(d_nodeManager->mkFunctionType(*domain.d_typeNode, *range.d_typeNode)))); } /** Make a function type with input types from argTypes. */ @@ -296,7 +296,7 @@ FunctionType ExprManager::mkFunctionType(const std::vector<Type>& argTypes, cons for (unsigned i = 0, i_end = argTypes.size(); i < i_end; ++ i) { argTypeNodes.push_back(*argTypes[i].d_typeNode); } - return Type(d_nodeManager, new TypeNode(d_nodeManager->mkFunctionType(argTypeNodes, *range.d_typeNode))); + return FunctionType(Type(d_nodeManager, new TypeNode(d_nodeManager->mkFunctionType(argTypeNodes, *range.d_typeNode)))); } FunctionType ExprManager::mkFunctionType(const std::vector<Type>& sorts) { @@ -306,7 +306,7 @@ FunctionType ExprManager::mkFunctionType(const std::vector<Type>& sorts) { for (unsigned i = 0, i_end = sorts.size(); i < i_end; ++ i) { sortNodes.push_back(*sorts[i].d_typeNode); } - return Type(d_nodeManager, new TypeNode(d_nodeManager->mkFunctionType(sortNodes))); + return FunctionType(Type(d_nodeManager, new TypeNode(d_nodeManager->mkFunctionType(sortNodes)))); } FunctionType ExprManager::mkPredicateType(const std::vector<Type>& sorts) { @@ -316,7 +316,7 @@ FunctionType ExprManager::mkPredicateType(const std::vector<Type>& sorts) { for (unsigned i = 0, i_end = sorts.size(); i < i_end; ++ i) { sortNodes.push_back(*sorts[i].d_typeNode); } - return Type(d_nodeManager, new TypeNode(d_nodeManager->mkPredicateType(sortNodes))); + return FunctionType(Type(d_nodeManager, new TypeNode(d_nodeManager->mkPredicateType(sortNodes)))); } TupleType ExprManager::mkTupleType(const std::vector<Type>& types) { @@ -326,29 +326,29 @@ TupleType ExprManager::mkTupleType(const std::vector<Type>& types) { 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))); + return TupleType(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))); + return BitVectorType(Type(d_nodeManager, new TypeNode(d_nodeManager->mkBitVectorType(size)))); } ArrayType ExprManager::mkArrayType(Type indexType, Type constituentType) const { NodeManagerScope nms(d_nodeManager); - return Type(d_nodeManager, new TypeNode(d_nodeManager->mkArrayType(*indexType.d_typeNode, *constituentType.d_typeNode))); + return ArrayType(Type(d_nodeManager, new TypeNode(d_nodeManager->mkArrayType(*indexType.d_typeNode, *constituentType.d_typeNode)))); } SortType ExprManager::mkSort(const std::string& name) const { NodeManagerScope nms(d_nodeManager); - return Type(d_nodeManager, new TypeNode(d_nodeManager->mkSort(name))); + return SortType(Type(d_nodeManager, new TypeNode(d_nodeManager->mkSort(name)))); } SortConstructorType ExprManager::mkSortConstructor(const std::string& name, size_t arity) const { NodeManagerScope nms(d_nodeManager); - return Type(d_nodeManager, - new TypeNode(d_nodeManager->mkSortConstructor(name, arity))); + return SortConstructorType(Type(d_nodeManager, + new TypeNode(d_nodeManager->mkSortConstructor(name, arity)))); } /** |