From: Haniel Barbosa <hanielbbarbosa@gmail.com>
Date: Wed, 9 Jun 2021 14:34:22 +0000 (-0300)
Subject: Removing spurious HO checks (#6707)
X-Git-Tag: cvc5-1.0.0~1622
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=cbb2fc4b1ec81fe5a3c00dbb030abc4631fe9db8;p=cvc5.git

Removing spurious HO checks (#6707)
---

diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index 1e6a38815..fe7d75ca3 100644
--- a/src/expr/node_manager.cpp
+++ b/src/expr/node_manager.cpp
@@ -528,10 +528,6 @@ TypeNode NodeManager::mkBagType(TypeNode elementType)
 {
   CheckArgument(
       !elementType.isNull(), elementType, "unexpected NULL element type");
-  CheckArgument(elementType.isFirstClass(),
-                elementType,
-                "cannot store types that are not first-class in bags. Try "
-                "option --uf-ho.");
   Debug("bags") << "making bags type " << elementType << std::endl;
   return mkTypeNode(kind::BAG_TYPE, elementType);
 }
@@ -540,10 +536,6 @@ TypeNode NodeManager::mkSequenceType(TypeNode elementType)
 {
   CheckArgument(
       !elementType.isNull(), elementType, "unexpected NULL element type");
-  CheckArgument(elementType.isFirstClass(),
-                elementType,
-                "cannot store types that are not first-class in sequences. Try "
-                "option --uf-ho.");
   return mkTypeNode(kind::SEQUENCE_TYPE, elementType);
 }
 
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index ad0593cee..b651c055a 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -1095,14 +1095,6 @@ inline TypeNode NodeManager::mkArrayType(TypeNode indexType,
                 "unexpected NULL index type");
   CheckArgument(!constituentType.isNull(), constituentType,
                 "unexpected NULL constituent type");
-  CheckArgument(indexType.isFirstClass(),
-                indexType,
-                "cannot index arrays by types that are not first-class. Try "
-                "option --uf-ho.");
-  CheckArgument(constituentType.isFirstClass(),
-                constituentType,
-                "cannot store types that are not first-class in arrays. Try "
-                "option --uf-ho.");
   Debug("arrays") << "making array type " << indexType << " "
                   << constituentType << std::endl;
   return mkTypeNode(kind::ARRAY_TYPE, indexType, constituentType);
@@ -1111,10 +1103,6 @@ inline TypeNode NodeManager::mkArrayType(TypeNode indexType,
 inline TypeNode NodeManager::mkSetType(TypeNode elementType) {
   CheckArgument(!elementType.isNull(), elementType,
                 "unexpected NULL element type");
-  CheckArgument(elementType.isFirstClass(),
-                elementType,
-                "cannot store types that are not first-class in sets. Try "
-                "option --uf-ho.");
   Debug("sets") << "making sets type " << elementType << std::endl;
   return mkTypeNode(kind::SET_TYPE, elementType);
 }