diff options
| author | Tim King <taking@cs.nyu.edu> | 2010-05-20 22:51:48 +0000 |
|---|---|---|
| committer | Tim King <taking@cs.nyu.edu> | 2010-05-20 22:51:48 +0000 |
| commit | 5321d62fce6c747fa9d11e9df5b2ef8c4e25de21 (patch) | |
| tree | 87685c6a9f32d99f09de28a02fc80378a94b6ec9 /src/parser/smt | |
| parent | ff70395fd3dcde9f68eda1c6a8bd70e6491f7458 (diff) | |
Added the division symbol to the parser, and minimal support for it in TheoryArith. Also directly hacked in support for theoryOf() to work for equalities where the left hand is a variable of type real.
Diffstat (limited to 'src/parser/smt')
| -rw-r--r-- | src/parser/smt/Smt.g | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/src/parser/smt/Smt.g b/src/parser/smt/Smt.g index dde5d26eb..07dd3de5b 100644 --- a/src/parser/smt/Smt.g +++ b/src/parser/smt/Smt.g @@ -284,10 +284,11 @@ builtinOp[CVC4::Kind& kind] | STAR_TOK { $kind = CVC4::kind::MULT; } | TILDE_TOK { $kind = CVC4::kind::UMINUS; } | MINUS_TOK { $kind = CVC4::kind::MINUS; } + | DIV_TOK { $kind = CVC4::kind::DIVISION; } // Bit-vectors | CONCAT_TOK { $kind = CVC4::kind::BITVECTOR_CONCAT; } - | BVAND_TOK { $kind = CVC4::kind::BITVECTOR_AND; } - | BVOR_TOK { $kind = CVC4::kind::BITVECTOR_OR; } + | BVAND_TOK { $kind = CVC4::kind::BITVECTOR_AND; } + | BVOR_TOK { $kind = CVC4::kind::BITVECTOR_OR; } | BVXOR_TOK { $kind = CVC4::kind::BITVECTOR_XOR; } | BVNOT_TOK { $kind = CVC4::kind::BITVECTOR_NOT; } | BVNAND_TOK { $kind = CVC4::kind::BITVECTOR_NAND; } @@ -300,7 +301,7 @@ builtinOp[CVC4::Kind& kind] | BVNEG_TOK { $kind = CVC4::kind::BITVECTOR_NEG; } | BVUDIV_TOK { $kind = CVC4::kind::BITVECTOR_UDIV; } | BVUREM_TOK { $kind = CVC4::kind::BITVECTOR_UREM; } - | BVSDIV_TOK { $kind = CVC4::kind::BITVECTOR_SDIV; } + | BVSDIV_TOK { $kind = CVC4::kind::BITVECTOR_SDIV; } | BVSREM_TOK { $kind = CVC4::kind::BITVECTOR_SREM; } | BVSMOD_TOK { $kind = CVC4::kind::BITVECTOR_SMOD; } | BVSHL_TOK { $kind = CVC4::kind::BITVECTOR_SHL; } |