diff options
author | Haniel Barbosa <hanielbbarbosa@gmail.com> | 2021-06-09 11:34:22 -0300 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-06-09 14:34:22 +0000 |
commit | cbb2fc4b1ec81fe5a3c00dbb030abc4631fe9db8 (patch) | |
tree | d121d6076625526177c7f656fb28119f76f83791 /src/expr | |
parent | b77fe268066841fa532e1d19ecf5e55c441ca034 (diff) |
Removing spurious HO checks (#6707)
Diffstat (limited to 'src/expr')
-rw-r--r-- | src/expr/node_manager.cpp | 8 | ||||
-rw-r--r-- | src/expr/node_manager.h | 12 |
2 files changed, 0 insertions, 20 deletions
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); } |