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/smt2 | |
parent | 4de93c75eb2e4d724c5c19749c81df92bde55154 (diff) |
Adding array select/store to SMT v1 and v2 parsers
Diffstat (limited to 'src/parser/smt2')
-rw-r--r-- | src/parser/smt2/Smt2.g | 4 | ||||
-rw-r--r-- | src/parser/smt2/smt2.cpp | 13 |
2 files changed, 16 insertions, 1 deletions
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 37612901e..0abc4c4c6 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -312,6 +312,8 @@ builtinOp[CVC4::Kind& kind] | STAR_TOK { $kind = CVC4::kind::MULT; } | TILDE_TOK { $kind = CVC4::kind::UMINUS; } | MINUS_TOK { $kind = CVC4::kind::MINUS; } + | SELECT_TOK { $kind = CVC4::kind::SELECT; } + | STORE_TOK { $kind = CVC4::kind::STORE; } // NOTE: Theory operators go here ; @@ -421,7 +423,9 @@ PERCENT_TOK : '%'; PIPE_TOK : '|'; PLUS_TOK : '+'; POUND_TOK : '#'; +SELECT_TOK : 'select'; STAR_TOK : '*'; +STORE_TOK : 'store'; TILDE_TOK : '~'; XOR_TOK : 'xor'; diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index 871262b43..34245669e 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -64,6 +64,14 @@ void Smt2::addTheory(Theory theory) { addOperator(kind::XOR); break; + case THEORY_ARRAYS: + // FIXME: should define a paramterized type 'Array' with 2 arguments + mkSort("Array"); + + addOperator(kind::SELECT); + addOperator(kind::STORE); + break; + case THEORY_REALS_INTS: defineType("Real", getExprManager()->realType()); // falling-through on purpose, to add Ints part of RealsInts @@ -105,6 +113,10 @@ void Smt2::setLogic(const std::string& name) { /* No extra symbols necessary */ break; + case Smt::QF_AX: + addTheory(THEORY_ARRAYS); + break; + case Smt::QF_IDL: case Smt::QF_LIA: case Smt::QF_NIA: @@ -129,7 +141,6 @@ void Smt2::setLogic(const std::string& name) { case Smt::AUFNIRA: case Smt::QF_AUFBV: case Smt::QF_AUFLIA: - case Smt::QF_AX: case Smt::QF_BV: Unhandled(name); } |