diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-05-11 19:11:56 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-05-11 19:11:56 +0000 |
commit | 90107a2c332fb4137a432424136cbfd1ab88b34d (patch) | |
tree | f30ee0c34fac6b524ebceb6ed89cb0a1d7a714e6 /src/expr/node_manager.h | |
parent | f20e159baa1669bbedbf6afd4f0a5117854822a9 (diff) |
output a warning message when a function type (or datatype, or array, etc.) is created with a Boolean term inside it
Diffstat (limited to 'src/expr/node_manager.h')
-rw-r--r-- | src/expr/node_manager.h | 14 |
1 files changed, 13 insertions, 1 deletions
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<TypeNode>& 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<TypeNode>& 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<TypeNode>& 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); } |