improving parsing error messages related to HOL (#3510)

diff --git a/src/base/exception.h b/src/base/exception.h
index 704ca928e3d06216a51a6e3320ac55499d531e0b..0d1abd9e0b3b8d611fb45293db119ab46c37c1b5 100644 (file)
--- a/src/base/exception.h
+++ b/src/base/exception.h
@@ -128,7 +128,7 @@ template <class T> inline void CheckArgument(bool cond, const T& arg,
 template <class T> inline void CheckArgument(bool cond, const T& arg CVC4_UNUSED,
                                              const char* tail CVC4_UNUSED) {
   if(__builtin_expect( ( !cond ), false )) { \
-    throw ::CVC4::IllegalArgumentException("", "", ""); \
+    throw ::CVC4::IllegalArgumentException("", "", tail); \
   } \
 }
 template <class T> inline void CheckArgument(bool cond, const T& arg)

diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index 8daaa04e6d6d2407c9421bb7407f9804ed620747..f47795c157ad7fd4525e29f9cc2acbf33417385a 100644 (file)
--- 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);
 }
 

diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 9110b9660756231d710de9d243d68486a5fe642f..c1a9df887424b01783cdadd54c997bf78595db92 100644 (file)
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -305,8 +305,11 @@ command [std::unique_ptr<CVC4::Command>* cmd]
         t = PARSER_STATE->mkFlatFunctionType(sorts, t);
       }
       if(t.isFunction() && !PARSER_STATE->isTheoryEnabled(Smt2::THEORY_UF)) {
-        PARSER_STATE->parseErrorLogic("Functions (of non-zero arity) cannot "
-                                      "be declared in logic ");
+        PARSER_STATE->parseError(
+            "Functions (of non-zero arity) cannot "
+            "be declared in logic "
+            + PARSER_STATE->getLogic().getLogicString()
+            + " unless option --uf-ho is used.");
       }
       // we allow overloading for function declarations
       if (PARSER_STATE->sygus_v1())
@@ -1283,8 +1286,11 @@ extendedCommand[std::unique_ptr<CVC4::Command>* cmd]
       { Type t;
         if(sorts.size() > 1) {
           if(!PARSER_STATE->isTheoryEnabled(Smt2::THEORY_UF)) {
-            PARSER_STATE->parseErrorLogic("Functions (of non-zero arity) "
-                                          "cannot be declared in logic ");
+            PARSER_STATE->parseError(
+                "Functions (of non-zero arity) cannot "
+                "be declared in logic "
+                + PARSER_STATE->getLogic().getLogicString()
+                + " unless option --uf-ho is used");
           }
           // must flatten
           Type range = sorts.back();
@@ -1310,8 +1316,11 @@ extendedCommand[std::unique_ptr<CVC4::Command>* cmd]
       { Type t = EXPR_MANAGER->booleanType();
         if(sorts.size() > 0) {
           if(!PARSER_STATE->isTheoryEnabled(Smt2::THEORY_UF)) {
-            PARSER_STATE->parseErrorLogic("Predicates (of non-zero arity) "
-                                          "cannot be declared in logic ");
+            PARSER_STATE->parseError(
+                "Functions (of non-zero arity) cannot "
+                "be declared in logic "
+                + PARSER_STATE->getLogic().getLogicString()
+                + " unless option --uf-ho is used");
           }
           t = EXPR_MANAGER->mkFunctionType(sorts, t);
         }