summaryrefslogtreecommitdiff
path: root/src/expr/expr_manager_template.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/expr/expr_manager_template.cpp')
-rw-r--r--src/expr/expr_manager_template.cpp51
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) );
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback