From 5321d62fce6c747fa9d11e9df5b2ef8c4e25de21 Mon Sep 17 00:00:00 2001 From: Tim King Date: Thu, 20 May 2010 22:51:48 +0000 Subject: 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. --- src/parser/smt/Smt.g | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) (limited to 'src/parser/smt') 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; } -- cgit v1.2.3