diff options
author | Morgan Deters <mdeters@gmail.com> | 2011-04-18 18:05:39 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2011-04-18 18:05:39 +0000 |
commit | 267858307741675cb78e829270e619f57cf21a27 (patch) | |
tree | d8b663f8b213f6d4a085b06c2f12bffccfd7de33 /src/expr/expr_manager_template.cpp | |
parent | abe849b486ea3707fd51a612c7982554f3d6581f (diff) |
mostly CVC presentation language parsing and printing
Diffstat (limited to 'src/expr/expr_manager_template.cpp')
-rw-r--r-- | src/expr/expr_manager_template.cpp | 172 |
1 files changed, 152 insertions, 20 deletions
diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp index 21fc0a4a1..870c77383 100644 --- a/src/expr/expr_manager_template.cpp +++ b/src/expr/expr_manager_template.cpp @@ -136,8 +136,8 @@ IntegerType ExprManager::integerType() const { return IntegerType(Type(d_nodeManager, new TypeNode(d_nodeManager->integerType()))); } -Expr ExprManager::mkExpr(Kind kind, const Expr& child1) { - const unsigned n = 1; +Expr ExprManager::mkExpr(Kind kind, Expr child1) { + const unsigned n = 1 - (kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED ? 1 : 0); CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind, "Exprs with kind %s must have at least %u children and " "at most %u children (the one under construction has %u)", @@ -152,8 +152,8 @@ Expr ExprManager::mkExpr(Kind kind, const Expr& child1) { } } -Expr ExprManager::mkExpr(Kind kind, const Expr& child1, const Expr& child2) { - const unsigned n = 2; +Expr ExprManager::mkExpr(Kind kind, Expr child1, Expr child2) { + const unsigned n = 2 - (kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED ? 1 : 0); CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind, "Exprs with kind %s must have at least %u children and " "at most %u children (the one under construction has %u)", @@ -170,9 +170,9 @@ Expr ExprManager::mkExpr(Kind kind, const Expr& child1, const Expr& child2) { } } -Expr ExprManager::mkExpr(Kind kind, const Expr& child1, const Expr& child2, - const Expr& child3) { - const unsigned n = 3; +Expr ExprManager::mkExpr(Kind kind, Expr child1, Expr child2, + Expr child3) { + const unsigned n = 3 - (kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED ? 1 : 0); CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind, "Exprs with kind %s must have at least %u children and " "at most %u children (the one under construction has %u)", @@ -190,9 +190,9 @@ Expr ExprManager::mkExpr(Kind kind, const Expr& child1, const Expr& child2, } } -Expr ExprManager::mkExpr(Kind kind, const Expr& child1, const Expr& child2, - const Expr& child3, const Expr& child4) { - const unsigned n = 4; +Expr ExprManager::mkExpr(Kind kind, Expr child1, Expr child2, + Expr child3, Expr child4) { + const unsigned n = 4 - (kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED ? 1 : 0); CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind, "Exprs with kind %s must have at least %u children and " "at most %u children (the one under construction has %u)", @@ -211,10 +211,10 @@ Expr ExprManager::mkExpr(Kind kind, const Expr& child1, const Expr& child2, } } -Expr ExprManager::mkExpr(Kind kind, const Expr& child1, const Expr& child2, - const Expr& child3, const Expr& child4, - const Expr& child5) { - const unsigned n = 5; +Expr ExprManager::mkExpr(Kind kind, Expr child1, Expr child2, + Expr child3, Expr child4, + Expr child5) { + const unsigned n = 5 - (kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED ? 1 : 0); CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind, "Exprs with kind %s must have at least %u children and " "at most %u children (the one under construction has %u)", @@ -235,7 +235,7 @@ Expr ExprManager::mkExpr(Kind kind, const Expr& child1, const Expr& child2, } Expr ExprManager::mkExpr(Kind kind, const std::vector<Expr>& children) { - const unsigned n = children.size(); + const unsigned n = children.size() - (kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED ? 1 : 0); CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind, "Exprs with kind %s must have at least %u children and " "at most %u children (the one under construction has %u)", @@ -259,9 +259,141 @@ Expr ExprManager::mkExpr(Kind kind, const std::vector<Expr>& children) { } } +Expr ExprManager::mkExpr(Expr opExpr) { + const unsigned n = 0; + Kind kind = kind::operatorKindToKind(opExpr.getKind()); + CheckArgument(kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED, opExpr, + "This Expr constructor is for parameterized kinds only"); + CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind, + "Exprs with kind %s must have at least %u children and " + "at most %u children (the one under construction has %u)", + kind::kindToString(kind).c_str(), + minArity(kind), maxArity(kind), n); + NodeManagerScope nms(d_nodeManager); + try { + INC_STAT(kind); + return Expr(this, d_nodeManager->mkNodePtr(opExpr.getNode())); + } catch (const TypeCheckingExceptionPrivate& e) { + throw TypeCheckingException(this, &e); + } +} + +Expr ExprManager::mkExpr(Expr opExpr, Expr child1) { + const unsigned n = 1; + Kind kind = kind::operatorKindToKind(opExpr.getKind()); + CheckArgument(kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED, opExpr, + "This Expr constructor is for parameterized kinds only"); + CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind, + "Exprs with kind %s must have at least %u children and " + "at most %u children (the one under construction has %u)", + kind::kindToString(kind).c_str(), + minArity(kind), maxArity(kind), n); + NodeManagerScope nms(d_nodeManager); + try { + INC_STAT(kind); + return Expr(this, d_nodeManager->mkNodePtr(opExpr.getNode(), child1.getNode())); + } catch (const TypeCheckingExceptionPrivate& e) { + throw TypeCheckingException(this, &e); + } +} + +Expr ExprManager::mkExpr(Expr opExpr, Expr child1, Expr child2) { + const unsigned n = 2; + Kind kind = kind::operatorKindToKind(opExpr.getKind()); + CheckArgument(kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED, opExpr, + "This Expr constructor is for parameterized kinds only"); + CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind, + "Exprs with kind %s must have at least %u children and " + "at most %u children (the one under construction has %u)", + kind::kindToString(kind).c_str(), + minArity(kind), maxArity(kind), n); + NodeManagerScope nms(d_nodeManager); + try { + INC_STAT(kind); + return Expr(this, d_nodeManager->mkNodePtr(opExpr.getNode(), + child1.getNode(), + child2.getNode())); + } catch (const TypeCheckingExceptionPrivate& e) { + throw TypeCheckingException(this, &e); + } +} + +Expr ExprManager::mkExpr(Expr opExpr, Expr child1, Expr child2, Expr child3) { + const unsigned n = 3; + Kind kind = kind::operatorKindToKind(opExpr.getKind()); + CheckArgument(kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED, opExpr, + "This Expr constructor is for parameterized kinds only"); + CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind, + "Exprs with kind %s must have at least %u children and " + "at most %u children (the one under construction has %u)", + kind::kindToString(kind).c_str(), + minArity(kind), maxArity(kind), n); + NodeManagerScope nms(d_nodeManager); + try { + INC_STAT(kind); + return Expr(this, d_nodeManager->mkNodePtr(opExpr.getNode(), + child1.getNode(), + child2.getNode(), + child3.getNode())); + } catch (const TypeCheckingExceptionPrivate& e) { + throw TypeCheckingException(this, &e); + } +} + +Expr ExprManager::mkExpr(Expr opExpr, Expr child1, Expr child2, Expr child3, + Expr child4) { + const unsigned n = 4; + Kind kind = kind::operatorKindToKind(opExpr.getKind()); + CheckArgument(kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED, opExpr, + "This Expr constructor is for parameterized kinds only"); + CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind, + "Exprs with kind %s must have at least %u children and " + "at most %u children (the one under construction has %u)", + kind::kindToString(kind).c_str(), + minArity(kind), maxArity(kind), n); + NodeManagerScope nms(d_nodeManager); + try { + INC_STAT(kind); + return Expr(this, d_nodeManager->mkNodePtr(opExpr.getNode(), + child1.getNode(), + child2.getNode(), + child3.getNode(), + child4.getNode())); + } catch (const TypeCheckingExceptionPrivate& e) { + throw TypeCheckingException(this, &e); + } +} + +Expr ExprManager::mkExpr(Expr opExpr, Expr child1, Expr child2, Expr child3, + Expr child4, Expr child5) { + const unsigned n = 5; + Kind kind = kind::operatorKindToKind(opExpr.getKind()); + CheckArgument(kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED, opExpr, + "This Expr constructor is for parameterized kinds only"); + CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind, + "Exprs with kind %s must have at least %u children and " + "at most %u children (the one under construction has %u)", + kind::kindToString(kind).c_str(), + minArity(kind), maxArity(kind), n); + NodeManagerScope nms(d_nodeManager); + try { + INC_STAT(kind); + return Expr(this, d_nodeManager->mkNodePtr(opExpr.getNode(), + child1.getNode(), + child2.getNode(), + child3.getNode(), + child4.getNode(), + child5.getNode())); + } catch (const TypeCheckingExceptionPrivate& e) { + throw TypeCheckingException(this, &e); + } +} + Expr ExprManager::mkExpr(Expr opExpr, const std::vector<Expr>& children) { const unsigned n = children.size(); Kind kind = kind::operatorKindToKind(opExpr.getKind()); + CheckArgument(kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED, opExpr, + "This Expr constructor is for parameterized kinds only"); CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind, "Exprs with kind %s must have at least %u children and " "at most %u children (the one under construction has %u)", @@ -286,13 +418,13 @@ 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) { +FunctionType ExprManager::mkFunctionType(Type domain, Type range) { NodeManagerScope nms(d_nodeManager); 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. */ -FunctionType ExprManager::mkFunctionType(const std::vector<Type>& argTypes, const Type& range) { +FunctionType ExprManager::mkFunctionType(const std::vector<Type>& argTypes, Type range) { NodeManagerScope nms(d_nodeManager); Assert( argTypes.size() >= 1 ); std::vector<TypeNode> argTypeNodes; @@ -436,7 +568,7 @@ SortConstructorType ExprManager::mkSortConstructor(const std::string& name, * @param check whether we should check the type as we compute it * (default: false) */ -Type ExprManager::getType(const Expr& e, bool check) throw (TypeCheckingException) { +Type ExprManager::getType(Expr e, bool check) throw (TypeCheckingException) { NodeManagerScope nms(d_nodeManager); Type t; try { @@ -448,7 +580,7 @@ Type ExprManager::getType(const Expr& e, bool check) throw (TypeCheckingExceptio return t; } -Expr ExprManager::mkVar(const std::string& name, const Type& type) { +Expr ExprManager::mkVar(const std::string& name, Type type) { NodeManagerScope nms(d_nodeManager); Node* n = d_nodeManager->mkVarPtr(name, *type.d_typeNode); Debug("nm") << "set " << name << " on " << *n << std::endl; @@ -456,7 +588,7 @@ Expr ExprManager::mkVar(const std::string& name, const Type& type) { return Expr(this, n); } -Expr ExprManager::mkVar(const Type& type) { +Expr ExprManager::mkVar(Type type) { NodeManagerScope nms(d_nodeManager); INC_STAT_VAR(type); return Expr(this, d_nodeManager->mkVarPtr(*type.d_typeNode)); |