diff options
Diffstat (limited to 'src/expr/expr_manager_template.cpp')
-rw-r--r-- | src/expr/expr_manager_template.cpp | 51 |
1 files changed, 29 insertions, 22 deletions
diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp index 56b89c125..55b59d13c 100644 --- a/src/expr/expr_manager_template.cpp +++ b/src/expr/expr_manager_template.cpp @@ -88,11 +88,11 @@ Expr ExprManager::mkExpr(Kind kind, const Expr& child1, const Expr& child2) { minArity(kind), maxArity(kind), n); NodeManagerScope nms(d_nodeManager); try { - return Expr(this, d_nodeManager->mkNodePtr(kind, + return Expr(this, d_nodeManager->mkNodePtr(kind, child1.getNode(), child2.getNode())); } catch (const TypeCheckingExceptionPrivate& e) { - throw TypeCheckingException(Expr(this, new Node(e.getNode())), + throw TypeCheckingException(Expr(this, new Node(e.getNode())), e.getMessage()); } } @@ -107,12 +107,12 @@ Expr ExprManager::mkExpr(Kind kind, const Expr& child1, const Expr& child2, minArity(kind), maxArity(kind), n); NodeManagerScope nms(d_nodeManager); try { - return Expr(this, d_nodeManager->mkNodePtr(kind, - child1.getNode(), - child2.getNode(), + return Expr(this, d_nodeManager->mkNodePtr(kind, + child1.getNode(), + child2.getNode(), child3.getNode())); } catch (const TypeCheckingExceptionPrivate& e) { - throw TypeCheckingException(Expr(this, new Node(e.getNode())), + throw TypeCheckingException(Expr(this, new Node(e.getNode())), e.getMessage()); } } @@ -127,13 +127,13 @@ Expr ExprManager::mkExpr(Kind kind, const Expr& child1, const Expr& child2, minArity(kind), maxArity(kind), n); NodeManagerScope nms(d_nodeManager); try { - return Expr(this, d_nodeManager->mkNodePtr(kind, + return Expr(this, d_nodeManager->mkNodePtr(kind, child1.getNode(), - child2.getNode(), + child2.getNode(), child3.getNode(), child4.getNode())); } catch (const TypeCheckingExceptionPrivate& e) { - throw TypeCheckingException(Expr(this, new Node(e.getNode())), + throw TypeCheckingException(Expr(this, new Node(e.getNode())), e.getMessage()); } } @@ -149,14 +149,14 @@ Expr ExprManager::mkExpr(Kind kind, const Expr& child1, const Expr& child2, minArity(kind), maxArity(kind), n); NodeManagerScope nms(d_nodeManager); try { - return Expr(this, d_nodeManager->mkNodePtr(kind, + return Expr(this, d_nodeManager->mkNodePtr(kind, child1.getNode(), - child2.getNode(), + child2.getNode(), child3.getNode(), child4.getNode(), child5.getNode())); } catch (const TypeCheckingExceptionPrivate& e) { - throw TypeCheckingException(Expr(this, new Node(e.getNode())), + throw TypeCheckingException(Expr(this, new Node(e.getNode())), e.getMessage()); } } @@ -181,7 +181,7 @@ Expr ExprManager::mkExpr(Kind kind, const std::vector<Expr>& children) { try { return Expr(this, d_nodeManager->mkNodePtr(kind, nodes)); } catch (const TypeCheckingExceptionPrivate& e) { - throw TypeCheckingException(Expr(this, new Node(e.getNode())), + throw TypeCheckingException(Expr(this, new Node(e.getNode())), e.getMessage()); } } @@ -219,8 +219,8 @@ FunctionType ExprManager::mkFunctionType(const Type& domain, const Type& range) /** 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); + Assert( argTypes.size() >= 1 ); std::vector<TypeNode> argTypeNodes; for (unsigned i = 0, i_end = argTypes.size(); i < i_end; ++ i) { argTypeNodes.push_back(*argTypes[i].d_typeNode); @@ -229,8 +229,8 @@ FunctionType ExprManager::mkFunctionType(const std::vector<Type>& argTypes, cons } FunctionType ExprManager::mkFunctionType(const std::vector<Type>& sorts) { - Assert( sorts.size() >= 2 ); NodeManagerScope nms(d_nodeManager); + Assert( sorts.size() >= 2 ); std::vector<TypeNode> sortNodes; for (unsigned i = 0, i_end = sorts.size(); i < i_end; ++ i) { sortNodes.push_back(*sorts[i].d_typeNode); @@ -239,8 +239,8 @@ FunctionType ExprManager::mkFunctionType(const std::vector<Type>& sorts) { } FunctionType ExprManager::mkPredicateType(const std::vector<Type>& sorts) { - Assert( sorts.size() >= 1 ); NodeManagerScope nms(d_nodeManager); + Assert( sorts.size() >= 1 ); std::vector<TypeNode> sortNodes; for (unsigned i = 0, i_end = sorts.size(); i < i_end; ++ i) { sortNodes.push_back(*sorts[i].d_typeNode); @@ -249,8 +249,8 @@ FunctionType ExprManager::mkPredicateType(const std::vector<Type>& sorts) { } TupleType ExprManager::mkTupleType(const std::vector<Type>& types) { - Assert( types.size() >= 2 ); NodeManagerScope nms(d_nodeManager); + Assert( types.size() >= 2 ); std::vector<TypeNode> typeNodes; for (unsigned i = 0, i_end = types.size(); i < i_end; ++ i) { typeNodes.push_back(*types[i].d_typeNode); @@ -268,9 +268,16 @@ ArrayType ExprManager::mkArrayType(Type indexType, Type constituentType) const { return Type(d_nodeManager, new TypeNode(d_nodeManager->mkArrayType(*indexType.d_typeNode, *constituentType.d_typeNode))); } -SortType ExprManager::mkSort(const std::string& name, size_t arity) const { +SortType ExprManager::mkSort(const std::string& name) const { + NodeManagerScope nms(d_nodeManager); + return 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->mkSort(name, arity))); + return Type(d_nodeManager, + new TypeNode(d_nodeManager->mkSortConstructor(name, arity))); } /** @@ -295,7 +302,7 @@ SortType ExprManager::mkSort(const std::string& name, size_t arity) const { * amount of checking required to return a valid result. * * @param n the Expr for which we want a type - * @param check whether we should check the type as we compute it + * @param check whether we should check the type as we compute it * (default: false) */ Type ExprManager::getType(const Expr& e, bool check) throw (TypeCheckingException) { @@ -333,7 +340,7 @@ Expr ExprManager::mkAssociative(Kind kind, /* If the number of children is within bounds, then there's nothing to do. */ if( numChildren <= max ) { return mkExpr(kind,children); - } + } std::vector<Expr>::const_iterator it = children.begin() ; std::vector<Expr>::const_iterator end = children.end() ; @@ -379,7 +386,7 @@ Expr ExprManager::mkAssociative(Kind kind, /* It would be really weird if this happened (it would require * min > 2, for one thing), but let's make sure. */ - AlwaysAssert( newChildren.size() >= min, + AlwaysAssert( newChildren.size() >= min, "Too few new children in mkAssociative" ); return Expr(this, d_nodeManager->mkNodePtr(kind,newChildren) ); |