diff options
| author | Morgan Deters <mdeters@cs.nyu.edu> | 2014-06-08 20:10:08 -0400 |
|---|---|---|
| committer | Morgan Deters <mdeters@cs.nyu.edu> | 2014-06-08 20:10:08 -0400 |
| commit | 751539f294fca0d039ccb748776c280e20cd9eab (patch) | |
| tree | 7808588cba82e0998f215249687b53d9521777d3 /src/parser | |
| parent | 7bf6c4aa1dabef2f3abd14124b16cbf1900cf3de (diff) | |
Previous "repeat" fix required extra lookahead (leading to assert-fails). Fixed, at the cost of an antlr warning that's safe to ignore for now.
Diffstat (limited to 'src/parser')
| -rw-r--r-- | src/parser/smt2/Smt2.g | 10 |
1 files changed, 7 insertions, 3 deletions
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 8fa047885..c857f3905 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -1206,7 +1206,7 @@ indexedFunctionName[CVC4::Expr& op] ( 'extract' n1=INTEGER_LITERAL n2=INTEGER_LITERAL { op = MK_CONST(BitVectorExtract(AntlrInput::tokenToUnsigned($n1), AntlrInput::tokenToUnsigned($n2))); } - | ('repeat')=>'repeat' n=INTEGER_LITERAL + | 'repeat' n=INTEGER_LITERAL { op = MK_CONST(BitVectorRepeat(AntlrInput::tokenToUnsigned($n))); } | 'zero_extend' n=INTEGER_LITERAL { op = MK_CONST(BitVectorZeroExtend(AntlrInput::tokenToUnsigned($n))); } @@ -1535,13 +1535,17 @@ symbolList[std::vector<std::string>& names, symbol[std::string& id, CVC4::parser::DeclarationCheck check, CVC4::parser::SymbolType type] - : s=( SIMPLE_SYMBOL | 'repeat' ) - { id = AntlrInput::tokenText($s); + : SIMPLE_SYMBOL + { id = AntlrInput::tokenText($SIMPLE_SYMBOL); if(!PARSER_STATE->isAbstractValue(id)) { // if an abstract value, SmtEngine handles declaration PARSER_STATE->checkDeclaration(id, check, type); } } + | 'repeat' + { id = "repeat"; + PARSER_STATE->checkDeclaration(id, check, type); + } | QUOTED_SYMBOL { id = AntlrInput::tokenText($QUOTED_SYMBOL); /* strip off the quotes */ |