From 90107a2c332fb4137a432424136cbfd1ab88b34d Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Fri, 11 May 2012 19:11:56 +0000 Subject: output a warning message when a function type (or datatype, or array, etc.) is created with a Boolean term inside it --- src/expr/expr_manager_template.cpp | 4 ++++ src/expr/node_manager.h | 14 +++++++++++++- 2 files changed, 17 insertions(+), 1 deletion(-) (limited to 'src/expr') diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp index 8819684fc..cf2616011 100644 --- a/src/expr/expr_manager_template.cpp +++ b/src/expr/expr_manager_template.cpp @@ -685,6 +685,10 @@ void ExprManager::checkResolvedDatatype(DatatypeType dtt) const { // CVC4::Datatype class, but this actually needs to be checked. AlwaysAssert(!SelectorType(selectorType).getRangeType().d_typeNode->isFunctionLike(), "cannot put function-like things in datatypes"); + // currently don't play well with Boolean terms + if(SelectorType(selectorType).getRangeType().d_typeNode->isBoolean()) { + WarningOnce() << "Warning: CVC4 does not yet support Boolean terms (you have created a datatype containing a Boolean)" << std::endl; + } } } } diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index b5ac9e973..593f3f715 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -932,6 +932,9 @@ NodeManager::mkFunctionType(const std::vector& sorts) { for (unsigned i = 0; i < sorts.size(); ++ i) { CheckArgument(!sorts[i].isFunctionLike(), sorts, "cannot create higher-order function types"); + if(i + 1 < sorts.size() && sorts[i].isBoolean()) { + WarningOnce() << "Warning: CVC4 does not yet support Boolean terms (you have created a function type with a Boolean argument)" << std::endl; + } sortNodes.push_back(sorts[i]); } return mkTypeNode(kind::FUNCTION_TYPE, sortNodes); @@ -944,6 +947,9 @@ NodeManager::mkPredicateType(const std::vector& sorts) { for (unsigned i = 0; i < sorts.size(); ++ i) { CheckArgument(!sorts[i].isFunctionLike(), sorts, "cannot create higher-order function types"); + if(i + 1 < sorts.size() && sorts[i].isBoolean()) { + WarningOnce() << "Warning: CVC4 does not yet support Boolean terms (you have created a predicate type with a Boolean argument)" << std::endl; + } sortNodes.push_back(sorts[i]); } sortNodes.push_back(booleanType()); @@ -958,6 +964,9 @@ inline TypeNode NodeManager::mkTupleType(const std::vector& types) { #if 0 CheckArgument(!types[i].isFunctionLike(), types, "cannot put function-like types in tuples"); + if(types[i].isBoolean()) { + WarningOnce() << "Warning: CVC4 does not yet support Boolean terms (you have created a tuple type with a Boolean argument)" << std::endl; + } #endif /* 0 */ typeNodes.push_back(types[i]); } @@ -978,7 +987,10 @@ inline TypeNode NodeManager::mkArrayType(TypeNode indexType, "cannot index arrays by a function-like type"); CheckArgument(!constituentType.isFunctionLike(), constituentType, "cannot store function-like types in arrays"); -Debug("arrays") << "making array type " << indexType << " " << constituentType << std::endl; + if(indexType.isBoolean() || constituentType.isBoolean()) { + WarningOnce() << "Warning: CVC4 does not yet support Boolean terms (you have created an array type with a Boolean index or constituent type)" << std::endl; + } + Debug("arrays") << "making array type " << indexType << " " << constituentType << std::endl; return mkTypeNode(kind::ARRAY_TYPE, indexType, constituentType); } -- cgit v1.2.3