diff options
| author | Christopher L. Conway <christopherleeconway@gmail.com> | 2010-06-14 20:45:11 +0000 |
|---|---|---|
| committer | Christopher L. Conway <christopherleeconway@gmail.com> | 2010-06-14 20:45:11 +0000 |
| commit | 41bb6f0c0c4eed4011793bdb802dac68c1e73b04 (patch) | |
| tree | b8fe406381d9020054eba477b122e45e7fa52d05 /src/parser/smt/Smt.g | |
| parent | 4de93c75eb2e4d724c5c19749c81df92bde55154 (diff) | |
Adding array select/store to SMT v1 and v2 parsers
Diffstat (limited to 'src/parser/smt/Smt.g')
| -rw-r--r-- | src/parser/smt/Smt.g | 8 |
1 files changed, 6 insertions, 2 deletions
diff --git a/src/parser/smt/Smt.g b/src/parser/smt/Smt.g index 4247dba7a..575f691a5 100644 --- a/src/parser/smt/Smt.g +++ b/src/parser/smt/Smt.g @@ -261,7 +261,7 @@ builtinOp[CVC4::Kind& kind] | IFF_TOK { $kind = CVC4::kind::IFF; } | EQUAL_TOK { $kind = CVC4::kind::EQUAL; } | DISTINCT_TOK { $kind = CVC4::kind::DISTINCT; } - // NOTE: Theory operators go here + // Arithmetic | GREATER_THAN_TOK { $kind = CVC4::kind::GT; } | GREATER_THAN_TOK EQUAL_TOK @@ -305,7 +305,9 @@ builtinOp[CVC4::Kind& kind] | BVSLE_TOK { $kind = CVC4::kind::BITVECTOR_SLE; } | BVSGT_TOK { $kind = CVC4::kind::BITVECTOR_SGT; } | BVSGE_TOK { $kind = CVC4::kind::BITVECTOR_SGE; } - /* TODO: lt, gt, plus, minus, etc. */ + // NOTE: Theory operators go here + | SELECT_TOK { $kind = CVC4::kind::SELECT; } + | STORE_TOK { $kind = CVC4::kind::STORE; } ; /** @@ -542,7 +544,9 @@ PERCENT_TOK : '%'; PIPE_TOK : '|'; PLUS_TOK : '+'; POUND_TOK : '#'; +SELECT_TOK : 'select'; STAR_TOK : '*'; +STORE_TOK : 'store'; TILDE_TOK : '~'; XOR_TOK : 'xor'; |