diff options
Diffstat (limited to 'src/expr/node_manager.h')
-rw-r--r-- | src/expr/node_manager.h | 36 |
1 files changed, 24 insertions, 12 deletions
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index 8daaa04e6..f47795c15 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -1095,8 +1095,10 @@ NodeManager::mkFunctionType(const std::vector<TypeNode>& sorts) { Assert(sorts.size() >= 2); std::vector<TypeNode> sortNodes; for (unsigned i = 0; i < sorts.size(); ++ i) { - CheckArgument(sorts[i].isFirstClass(), sorts, - "cannot create function types for argument types that are not first-class"); + CheckArgument(sorts[i].isFirstClass(), + sorts, + "cannot create function types for argument types that are " + "not first-class. Try option --uf-ho."); sortNodes.push_back(sorts[i]); } CheckArgument(!sorts[sorts.size()-1].isFunction(), sorts[sorts.size()-1], @@ -1109,8 +1111,10 @@ NodeManager::mkPredicateType(const std::vector<TypeNode>& sorts) { Assert(sorts.size() >= 1); std::vector<TypeNode> sortNodes; for (unsigned i = 0; i < sorts.size(); ++ i) { - CheckArgument(sorts[i].isFirstClass(), sorts, - "cannot create predicate types for argument types that are not first-class"); + CheckArgument(sorts[i].isFirstClass(), + sorts, + "cannot create predicate types for argument types that are " + "not first-class. Try option --uf-ho."); sortNodes.push_back(sorts[i]); } sortNodes.push_back(booleanType()); @@ -1143,10 +1147,14 @@ 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"); - CheckArgument(constituentType.isFirstClass(), constituentType, - "cannot store types that are not first-class in arrays"); + 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); @@ -1155,8 +1163,10 @@ 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"); + 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); } @@ -1164,8 +1174,10 @@ inline TypeNode NodeManager::mkSetType(TypeNode elementType) { inline TypeNode NodeManager::mkSelectorType(TypeNode domain, TypeNode range) { CheckArgument(domain.isDatatype(), domain, "cannot create non-datatype selector type"); - CheckArgument(range.isFirstClass(), range, - "cannot have selector fields that are not first-class types"); + CheckArgument(range.isFirstClass(), + range, + "cannot have selector fields that are not first-class types. " + "Try option --uf-ho."); return mkTypeNode(kind::SELECTOR_TYPE, domain, range); } |