diff options
Diffstat (limited to 'src/parser/smt2')
| -rw-r--r-- | src/parser/smt2/Smt2.g | 27 | ||||
| -rw-r--r-- | src/parser/smt2/smt2.cpp | 14 |
2 files changed, 26 insertions, 15 deletions
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 69b2eba76..56457d006 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -230,16 +230,16 @@ term[CVC4::Expr& expr] // TODO: check arity { expr = MK_EXPR(CVC4::kind::APPLY_UF,args); } - | /* An ite expression */ - LPAREN_TOK ITE_TOK - term[expr] - { args.push_back(expr); } - term[expr] - { args.push_back(expr); } - term[expr] - { args.push_back(expr); } - RPAREN_TOK - { expr = MK_EXPR(CVC4::kind::ITE, args); } + // | /* An ite expression */ + // LPAREN_TOK ITE_TOK + // term[expr] + // { args.push_back(expr); } + // term[expr] + // { args.push_back(expr); } + // term[expr] + // { args.push_back(expr); } + // RPAREN_TOK + // { expr = MK_EXPR(CVC4::kind::ITE, args); } | /* a let binding */ LPAREN_TOK LET_TOK LPAREN_TOK @@ -256,17 +256,18 @@ term[CVC4::Expr& expr] { expr = PARSER_STATE->getVariable(name); } /* constants */ -// | TRUE_TOK { expr = MK_CONST(true); } -// | FALSE_TOK { expr = MK_CONST(false); } | INTEGER_LITERAL { expr = MK_CONST( AntlrInput::tokenToInteger($INTEGER_LITERAL) ); } + | DECIMAL_LITERAL { // FIXME: This doesn't work because an SMT rational is not a valid GMP rational string expr = MK_CONST( AntlrInput::tokenToRational($DECIMAL_LITERAL) ); } + | HEX_LITERAL { Assert( AntlrInput::tokenText($HEX_LITERAL).find("#x") == 0 ); std::string hexString = AntlrInput::tokenTextSubstr($HEX_LITERAL,2); expr = MK_CONST( BitVector(hexString, 16) ); } + | BINARY_LITERAL { Assert( AntlrInput::tokenText($BINARY_LITERAL).find("#b") == 0 ); std::string binString = AntlrInput::tokenTextSubstr($BINARY_LITERAL,2); @@ -300,6 +301,7 @@ builtinOp[CVC4::Kind& kind] | XOR_TOK { $kind = CVC4::kind::XOR; } | EQUAL_TOK { $kind = CVC4::kind::EQUAL; } | DISTINCT_TOK { $kind = CVC4::kind::DISTINCT; } + | ITE_TOK { $kind = CVC4::kind::ITE; } | GREATER_THAN_TOK { $kind = CVC4::kind::GT; } | GREATER_THAN_TOK EQUAL_TOK @@ -310,7 +312,6 @@ builtinOp[CVC4::Kind& kind] { $kind = CVC4::kind::LT; } | PLUS_TOK { $kind = CVC4::kind::PLUS; } | 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; } diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index 34245669e..79d5ccb3a 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -128,17 +128,27 @@ void Smt2::setLogic(const std::string& name) { addTheory(THEORY_REALS); break; + case Smt::QF_UF: + addOperator(kind::APPLY_UF); + break; + case Smt::QF_UFIDL: addTheory(THEORY_INTS); - // falling-through on purpose, to add UF part of UFIDL + addOperator(kind::APPLY_UF); + break; - case Smt::QF_UF: + case Smt::QF_UFLIA: + case Smt::QF_UFLRA: + case Smt::QF_UFNRA: + addTheory(THEORY_REALS); addOperator(kind::APPLY_UF); break; case Smt::AUFLIA: case Smt::AUFLIRA: case Smt::AUFNIRA: + case Smt::LRA: + case Smt::UFNIA: case Smt::QF_AUFBV: case Smt::QF_AUFLIA: case Smt::QF_BV: |