From 9bf87b8b5572bbfc110018081b28ad0a88b8a619 Mon Sep 17 00:00:00 2001 From: Haniel Barbosa Date: Fri, 29 Nov 2019 23:46:55 -0300 Subject: improving parsing error messages related to HOL (#3510) --- src/base/exception.h | 2 +- src/expr/node_manager.h | 36 ++++++++++++++++++++++++------------ src/parser/smt2/Smt2.g | 21 +++++++++++++++------ 3 files changed, 40 insertions(+), 19 deletions(-) diff --git a/src/base/exception.h b/src/base/exception.h index 704ca928e..0d1abd9e0 100644 --- a/src/base/exception.h +++ b/src/base/exception.h @@ -128,7 +128,7 @@ template inline void CheckArgument(bool cond, const T& arg, template 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 inline void CheckArgument(bool cond, const T& arg) 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& sorts) { Assert(sorts.size() >= 2); std::vector 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& sorts) { Assert(sorts.size() >= 1); std::vector 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 9110b9660..c1a9df887 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -305,8 +305,11 @@ command [std::unique_ptr* 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* 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* 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); } -- cgit v1.2.3