diff options
| author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2010-09-20 01:08:32 +0000 |
|---|---|---|
| committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2010-09-20 01:08:32 +0000 |
| commit | 1b30b256a0ec40ff431b83296bfe5aa0e099eb2e (patch) | |
| tree | 91fb063e9cfcf360d601e21a19996995576ece7d /src/parser/smt/Smt.g | |
| parent | 9eaf94708275337a4749b7ef2f44bf1c6746d8fc (diff) | |
bitvector rewriting for the core theory and testcases
Diffstat (limited to 'src/parser/smt/Smt.g')
| -rw-r--r-- | src/parser/smt/Smt.g | 24 |
1 files changed, 18 insertions, 6 deletions
diff --git a/src/parser/smt/Smt.g b/src/parser/smt/Smt.g index ecb3d39b6..55c158a6f 100644 --- a/src/parser/smt/Smt.g +++ b/src/parser/smt/Smt.g @@ -216,12 +216,6 @@ annotatedFormula[CVC4::Expr& expr] RPAREN_TOK { PARSER_STATE->popScope(); } - | /* a variable */ - ( identifier[name,CHECK_DECLARED,SYM_VARIABLE] - | let_identifier[name,CHECK_DECLARED] - | flet_identifier[name,CHECK_DECLARED] ) - { expr = PARSER_STATE->getVariable(name); } - /* constants */ | TRUE_TOK { expr = MK_CONST(true); } | FALSE_TOK { expr = MK_CONST(false); } @@ -230,8 +224,17 @@ annotatedFormula[CVC4::Expr& expr] | RATIONAL_TOK { // FIXME: This doesn't work because an SMT rational is not a valid GMP rational string expr = MK_CONST( AntlrInput::tokenToRational($RATIONAL_TOK) ); } + | n = BITVECTOR_BV_CONST '[' size = NUMERAL_TOK ']' + { expr = MK_CONST( AntlrInput::tokenToBitvector($n, $size) ); } // NOTE: Theory constants go here /* TODO: quantifiers, arithmetic constants */ + + | /* a variable */ + ( identifier[name,CHECK_DECLARED,SYM_VARIABLE] + | let_identifier[name,CHECK_DECLARED] + | flet_identifier[name,CHECK_DECLARED] ) + { expr = PARSER_STATE->getVariable(name); } + ; /** @@ -553,6 +556,7 @@ XOR_TOK : 'xor'; // Bitvector tokens BITVECTOR_TOK : 'BitVec'; +BV_TOK : 'bv'; CONCAT_TOK : 'concat'; EXTRACT_TOK : 'extract'; BVAND_TOK : 'bvand'; @@ -590,6 +594,14 @@ ROTATE_LEFT_TOK : 'rotate_left'; ROTATE_RIGHT_TOK : 'rotate_right'; /** + * Mathces a bit-vector constant of the form bv123 + */ +BITVECTOR_BV_CONST + : 'bv' DIGIT+ + ; + + +/** * Matches an identifier from the input. An identifier is a sequence of letters, * digits and "_", "'", "." symbols, starting with a letter. */ |