diff options
| author | Morgan Deters <mdeters@gmail.com> | 2012-07-18 21:32:05 +0000 |
|---|---|---|
| committer | Morgan Deters <mdeters@gmail.com> | 2012-07-18 21:32:05 +0000 |
| commit | 06077433dd58f92a06e9539b6f17a551421141b4 (patch) | |
| tree | 65b52313a45361c66a51edc60b195761e5b4ea03 /src/parser/smt2/Smt2.g | |
| parent | ae2d100393355bea6e486013a184f32543cd3528 (diff) | |
more compliance fixes for SMT-LIBv2
Diffstat (limited to 'src/parser/smt2/Smt2.g')
| -rw-r--r-- | src/parser/smt2/Smt2.g | 7 |
1 files changed, 6 insertions, 1 deletions
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index bddb64c3c..be5a797bf 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -198,7 +198,9 @@ command returns [CVC4::Command* cmd = NULL] { cmd = new GetOptionCommand(AntlrInput::tokenText($KEYWORD)); } | /* sort declaration */ DECLARE_SORT_TOK { PARSER_STATE->checkThatLogicIsSet(); } - symbol[name,CHECK_UNDECLARED,SYM_SORT] n=INTEGER_LITERAL + symbol[name,CHECK_UNDECLARED,SYM_SORT] + { PARSER_STATE->checkUserSymbol(name); } + n=INTEGER_LITERAL { Debug("parser") << "declare sort: '" << name << "' arity=" << n << std::endl; unsigned arity = AntlrInput::tokenToUnsigned(n); @@ -213,6 +215,7 @@ command returns [CVC4::Command* cmd = NULL] | /* sort definition */ DEFINE_SORT_TOK { PARSER_STATE->checkThatLogicIsSet(); } symbol[name,CHECK_UNDECLARED,SYM_SORT] + { PARSER_STATE->checkUserSymbol(name); } LPAREN_TOK symbolList[names,CHECK_NONE,SYM_SORT] RPAREN_TOK { PARSER_STATE->pushScope(); @@ -233,6 +236,7 @@ command returns [CVC4::Command* cmd = NULL] | /* function declaration */ DECLARE_FUN_TOK { PARSER_STATE->checkThatLogicIsSet(); } symbol[name,CHECK_UNDECLARED,SYM_VARIABLE] + { PARSER_STATE->checkUserSymbol(name); } LPAREN_TOK sortList[sorts] RPAREN_TOK sortSymbol[t,CHECK_DECLARED] { Debug("parser") << "declare fun: '" << name << "'" << std::endl; @@ -244,6 +248,7 @@ command returns [CVC4::Command* cmd = NULL] | /* function definition */ DEFINE_FUN_TOK { PARSER_STATE->checkThatLogicIsSet(); } symbol[name,CHECK_UNDECLARED,SYM_VARIABLE] + { PARSER_STATE->checkUserSymbol(name); } LPAREN_TOK sortedVarList[sortedVarNames] RPAREN_TOK sortSymbol[t,CHECK_DECLARED] { /* add variables to parser state before parsing term */ |