diff options
author | Aina Niemetz <aina.niemetz@gmail.com> | 2019-01-29 11:47:04 -0800 |
---|---|---|
committer | GitHub <noreply@github.com> | 2019-01-29 11:47:04 -0800 |
commit | d4870775e67c7878c32c17f10b1217c14dc5869b (patch) | |
tree | 8e2bcd1a731eab54041724bb9310e1c7aaaf3e4c /src/expr/expr_manager_template.cpp | |
parent | 1eaf6cf987fa1452528dc0598ca7235be735ba3b (diff) |
New C++ API: Fix checks for mkTerm. (#2820)
This required fixing the OpTerm handling for mkTerm functions in the API.
Diffstat (limited to 'src/expr/expr_manager_template.cpp')
-rw-r--r-- | src/expr/expr_manager_template.cpp | 27 |
1 files changed, 18 insertions, 9 deletions
diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp index e6b89b498..d0d36508f 100644 --- a/src/expr/expr_manager_template.cpp +++ b/src/expr/expr_manager_template.cpp @@ -301,21 +301,30 @@ Expr ExprManager::mkExpr(Kind kind, Expr child1, Expr child2, Expr child3, } } -Expr ExprManager::mkExpr(Kind kind, const std::vector<Expr>& children) { +Expr ExprManager::mkExpr(Kind kind, const std::vector<Expr>& children) +{ + const size_t nchildren = children.size(); const kind::MetaKind mk = kind::metaKindOf(kind); - const unsigned n = children.size() - (mk == kind::metakind::PARAMETERIZED ? 1 : 0); PrettyCheckArgument( - mk == kind::metakind::PARAMETERIZED || - mk == kind::metakind::OPERATOR, kind, + mk == kind::metakind::PARAMETERIZED || mk == kind::metakind::OPERATOR, + kind, "Only operator-style expressions are made with mkExpr(); " "to make variables and constants, see mkVar(), mkBoundVar(), " "and mkConst()."); PrettyCheckArgument( - 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); + mk != kind::metakind::PARAMETERIZED || nchildren > 0, + kind, + "Terms with kind %s must have an operator expression as first argument", + kind::kindToString(kind).c_str()); + const size_t n = nchildren - (mk == kind::metakind::PARAMETERIZED ? 1 : 0); + PrettyCheckArgument(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); |