diff options
| author | Morgan Deters <mdeters@cs.nyu.edu> | 2014-06-08 17:54:50 -0400 |
|---|---|---|
| committer | Morgan Deters <mdeters@cs.nyu.edu> | 2014-06-08 17:54:50 -0400 |
| commit | aee4775c89adf56df6b9a177f3666d79899863dd (patch) | |
| tree | e6a238e5915e3636111d63a7ca4dfc140daeaff7 | |
| parent | cf13918f84ddeb228cb3ec7349deeea25f75b88b (diff) | |
Allow 'repeat' as an SMT-LIB user symbol name (UFNIA/vcc-havoc does this).
| -rw-r--r-- | src/parser/smt2/Smt2.g | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index b3761dfbd..39f746244 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' n=INTEGER_LITERAL + | ('repeat')=>'repeat' n=INTEGER_LITERAL { op = MK_CONST(BitVectorRepeat(AntlrInput::tokenToUnsigned($n))); } | 'zero_extend' n=INTEGER_LITERAL { op = MK_CONST(BitVectorZeroExtend(AntlrInput::tokenToUnsigned($n))); } @@ -1535,8 +1535,8 @@ symbolList[std::vector<std::string>& names, symbol[std::string& id, CVC4::parser::DeclarationCheck check, CVC4::parser::SymbolType type] - : SIMPLE_SYMBOL - { id = AntlrInput::tokenText($SIMPLE_SYMBOL); + : s=( SIMPLE_SYMBOL | 'repeat' ) + { id = AntlrInput::tokenText($s); if(!PARSER_STATE->isAbstractValue(id)) { // if an abstract value, SmtEngine handles declaration PARSER_STATE->checkDeclaration(id, check, type); |