diff options
Diffstat (limited to 'src/expr/expr_manager.cpp')
-rw-r--r-- | src/expr/expr_manager.cpp | 15 |
1 files changed, 7 insertions, 8 deletions
diff --git a/src/expr/expr_manager.cpp b/src/expr/expr_manager.cpp index 6e1be2e09..993bf3483 100644 --- a/src/expr/expr_manager.cpp +++ b/src/expr/expr_manager.cpp @@ -38,14 +38,14 @@ ExprManager::~ExprManager() { delete d_nodeManager; } -const BooleanType* ExprManager::booleanType() { +const BooleanType* ExprManager::booleanType() const { NodeManagerScope nms(d_nodeManager); - return BooleanType::getInstance(); + d_nodeManager->booleanType(); } -const KindType* ExprManager::kindType() { +const KindType* ExprManager::kindType() const { NodeManagerScope nms(d_nodeManager); - return KindType::getInstance(); + d_nodeManager->kindType(); } Expr ExprManager::mkExpr(Kind kind) { @@ -106,7 +106,7 @@ const FunctionType* ExprManager::mkFunctionType(const Type* domain, const Type* range) { NodeManagerScope nms(d_nodeManager); - return FunctionType::getInstance(this, domain, range); + return d_nodeManager->mkFunctionType(domain,range); } /** Make a function type with input types from argTypes. */ @@ -114,13 +114,12 @@ const FunctionType* ExprManager::mkFunctionType(const std::vector<const Type*>& argTypes, const Type* range) { NodeManagerScope nms(d_nodeManager); - return FunctionType::getInstance(this, argTypes, range); + return d_nodeManager->mkFunctionType(argTypes,range); } const Type* ExprManager::mkSort(const std::string& name) { - // FIXME: Sorts should be unique per-ExprManager NodeManagerScope nms(d_nodeManager); - return new SortType(this, name); + return d_nodeManager->mkSort(name); } Expr ExprManager::mkVar(const Type* type, const std::string& name) { |