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/expr_manager_template.cpp | |
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/expr_manager_template.cpp')
-rw-r--r-- | src/expr/expr_manager_template.cpp | 4 |
1 files changed, 4 insertions, 0 deletions
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; + } } } } |