diff options
author | Tim King <taking@google.com> | 2015-12-24 05:38:43 -0500 |
---|---|---|
committer | Tim King <taking@google.com> | 2015-12-24 05:38:43 -0500 |
commit | a39ad6584c1d61e22e72b53c3838f4f675ed2e19 (patch) | |
tree | ed40cb371c41ac285ca2bf41a82254a36134e132 /src/expr/expr_manager_template.cpp | |
parent | 87b0fe9ce10d1e5e9ed5a3e7db77f46bf3f68922 (diff) |
Miscellaneous fixes
- Splitting the two instances of CheckArgument. The template version is now always defined in base/exception.h and is available in a cvc4_public header. This version has lost its variadic version (due to swig not supporting va_list's). The CPP macro version has been renamed PrettyCheckArgument. (Taking suggestions for a better name.) This is now only defined in base/cvc4_assert.h. Only use this in cvc4_private headers and in .cpp files that can use cvc4_private headers. To use a variadic version of CheckArguments, outside of this scope, you need to duplicate this macro locally. See cvc3_compat.cpp for an example.
- Making fitsSignedInt() and fitsUnsignedInt() work more robustly for CLN on 32 bit systems.
- Refactoring ArrayStoreAll to avoid potential problems with circular header inclusions.
- Changing some headers to use iosfwd when possible.
Diffstat (limited to 'src/expr/expr_manager_template.cpp')
-rw-r--r-- | src/expr/expr_manager_template.cpp | 296 |
1 files changed, 168 insertions, 128 deletions
diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp index e7088a395..59f423e3c 100644 --- a/src/expr/expr_manager_template.cpp +++ b/src/expr/expr_manager_template.cpp @@ -29,7 +29,7 @@ ${includes} // compiler directs the user to the template file instead of the // generated one. We don't want the user to modify the generated one, // since it'll get overwritten on a later build. -#line 32 "${template}" +#line 33 "${template}" #ifdef CVC4_STATISTICS_ON #define INC_STAT(kind) \ @@ -164,16 +164,18 @@ RoundingModeType ExprManager::roundingModeType() const { Expr ExprManager::mkExpr(Kind kind, Expr child1) { const kind::MetaKind mk = kind::metaKindOf(kind); const unsigned n = 1 - (mk == kind::metakind::PARAMETERIZED ? 1 : 0); - CheckArgument(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()."); - 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); + PrettyCheckArgument( + 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); NodeManagerScope nms(d_nodeManager); try { INC_STAT(kind); @@ -186,16 +188,18 @@ Expr ExprManager::mkExpr(Kind kind, Expr child1) { Expr ExprManager::mkExpr(Kind kind, Expr child1, Expr child2) { const kind::MetaKind mk = kind::metaKindOf(kind); const unsigned n = 2 - (mk == kind::metakind::PARAMETERIZED ? 1 : 0); - CheckArgument(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()."); - 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); + PrettyCheckArgument( + 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); NodeManagerScope nms(d_nodeManager); try { INC_STAT(kind); @@ -210,16 +214,18 @@ Expr ExprManager::mkExpr(Kind kind, Expr child1, Expr child2) { Expr ExprManager::mkExpr(Kind kind, Expr child1, Expr child2, Expr child3) { const kind::MetaKind mk = kind::metaKindOf(kind); const unsigned n = 3 - (mk == kind::metakind::PARAMETERIZED ? 1 : 0); - CheckArgument(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()."); - 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); + PrettyCheckArgument( + 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); NodeManagerScope nms(d_nodeManager); try { INC_STAT(kind); @@ -236,16 +242,18 @@ Expr ExprManager::mkExpr(Kind kind, Expr child1, Expr child2, Expr child3, Expr child4) { const kind::MetaKind mk = kind::metaKindOf(kind); const unsigned n = 4 - (mk == kind::metakind::PARAMETERIZED ? 1 : 0); - CheckArgument(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()."); - 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); + PrettyCheckArgument( + 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); NodeManagerScope nms(d_nodeManager); try { INC_STAT(kind); @@ -263,16 +271,18 @@ Expr ExprManager::mkExpr(Kind kind, Expr child1, Expr child2, Expr child3, Expr child4, Expr child5) { const kind::MetaKind mk = kind::metaKindOf(kind); const unsigned n = 5 - (mk == kind::metakind::PARAMETERIZED ? 1 : 0); - CheckArgument(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()."); - 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); + PrettyCheckArgument( + 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); NodeManagerScope nms(d_nodeManager); try { INC_STAT(kind); @@ -290,16 +300,18 @@ Expr ExprManager::mkExpr(Kind kind, Expr child1, Expr child2, Expr child3, Expr ExprManager::mkExpr(Kind kind, const std::vector<Expr>& children) { const kind::MetaKind mk = kind::metaKindOf(kind); const unsigned n = children.size() - (mk == kind::metakind::PARAMETERIZED ? 1 : 0); - CheckArgument(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()."); - 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); + PrettyCheckArgument( + 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); NodeManagerScope nms(d_nodeManager); @@ -321,17 +333,20 @@ Expr ExprManager::mkExpr(Kind kind, const std::vector<Expr>& children) { Expr ExprManager::mkExpr(Kind kind, Expr child1, const std::vector<Expr>& otherChildren) { const kind::MetaKind mk = kind::metaKindOf(kind); - const unsigned n = otherChildren.size() - (mk == kind::metakind::PARAMETERIZED ? 1 : 0) + 1; - CheckArgument(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()."); - 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); + const unsigned n = + otherChildren.size() - (mk == kind::metakind::PARAMETERIZED ? 1 : 0) + 1; + PrettyCheckArgument( + 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); NodeManagerScope nms(d_nodeManager); @@ -355,13 +370,16 @@ Expr ExprManager::mkExpr(Kind kind, Expr child1, Expr ExprManager::mkExpr(Expr opExpr) { const unsigned n = 0; Kind kind = NodeManager::operatorToKind(opExpr.getNode()); - CheckArgument(opExpr.getKind() == kind::BUILTIN || 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); + PrettyCheckArgument( + opExpr.getKind() == kind::BUILTIN || + kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED, opExpr, + "This Expr constructor is for parameterized kinds only"); + 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); try { INC_STAT(kind); @@ -374,13 +392,16 @@ Expr ExprManager::mkExpr(Expr opExpr) { Expr ExprManager::mkExpr(Expr opExpr, Expr child1) { const unsigned n = 1; Kind kind = NodeManager::operatorToKind(opExpr.getNode()); - CheckArgument(opExpr.getKind() == kind::BUILTIN || 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); + PrettyCheckArgument( + (opExpr.getKind() == kind::BUILTIN || + kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED), opExpr, + "This Expr constructor is for parameterized kinds only"); + 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); try { INC_STAT(kind); @@ -393,13 +414,16 @@ Expr ExprManager::mkExpr(Expr opExpr, Expr child1) { Expr ExprManager::mkExpr(Expr opExpr, Expr child1, Expr child2) { const unsigned n = 2; Kind kind = NodeManager::operatorToKind(opExpr.getNode()); - CheckArgument(opExpr.getKind() == kind::BUILTIN || 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); + PrettyCheckArgument( + (opExpr.getKind() == kind::BUILTIN || + kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED), opExpr, + "This Expr constructor is for parameterized kinds only"); + 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); try { INC_STAT(kind); @@ -414,9 +438,11 @@ Expr ExprManager::mkExpr(Expr opExpr, Expr child1, Expr child2) { Expr ExprManager::mkExpr(Expr opExpr, Expr child1, Expr child2, Expr child3) { const unsigned n = 3; Kind kind = NodeManager::operatorToKind(opExpr.getNode()); - CheckArgument(opExpr.getKind() == kind::BUILTIN || kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED, opExpr, + PrettyCheckArgument( + (opExpr.getKind() == kind::BUILTIN || + kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED), opExpr, "This Expr constructor is for parameterized kinds only"); - CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind, + 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(), @@ -437,13 +463,18 @@ Expr ExprManager::mkExpr(Expr opExpr, Expr child1, Expr child2, Expr child3, Expr child4) { const unsigned n = 4; Kind kind = NodeManager::operatorToKind(opExpr.getNode()); - CheckArgument(opExpr.getKind() == kind::BUILTIN || 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); + PrettyCheckArgument( + (opExpr.getKind() == kind::BUILTIN || + kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED), opExpr, + "This Expr constructor is for parameterized kinds only"); + + 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); try { INC_STAT(kind); @@ -461,13 +492,16 @@ Expr ExprManager::mkExpr(Expr opExpr, Expr child1, Expr child2, Expr child3, Expr child4, Expr child5) { const unsigned n = 5; Kind kind = NodeManager::operatorToKind(opExpr.getNode()); - CheckArgument(opExpr.getKind() == kind::BUILTIN || 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); + PrettyCheckArgument( + (opExpr.getKind() == kind::BUILTIN || + kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED), opExpr, + "This Expr constructor is for parameterized kinds only"); + 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); try { INC_STAT(kind); @@ -485,13 +519,16 @@ Expr ExprManager::mkExpr(Expr opExpr, Expr child1, Expr child2, Expr child3, Expr ExprManager::mkExpr(Expr opExpr, const std::vector<Expr>& children) { const unsigned n = children.size(); Kind kind = NodeManager::operatorToKind(opExpr.getNode()); - CheckArgument(opExpr.getKind() == kind::BUILTIN || 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); + PrettyCheckArgument( + (opExpr.getKind() == kind::BUILTIN || + kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED), opExpr, + "This Expr constructor is for parameterized kinds only"); + 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); @@ -652,11 +689,12 @@ ExprManager::mkMutualDatatypeTypes(const std::vector<Datatype>& datatypes, } Type type(d_nodeManager, typeNode); DatatypeType dtt(type); - CheckArgument(nameResolutions.find((*i).getName()) == nameResolutions.end(), - datatypes, - "cannot construct two datatypes at the same time " - "with the same name `%s'", - (*i).getName().c_str()); + PrettyCheckArgument( + nameResolutions.find((*i).getName()) == nameResolutions.end(), + datatypes, + "cannot construct two datatypes at the same time " + "with the same name `%s'", + (*i).getName().c_str()); nameResolutions.insert(std::make_pair((*i).getName(), dtt)); dtts.push_back(dtt); } @@ -687,10 +725,11 @@ ExprManager::mkMutualDatatypeTypes(const std::vector<Datatype>& datatypes, } std::map<std::string, DatatypeType>::const_iterator resolver = nameResolutions.find(name); - CheckArgument(resolver != nameResolutions.end(), - unresolvedTypes, - "cannot resolve type `%s'; it's not among " - "the datatypes being defined", name.c_str()); + PrettyCheckArgument( + resolver != nameResolutions.end(), + unresolvedTypes, + "cannot resolve type `%s'; it's not among " + "the datatypes being defined", name.c_str()); // We will instruct the Datatype to substitute "*i" (the // unresolved SortType used as a placeholder in complex types) // with "(*resolver).second" (the DatatypeType we created in the @@ -902,9 +941,10 @@ Expr ExprManager::mkBoundVar(Type type) { Expr ExprManager::mkAssociative(Kind kind, const std::vector<Expr>& children) { - CheckArgument( kind::isAssociative(kind), kind, - "Illegal kind in mkAssociative: %s", - kind::kindToString(kind).c_str()); + PrettyCheckArgument( + kind::isAssociative(kind), kind, + "Illegal kind in mkAssociative: %s", + kind::kindToString(kind).c_str()); NodeManagerScope nms(d_nodeManager); const unsigned int max = maxArity(kind); |