diff options
| author | Haniel Barbosa <hanielbbarbosa@gmail.com> | 2019-11-29 23:46:55 -0300 |
|---|---|---|
| committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-11-29 20:46:55 -0600 |
| commit | 9bf87b8b5572bbfc110018081b28ad0a88b8a619 (patch) | |
| tree | 58cc585d02302c19ab1ea0f393e06ea856ab1758 /src/parser/smt2/Smt2.g | |
| parent | aada92b267faf9c6388833ae206e421aee18a794 (diff) | |
improving parsing error messages related to HOL (#3510)
Diffstat (limited to 'src/parser/smt2/Smt2.g')
| -rw-r--r-- | src/parser/smt2/Smt2.g | 21 |
1 files changed, 15 insertions, 6 deletions
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<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); } |