output a warning message when a function type (or datatype, or array, etc.) is created with a Boolean term inside it

2 files changed, 17 insertions, 1 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;
+      }
     }
   }
 }
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);
 }