improving parsing error messages related to HOL (#3510)

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