First chunk of boolean-terms support.

Passes simple tests and doesn't break existing functionality.
Still need some work merged in for models.

This version enables BV except for pure arithmetic (since we might otherwise need Boolean term support, which uses BV).  Tonight's nightly regression run should tell us if/how that hurts performance.

(this commit was certified error- and warning-free by the test-and-commit script.)

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);
 }