diff options
Diffstat (limited to 'src/expr/node_manager.h')
-rw-r--r-- | src/expr/node_manager.h | 12 |
1 files changed, 0 insertions, 12 deletions
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index 6e08a9bc2..5cf591f9d 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -1055,9 +1055,6 @@ 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); @@ -1070,9 +1067,6 @@ 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()); @@ -1085,9 +1079,6 @@ inline TypeNode NodeManager::mkTupleType(const std::vector<TypeNode>& types) { for (unsigned i = 0; i < types.size(); ++ i) { 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; - } typeNodes.push_back(types[i]); } return mkTypeNode(kind::TUPLE_TYPE, typeNodes); @@ -1119,9 +1110,6 @@ 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"); - 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); } |