diff options
| author | Morgan Deters <mdeters@cs.nyu.edu> | 2014-03-15 17:29:09 -0400 |
|---|---|---|
| committer | Morgan Deters <mdeters@cs.nyu.edu> | 2014-03-19 10:38:05 -0400 |
| commit | 035aaf3a248960e6bbe6a7350fa8e4ca86b35f94 (patch) | |
| tree | cd9cb21c00fba3bfb297afecb7e671df42ef246f /src/parser/smt2/Smt2.g | |
| parent | 4edafb39fd8989238a01f3b0b925e191765799ad (diff) | |
Minor usability fixes related to SMT-LIB compliance.
Diffstat (limited to 'src/parser/smt2/Smt2.g')
| -rw-r--r-- | src/parser/smt2/Smt2.g | 23 |
1 files changed, 23 insertions, 0 deletions
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 3c68e4e4c..f987de2f1 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -253,6 +253,13 @@ command returns [CVC4::Command* cmd = NULL] { cmd = new GetOptionCommand(AntlrInput::tokenText($KEYWORD).c_str() + 1); } | /* sort declaration */ DECLARE_SORT_TOK { PARSER_STATE->checkThatLogicIsSet(); } + { if(!PARSER_STATE->isTheoryEnabled(Smt2::THEORY_UF) && + !PARSER_STATE->isTheoryEnabled(Smt2::THEORY_ARRAYS) && + !PARSER_STATE->isTheoryEnabled(Smt2::THEORY_DATATYPES) && + !PARSER_STATE->isTheoryEnabled(Smt2::THEORY_SETS)) { + PARSER_STATE->parseError(std::string("Free sort symbols not allowed in ") + PARSER_STATE->getLogic().getLogicString()); + } + } symbol[name,CHECK_UNDECLARED,SYM_SORT] { PARSER_STATE->checkUserSymbol(name); } n=INTEGER_LITERAL @@ -295,6 +302,9 @@ command returns [CVC4::Command* cmd = NULL] sortSymbol[t,CHECK_DECLARED] { Debug("parser") << "declare fun: '" << name << "'" << std::endl; if( sorts.size() > 0 ) { + if(!PARSER_STATE->isTheoryEnabled(Smt2::THEORY_UF)) { + PARSER_STATE->parseError(std::string("Functions (of non-zero arity) cannot be declared in logic ") + PARSER_STATE->getLogic().getLogicString()); + } t = EXPR_MANAGER->mkFunctionType(sorts, t); } Expr func = PARSER_STATE->mkVar(name, t); @@ -488,6 +498,13 @@ extendedCommand[CVC4::Command*& cmd] $cmd = new DeclareFunctionCommand(name, c, t); } | DECLARE_SORTS_TOK { PARSER_STATE->checkThatLogicIsSet(); } + { if(!PARSER_STATE->isTheoryEnabled(Smt2::THEORY_UF) && + !PARSER_STATE->isTheoryEnabled(Smt2::THEORY_ARRAYS) && + !PARSER_STATE->isTheoryEnabled(Smt2::THEORY_DATATYPES) && + !PARSER_STATE->isTheoryEnabled(Smt2::THEORY_SETS)) { + PARSER_STATE->parseError(std::string("Free sort symbols not allowed in ") + PARSER_STATE->getLogic().getLogicString()); + } + } { $cmd = new CommandSequence(); } LPAREN_TOK ( symbol[name,CHECK_UNDECLARED,SYM_SORT] @@ -506,6 +523,9 @@ extendedCommand[CVC4::Command*& cmd] nonemptySortList[sorts] RPAREN_TOK { Type t; if(sorts.size() > 1) { + if(!PARSER_STATE->isTheoryEnabled(Smt2::THEORY_UF)) { + PARSER_STATE->parseError(std::string("Functions (of non-zero arity) cannot be declared in logic ") + PARSER_STATE->getLogic().getLogicString()); + } t = EXPR_MANAGER->mkFunctionType(sorts); } else { t = sorts[0]; @@ -524,6 +544,9 @@ extendedCommand[CVC4::Command*& cmd] sortList[sorts] RPAREN_TOK { Type t = EXPR_MANAGER->booleanType(); if(sorts.size() > 0) { + if(!PARSER_STATE->isTheoryEnabled(Smt2::THEORY_UF)) { + PARSER_STATE->parseError(std::string("Predicates (of non-zero arity) cannot be declared in logic ") + PARSER_STATE->getLogic().getLogicString()); + } t = EXPR_MANAGER->mkFunctionType(sorts, t); } Expr func = PARSER_STATE->mkVar(name, t); |