diff options
author | Morgan Deters <mdeters@gmail.com> | 2011-11-06 02:09:06 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2011-11-06 02:09:06 +0000 |
commit | 0deb883f8c5ba550fda8b90501890940fd916a1b (patch) | |
tree | 645e90ff08d9120f207970f302661a149b988714 /src/expr/expr_manager_template.cpp | |
parent | 4c7de64f3367940faf9c6af48631bc837795c46d (diff) |
datatype stuff in compatibility interface implemented
Diffstat (limited to 'src/expr/expr_manager_template.cpp')
-rw-r--r-- | src/expr/expr_manager_template.cpp | 27 |
1 files changed, 27 insertions, 0 deletions
diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp index 624fbd9a2..12a60021e 100644 --- a/src/expr/expr_manager_template.cpp +++ b/src/expr/expr_manager_template.cpp @@ -268,6 +268,33 @@ Expr ExprManager::mkExpr(Kind kind, const std::vector<Expr>& children) { } } +Expr ExprManager::mkExpr(Kind kind, Expr child1, const std::vector<Expr>& otherChildren) { + const unsigned n = otherChildren.size() - (kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED ? 1 : 0) + 1; + 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); + + vector<Node> nodes; + nodes.push_back(child1.getNode()); + + vector<Expr>::const_iterator it = otherChildren.begin(); + vector<Expr>::const_iterator it_end = otherChildren.end(); + while(it != it_end) { + nodes.push_back(it->getNode()); + ++it; + } + try { + INC_STAT(kind); + return Expr(this, d_nodeManager->mkNodePtr(kind, nodes)); + } catch (const TypeCheckingExceptionPrivate& e) { + throw TypeCheckingException(this, &e); + } +} + Expr ExprManager::mkExpr(Expr opExpr) { const unsigned n = 0; Kind kind = kind::operatorKindToKind(opExpr.getKind()); |