diff options
Diffstat (limited to 'src/expr/expr_manager_template.cpp')
-rw-r--r-- | src/expr/expr_manager_template.cpp | 32 |
1 files changed, 22 insertions, 10 deletions
diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp index 7407043d2..5d50dd100 100644 --- a/src/expr/expr_manager_template.cpp +++ b/src/expr/expr_manager_template.cpp @@ -48,12 +48,12 @@ ExprManager::~ExprManager() { BooleanType ExprManager::booleanType() const { NodeManagerScope nms(d_nodeManager); - return d_nodeManager->booleanType(); + return Type(d_nodeManager, new TypeNode(d_nodeManager->booleanType())); } KindType ExprManager::kindType() const { NodeManagerScope nms(d_nodeManager); - return d_nodeManager->kindType(); + return Type(d_nodeManager, new TypeNode(d_nodeManager->kindType())); } Expr ExprManager::mkExpr(Kind kind) { @@ -154,46 +154,58 @@ Expr ExprManager::mkExpr(Kind kind, 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 d_nodeManager->mkFunctionType(domain, range); + return Type(d_nodeManager, new TypeNode(d_nodeManager->mkFunctionType(*domain.d_typeNode, *range.d_typeNode))); } /** Make a function type with input types from argTypes. */ FunctionType ExprManager::mkFunctionType(const std::vector<Type>& argTypes, const Type& range) { Assert( argTypes.size() >= 1 ); NodeManagerScope nms(d_nodeManager); - return d_nodeManager->mkFunctionType(argTypes, range); + std::vector<TypeNode> argTypeNodes; + 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))); } FunctionType ExprManager::mkFunctionType(const std::vector<Type>& sorts) { Assert( sorts.size() >= 2 ); NodeManagerScope nms(d_nodeManager); - return d_nodeManager->mkFunctionType(sorts); + std::vector<TypeNode> sortNodes; + 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))); } FunctionType ExprManager::mkPredicateType(const std::vector<Type>& sorts) { Assert( sorts.size() >= 1 ); NodeManagerScope nms(d_nodeManager); - return d_nodeManager->mkPredicateType(sorts); + std::vector<TypeNode> sortNodes; + 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))); } SortType ExprManager::mkSort(const std::string& name) { NodeManagerScope nms(d_nodeManager); - return d_nodeManager->mkSort(name); + return Type(d_nodeManager, new TypeNode(d_nodeManager->mkSort(name))); } Type ExprManager::getType(const Expr& e) { NodeManagerScope nms(d_nodeManager); - return d_nodeManager->getType(e.getNode()); + return Type(d_nodeManager, new TypeNode(d_nodeManager->getType(e.getNode()))); } Expr ExprManager::mkVar(const std::string& name, const Type& type) { NodeManagerScope nms(d_nodeManager); - return Expr(this, d_nodeManager->mkVarPtr(name, type)); + return Expr(this, d_nodeManager->mkVarPtr(name, *type.d_typeNode)); } Expr ExprManager::mkVar(const Type& type) { NodeManagerScope nms(d_nodeManager); - return Expr(this, d_nodeManager->mkVarPtr(type)); + return Expr(this, d_nodeManager->mkVarPtr(*type.d_typeNode)); } unsigned ExprManager::minArity(Kind kind) { |