diff options
| author | Morgan Deters <mdeters@cs.nyu.edu> | 2013-04-22 09:49:46 -0400 |
|---|---|---|
| committer | Morgan Deters <mdeters@cs.nyu.edu> | 2013-04-22 09:49:46 -0400 |
| commit | a006e7b92327668b76a1ab993007f42fe91052c3 (patch) | |
| tree | aeebe2fb9b11c9434e1c538c062aecbcae9037b5 /src/parser/smt1 | |
| parent | 8d56bb7184d573448fd16242afda2e4224e8641d (diff) | |
add bit0 and bit1 constants to smt-lib v1 parser
Diffstat (limited to 'src/parser/smt1')
| -rw-r--r-- | src/parser/smt1/Smt1.g | 11 |
1 files changed, 11 insertions, 0 deletions
diff --git a/src/parser/smt1/Smt1.g b/src/parser/smt1/Smt1.g index ee4e19689..bfcd8cd4d 100644 --- a/src/parser/smt1/Smt1.g +++ b/src/parser/smt1/Smt1.g @@ -313,6 +313,10 @@ annotatedFormula[CVC4::Expr& expr] expr = MK_CONST( AntlrInput::tokenToRational($RATIONAL_TOK) ); } | n = BITVECTOR_BV_CONST '[' size = NUMERAL_TOK ']' { expr = MK_CONST( AntlrInput::tokenToBitvector($n, $size) ); } + | n = BITVECTOR1_BV_CONST + { unsigned int bit = AntlrInput::tokenText($n)[3] - '0'; + expr = MK_CONST( BitVector(1, bit) ); + } // NOTE: Theory constants go here /* TODO: quantifiers, arithmetic constants */ @@ -745,6 +749,13 @@ BITVECTOR_BV_CONST : 'bv' DIGIT+ ; +/** + * Matches a bit-vector constant of the form bit(0|1) + */ +BITVECTOR1_BV_CONST + : 'bit0' | 'bit1' + ; + /** * Matches an identifier from the input. An identifier is a sequence of letters, |