diff options
| author | Kshitij Bansal <kshitij@cs.nyu.edu> | 2015-04-15 23:31:07 -0400 |
|---|---|---|
| committer | Kshitij Bansal <kshitij@cs.nyu.edu> | 2015-04-15 23:31:07 -0400 |
| commit | 7d00e71793a0af9b5eef1951ed3208863db90855 (patch) | |
| tree | 5f2f0c137bbf15662434a7a0b804ebcadd489e4a /src/parser | |
| parent | 2df5b1632d48df1d526bb14ea31f3cb84defb5a6 (diff) | |
THEORY_REAL_INTS parser changes
Diffstat (limited to 'src/parser')
| -rw-r--r-- | src/parser/smt2/Smt2.g | 7 | ||||
| -rw-r--r-- | src/parser/smt2/smt2.cpp | 6 |
2 files changed, 4 insertions, 9 deletions
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index dfbb79d72..13455506c 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -2040,9 +2040,6 @@ builtinOp[CVC4::Kind& kind] | INTS_DIV_TOK { $kind = CVC4::kind::INTS_DIVISION; } | INTS_MOD_TOK { $kind = CVC4::kind::INTS_MODULUS; } | ABS_TOK { $kind = CVC4::kind::ABS; } - | IS_INT_TOK { $kind = CVC4::kind::IS_INTEGER; } - | TO_INT_TOK { $kind = CVC4::kind::TO_INTEGER; } - | TO_REAL_TOK { $kind = CVC4::kind::TO_REAL; } | BV2NAT_TOK { $kind = CVC4::kind::BITVECTOR_TO_NAT; if(PARSER_STATE->strictModeEnabled()) { @@ -2462,7 +2459,6 @@ FORALL_TOK : 'forall'; GREATER_THAN_TOK : '>'; GREATER_THAN_EQUAL_TOK : '>='; IMPLIES_TOK : '=>'; -IS_INT_TOK : 'is_int'; LESS_THAN_TOK : '<'; LESS_THAN_EQUAL_TOK : '<='; MINUS_TOK : '-'; @@ -2473,10 +2469,9 @@ PLUS_TOK : '+'; //POUND_TOK : '#'; STAR_TOK : '*'; // TILDE_TOK : '~'; -TO_INT_TOK : 'to_int'; -TO_REAL_TOK : 'to_real'; XOR_TOK : 'xor'; + INTS_DIV_TOK : 'div'; INTS_MOD_TOK : 'mod'; ABS_TOK : 'abs'; diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index a782bf1ba..73a5124e0 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -161,9 +161,9 @@ void Smt2::addTheory(Theory theory) { case THEORY_REALS_INTS: defineType("Real", getExprManager()->realType()); Parser::addOperator(kind::DIVISION); - Parser::addOperator(kind::TO_INTEGER); - Parser::addOperator(kind::IS_INTEGER); - Parser::addOperator(kind::TO_REAL); + addOperator(kind::TO_INTEGER, "to_int"); + addOperator(kind::IS_INTEGER, "is_int"); + addOperator(kind::TO_REAL, "to_real"); // falling through on purpose, to add Ints part of Reals_Ints case THEORY_INTS: defineType("Int", getExprManager()->integerType()); |