From 27e1a5835139d5107010475cb951a1aa1350e7f4 Mon Sep 17 00:00:00 2001 From: Haniel Barbosa Date: Mon, 17 Feb 2020 13:11:17 -0300 Subject: Using ParseOp in TPTP (#3764) --- src/parser/tptp/Tptp.g | 462 +++++++++++++++++++++++++++++++---------------- src/parser/tptp/tptp.cpp | 192 ++++++++++++++++---- src/parser/tptp/tptp.h | 28 ++- 3 files changed, 491 insertions(+), 191 deletions(-) (limited to 'src/parser/tptp') diff --git a/src/parser/tptp/Tptp.g b/src/parser/tptp/Tptp.g index 54fba4d1b..bb9600061 100644 --- a/src/parser/tptp/Tptp.g +++ b/src/parser/tptp/Tptp.g @@ -88,6 +88,7 @@ using namespace CVC4::parser; #include #include "smt/command.h" +#include "parser/parse_op.h" #include "parser/parser.h" #include "parser/tptp/tptp.h" #include "parser/antlr_tracing.h" @@ -328,25 +329,40 @@ atomicFormula[CVC4::Expr& expr] std::string name; std::vector args; bool equal; + ParseOp p; } - : atomicWord[name] (LPAREN_TOK arguments[args] RPAREN_TOK)? + : atomicWord[p.d_name] (LPAREN_TOK arguments[args] RPAREN_TOK)? ( equalOp[equal] term[expr2] { // equality/disequality between terms - PARSER_STATE->makeApplication(expr, name, args, true); - expr = MK_EXPR(kind::EQUAL, expr, expr2); - if(!equal) expr = MK_EXPR(kind::NOT, expr); + expr = args.empty() ? PARSER_STATE->parseOpToExpr(p) + : PARSER_STATE->applyParseOp(p, args); + args.clear(); + args.push_back(expr); + args.push_back(expr2); + ParseOp p1(kind::EQUAL); + expr = PARSER_STATE->applyParseOp(p1, args); + if (!equal) + { + expr = MK_EXPR(kind::NOT, expr); + } } | { // predicate - PARSER_STATE->makeApplication(expr, name, args, false); + p.d_type = EXPR_MANAGER->booleanType(); + expr = args.empty() ? PARSER_STATE->parseOpToExpr(p) + : PARSER_STATE->applyParseOp(p, args); } ) - | definedFun[expr] + | definedFun[p] ( LPAREN_TOK arguments[args] RPAREN_TOK equalOp[equal] term[expr2] { - expr = EXPR_MANAGER->mkExpr(expr, args); - expr = MK_EXPR(kind::EQUAL, expr, expr2); + expr = PARSER_STATE->applyParseOp(p, args); + args.clear(); + args.push_back(expr); + args.push_back(expr2); + ParseOp p1(kind::EQUAL); + expr = PARSER_STATE->applyParseOp(p1, args); if (!equal) { expr = MK_EXPR(kind::NOT, expr); @@ -357,19 +373,21 @@ atomicFormula[CVC4::Expr& expr] ( equalOp[equal] term[expr2] { // equality/disequality between terms - expr = MK_EXPR(kind::EQUAL, expr, expr2); + args.push_back(expr); + args.push_back(expr2); + p.d_kind = kind::EQUAL; + expr = PARSER_STATE->applyParseOp(p, args); if (!equal) { expr = MK_EXPR(kind::NOT, expr); } } )? - | definedPred[expr] (LPAREN_TOK arguments[args] RPAREN_TOK)? + | definedPred[p] (LPAREN_TOK arguments[args] RPAREN_TOK)? { - if (!args.empty()) - { - expr = EXPR_MANAGER->mkExpr(expr, args); - } + p.d_type = EXPR_MANAGER->booleanType(); + expr = args.empty() ? PARSER_STATE->parseOpToExpr(p) + : PARSER_STATE->applyParseOp(p, args); } | definedProp[expr] ; @@ -380,18 +398,24 @@ thfAtomicFormula[CVC4::Expr& expr] std::string name; std::vector args; bool equal; + ParseOp p; } - : atomicWord[name] (LPAREN_TOK arguments[args] RPAREN_TOK)? + : atomicWord[p.d_name] (LPAREN_TOK arguments[args] RPAREN_TOK)? { - PARSER_STATE->makeApplication(expr, name, args, true); + expr = args.empty() ? PARSER_STATE->parseOpToExpr(p) + : PARSER_STATE->applyParseOp(p, args); } - | definedFun[expr] + | definedFun[p] ( LPAREN_TOK arguments[args] RPAREN_TOK equalOp[equal] term[expr2] { - expr = EXPR_MANAGER->mkExpr(expr, args); - expr = MK_EXPR(kind::EQUAL, expr, expr2); + expr = PARSER_STATE->applyParseOp(p, args); + args.clear(); + args.push_back(expr); + args.push_back(expr2); + ParseOp p1(kind::EQUAL); + expr = PARSER_STATE->applyParseOp(p1, args); if (!equal) { expr = MK_EXPR(kind::NOT, expr); @@ -401,12 +425,11 @@ thfAtomicFormula[CVC4::Expr& expr] | thfSimpleTerm[expr] | letTerm[expr] | conditionalTerm[expr] - | thfDefinedPred[expr] (LPAREN_TOK arguments[args] RPAREN_TOK)? + | thfDefinedPred[p] (LPAREN_TOK arguments[args] RPAREN_TOK)? { - if (!args.empty()) - { - expr = EXPR_MANAGER->mkExpr(expr, args); - } + p.d_type = EXPR_MANAGER->booleanType(); + expr = args.empty() ? PARSER_STATE->parseOpToExpr(p) + : PARSER_STATE->applyParseOp(p, args); } | definedProp[expr] ; @@ -419,42 +442,82 @@ definedProp[CVC4::Expr& expr] | FALSE_TOK { expr = MK_CONST(bool(false)); } ; -definedPred[CVC4::Expr& expr] - : '$less' { expr = EXPR_MANAGER->operatorOf(CVC4::kind::LT); } - | '$lesseq' { expr = EXPR_MANAGER->operatorOf(CVC4::kind::LEQ); } - | '$greater' { expr = EXPR_MANAGER->operatorOf(CVC4::kind::GT); } - | '$greatereq' { expr = EXPR_MANAGER->operatorOf(CVC4::kind::GEQ); } +definedPred[CVC4::ParseOp& p] + : '$less' + { + p.d_kind = kind::LT; + } + | '$lesseq' + { + p.d_kind = kind::LEQ; + } + | '$greater' + { + p.d_kind = kind::GT; + } + | '$greatereq' + { + p.d_kind = kind::GEQ; + } | '$is_rat' // a real n is a rational if there exists q,r integers such that // to_real(q) = n*to_real(r), // where r is non-zero. { Expr n = EXPR_MANAGER->mkBoundVar("N", EXPR_MANAGER->realType()); Expr q = EXPR_MANAGER->mkBoundVar("Q", EXPR_MANAGER->integerType()); - Expr qr = MK_EXPR(CVC4::kind::TO_REAL, q); + Expr qr = MK_EXPR(kind::TO_REAL, q); Expr r = EXPR_MANAGER->mkBoundVar("R", EXPR_MANAGER->integerType()); - Expr rr = MK_EXPR(CVC4::kind::TO_REAL, r); + Expr rr = MK_EXPR(kind::TO_REAL, r); Expr body = - MK_EXPR(CVC4::kind::AND, - MK_EXPR(CVC4::kind::NOT, - MK_EXPR(CVC4::kind::EQUAL, r, MK_CONST(Rational(0)))), - MK_EXPR(CVC4::kind::EQUAL, qr, MK_EXPR(CVC4::kind::MULT, n, rr))); - Expr bvl = MK_EXPR(CVC4::kind::BOUND_VAR_LIST, q, r); - body = MK_EXPR(CVC4::kind::EXISTS, bvl, body); - Expr lbvl = MK_EXPR(CVC4::kind::BOUND_VAR_LIST, n); - expr = MK_EXPR(CVC4::kind::LAMBDA, lbvl, body); - } - | '$is_int' { expr = EXPR_MANAGER->operatorOf(CVC4::kind::IS_INTEGER); } - | '$distinct' { expr = EXPR_MANAGER->operatorOf(CVC4::kind::DISTINCT); } - | AND_TOK { expr = EXPR_MANAGER->operatorOf(CVC4::kind::AND); } - | IMPLIES_TOK { expr = EXPR_MANAGER->operatorOf(CVC4::kind::IMPLIES); } - | OR_TOK { expr = EXPR_MANAGER->operatorOf(CVC4::kind::OR); } + MK_EXPR(kind::AND, + MK_EXPR(kind::NOT, + MK_EXPR(kind::EQUAL, r, MK_CONST(Rational(0)))), + MK_EXPR(kind::EQUAL, qr, MK_EXPR(kind::MULT, n, rr))); + Expr bvl = MK_EXPR(kind::BOUND_VAR_LIST, q, r); + body = MK_EXPR(kind::EXISTS, bvl, body); + Expr lbvl = MK_EXPR(kind::BOUND_VAR_LIST, n); + p.d_kind = kind::LAMBDA; + p.d_expr = MK_EXPR(kind::LAMBDA, lbvl, body); + } + | '$is_int' + { + p.d_kind = kind::IS_INTEGER; + } + | '$distinct' + { + p.d_kind = kind::DISTINCT; + } + | AND_TOK + { + p.d_kind = kind::AND; + } + | IMPLIES_TOK + { + p.d_kind = kind::IMPLIES; + } + | OR_TOK + { + p.d_kind = kind::OR; + } ; -thfDefinedPred[CVC4::Expr& expr] - : '$less' { expr = EXPR_MANAGER->operatorOf(CVC4::kind::LT); } - | '$lesseq' { expr = EXPR_MANAGER->operatorOf(CVC4::kind::LEQ); } - | '$greater' { expr = EXPR_MANAGER->operatorOf(CVC4::kind::GT); } - | '$greatereq' { expr = EXPR_MANAGER->operatorOf(CVC4::kind::GEQ); } +thfDefinedPred[CVC4::ParseOp& p] + : '$less' + { + p.d_kind = kind::LT; + } + | '$lesseq' + { + p.d_kind = kind::LEQ; + } + | '$greater' + { + p.d_kind = kind::GT; + } + | '$greatereq' + { + p.d_kind = kind::GEQ; + } | '$is_rat' // a real n is a rational if there exists q,r integers such that // to_real(q) = n*to_real(r), @@ -462,115 +525,199 @@ thfDefinedPred[CVC4::Expr& expr] { Expr n = EXPR_MANAGER->mkBoundVar("N", EXPR_MANAGER->realType()); Expr q = EXPR_MANAGER->mkBoundVar("Q", EXPR_MANAGER->integerType()); - Expr qr = MK_EXPR(CVC4::kind::TO_REAL, q); + Expr qr = MK_EXPR(kind::TO_REAL, q); Expr r = EXPR_MANAGER->mkBoundVar("R", EXPR_MANAGER->integerType()); - Expr rr = MK_EXPR(CVC4::kind::TO_REAL, r); + Expr rr = MK_EXPR(kind::TO_REAL, r); Expr body = MK_EXPR( - CVC4::kind::AND, - MK_EXPR(CVC4::kind::NOT, - MK_EXPR(CVC4::kind::EQUAL, r, MK_CONST(Rational(0)))), - MK_EXPR(CVC4::kind::EQUAL, qr, MK_EXPR(CVC4::kind::MULT, n, rr))); - Expr bvl = MK_EXPR(CVC4::kind::BOUND_VAR_LIST, q, r); - body = MK_EXPR(CVC4::kind::EXISTS, bvl, body); - Expr lbvl = MK_EXPR(CVC4::kind::BOUND_VAR_LIST, n); - expr = MK_EXPR(CVC4::kind::LAMBDA, lbvl, body); - } - | '$is_int' { expr = EXPR_MANAGER->operatorOf(CVC4::kind::IS_INTEGER); } - | '$distinct' { expr = EXPR_MANAGER->operatorOf(CVC4::kind::DISTINCT); } + kind::AND, + MK_EXPR(kind::NOT, + MK_EXPR(kind::EQUAL, r, MK_CONST(Rational(0)))), + MK_EXPR(kind::EQUAL, qr, MK_EXPR(kind::MULT, n, rr))); + Expr bvl = MK_EXPR(kind::BOUND_VAR_LIST, q, r); + body = MK_EXPR(kind::EXISTS, bvl, body); + Expr lbvl = MK_EXPR(kind::BOUND_VAR_LIST, n); + p.d_kind = kind::LAMBDA; + p.d_expr = MK_EXPR(kind::LAMBDA, lbvl, body); + } + | '$is_int' + { + p.d_kind = kind::IS_INTEGER; + } + | '$distinct' + { + p.d_kind = kind::DISTINCT; + } | LPAREN_TOK ( - AND_TOK { expr = EXPR_MANAGER->operatorOf(CVC4::kind::AND); } - | OR_TOK { expr = EXPR_MANAGER->operatorOf(CVC4::kind::OR); } - | IMPLIES_TOK { expr = EXPR_MANAGER->operatorOf(CVC4::kind::IMPLIES); } + AND_TOK + { + p.d_kind = kind::AND; + } + | OR_TOK + { + p.d_kind = kind::OR; + } + | IMPLIES_TOK + { + p.d_kind = kind::IMPLIES; + } ) RPAREN_TOK ; -definedFun[CVC4::Expr& expr] +definedFun[CVC4::ParseOp& p] @declarations { bool remainder = false; } - : '$uminus' { expr = EXPR_MANAGER->operatorOf(CVC4::kind::UMINUS); } - | '$sum' { expr = EXPR_MANAGER->operatorOf(CVC4::kind::PLUS); } - | '$difference' { expr = EXPR_MANAGER->operatorOf(CVC4::kind::MINUS); } - | '$product' { expr = EXPR_MANAGER->operatorOf(CVC4::kind::MULT); } - | '$quotient' { expr = EXPR_MANAGER->operatorOf(CVC4::kind::DIVISION_TOTAL); } + : '$uminus' + { + p.d_kind = kind::UMINUS; + } + | '$sum' + { + p.d_kind = kind::PLUS; + } + | '$difference' + { + p.d_kind = kind::MINUS; + } + | '$product' + { + p.d_kind = kind::MULT; + } + | '$quotient' + { + p.d_kind = kind::DIVISION_TOTAL; + } | ( '$quotient_e' { remainder = false; } | '$remainder_e' { remainder = true; } ) - { Expr n = EXPR_MANAGER->mkBoundVar("N", EXPR_MANAGER->realType()); + { + Expr n = EXPR_MANAGER->mkBoundVar("N", EXPR_MANAGER->realType()); Expr d = EXPR_MANAGER->mkBoundVar("D", EXPR_MANAGER->realType()); - Expr formals = MK_EXPR(CVC4::kind::BOUND_VAR_LIST, n, d); - expr = MK_EXPR(CVC4::kind::DIVISION_TOTAL, n, d); - expr = MK_EXPR(CVC4::kind::ITE, MK_EXPR(CVC4::kind::GEQ, d, MK_CONST(Rational(0))), - MK_EXPR(CVC4::kind::TO_INTEGER, expr), - MK_EXPR(CVC4::kind::UMINUS, MK_EXPR(CVC4::kind::TO_INTEGER, MK_EXPR(CVC4::kind::UMINUS, expr)))); - if(remainder) { - expr = MK_EXPR(CVC4::kind::TO_INTEGER, MK_EXPR(CVC4::kind::MINUS, n, MK_EXPR(CVC4::kind::MULT, expr, d))); + Expr formals = MK_EXPR(kind::BOUND_VAR_LIST, n, d); + Expr expr = MK_EXPR(kind::DIVISION_TOTAL, n, d); + expr = MK_EXPR(kind::ITE, + MK_EXPR(kind::GEQ, d, MK_CONST(Rational(0))), + MK_EXPR(kind::TO_INTEGER, expr), + MK_EXPR(kind::UMINUS, + MK_EXPR(kind::TO_INTEGER, + MK_EXPR(kind::UMINUS, expr)))); + if (remainder) + { + expr = MK_EXPR( + kind::TO_INTEGER, + MK_EXPR(kind::MINUS, n, MK_EXPR(kind::MULT, expr, d))); } - expr = MK_EXPR(CVC4::kind::LAMBDA, formals, expr); + p.d_kind = kind::LAMBDA; + p.d_expr = MK_EXPR(kind::LAMBDA, formals, expr); } | ( '$quotient_t' { remainder = false; } | '$remainder_t' { remainder = true; } ) - { Expr n = EXPR_MANAGER->mkBoundVar("N", EXPR_MANAGER->realType()); + { + Expr n = EXPR_MANAGER->mkBoundVar("N", EXPR_MANAGER->realType()); Expr d = EXPR_MANAGER->mkBoundVar("D", EXPR_MANAGER->realType()); - Expr formals = MK_EXPR(CVC4::kind::BOUND_VAR_LIST, n, d); - expr = MK_EXPR(CVC4::kind::DIVISION_TOTAL, n, d); - expr = MK_EXPR(CVC4::kind::ITE, MK_EXPR(CVC4::kind::GEQ, expr, MK_CONST(Rational(0))), - MK_EXPR(CVC4::kind::TO_INTEGER, expr), - MK_EXPR(CVC4::kind::UMINUS, MK_EXPR(CVC4::kind::TO_INTEGER, MK_EXPR(CVC4::kind::UMINUS, expr)))); - if(remainder) { - expr = MK_EXPR(CVC4::kind::TO_INTEGER, MK_EXPR(CVC4::kind::MINUS, n, MK_EXPR(CVC4::kind::MULT, expr, d))); + Expr formals = MK_EXPR(kind::BOUND_VAR_LIST, n, d); + Expr expr = MK_EXPR(kind::DIVISION_TOTAL, n, d); + expr = MK_EXPR(kind::ITE, + MK_EXPR(kind::GEQ, expr, MK_CONST(Rational(0))), + MK_EXPR(kind::TO_INTEGER, expr), + MK_EXPR(kind::UMINUS, + MK_EXPR(kind::TO_INTEGER, + MK_EXPR(kind::UMINUS, expr)))); + if (remainder) + { + expr = MK_EXPR( + kind::TO_INTEGER, + MK_EXPR(kind::MINUS, n, MK_EXPR(kind::MULT, expr, d))); } - expr = MK_EXPR(CVC4::kind::LAMBDA, formals, expr); + p.d_kind = kind::LAMBDA; + p.d_expr = MK_EXPR(kind::LAMBDA, formals, expr); } | ( '$quotient_f' { remainder = false; } | '$remainder_f' { remainder = true; } ) - { Expr n = EXPR_MANAGER->mkBoundVar("N", EXPR_MANAGER->realType()); + { + Expr n = EXPR_MANAGER->mkBoundVar("N", EXPR_MANAGER->realType()); Expr d = EXPR_MANAGER->mkBoundVar("D", EXPR_MANAGER->realType()); - Expr formals = MK_EXPR(CVC4::kind::BOUND_VAR_LIST, n, d); - expr = MK_EXPR(CVC4::kind::DIVISION_TOTAL, n, d); - expr = MK_EXPR(CVC4::kind::TO_INTEGER, expr); - if(remainder) { - expr = MK_EXPR(CVC4::kind::TO_INTEGER, MK_EXPR(CVC4::kind::MINUS, n, MK_EXPR(CVC4::kind::MULT, expr, d))); + Expr formals = MK_EXPR(kind::BOUND_VAR_LIST, n, d); + Expr expr = MK_EXPR(kind::DIVISION_TOTAL, n, d); + expr = MK_EXPR(kind::TO_INTEGER, expr); + if (remainder) + { + expr = MK_EXPR(kind::TO_INTEGER, + MK_EXPR(kind::MINUS, n, MK_EXPR(kind::MULT, expr, d))); } - expr = MK_EXPR(CVC4::kind::LAMBDA, formals, expr); + p.d_kind = kind::LAMBDA; + p.d_expr = MK_EXPR(kind::LAMBDA, formals, expr); + } + | '$floor' + { + p.d_kind = kind::TO_INTEGER; } - | '$floor' { expr = EXPR_MANAGER->operatorOf(CVC4::kind::TO_INTEGER); } | '$ceiling' - { Expr n = EXPR_MANAGER->mkBoundVar("N", EXPR_MANAGER->realType()); - Expr formals = MK_EXPR(CVC4::kind::BOUND_VAR_LIST, n); - expr = MK_EXPR(CVC4::kind::UMINUS, MK_EXPR(CVC4::kind::TO_INTEGER, MK_EXPR(CVC4::kind::UMINUS, n))); - expr = MK_EXPR(CVC4::kind::LAMBDA, formals, expr); + { + Expr n = EXPR_MANAGER->mkBoundVar("N", EXPR_MANAGER->realType()); + Expr formals = MK_EXPR(kind::BOUND_VAR_LIST, n); + Expr expr = MK_EXPR(kind::UMINUS, + MK_EXPR(kind::TO_INTEGER, MK_EXPR(kind::UMINUS, n))); + p.d_kind = kind::LAMBDA; + p.d_expr = MK_EXPR(kind::LAMBDA, formals, expr); } | '$truncate' - { Expr n = EXPR_MANAGER->mkBoundVar("N", EXPR_MANAGER->realType()); - Expr formals = MK_EXPR(CVC4::kind::BOUND_VAR_LIST, n); - expr = MK_EXPR(CVC4::kind::ITE, MK_EXPR(CVC4::kind::GEQ, n, MK_CONST(Rational(0))), - MK_EXPR(CVC4::kind::TO_INTEGER, n), - MK_EXPR(CVC4::kind::UMINUS, MK_EXPR(CVC4::kind::TO_INTEGER, MK_EXPR(CVC4::kind::UMINUS, n)))); - expr = MK_EXPR(CVC4::kind::LAMBDA, formals, expr); + { + Expr n = EXPR_MANAGER->mkBoundVar("N", EXPR_MANAGER->realType()); + Expr formals = MK_EXPR(kind::BOUND_VAR_LIST, n); + Expr expr = + MK_EXPR(kind::ITE, + MK_EXPR(kind::GEQ, n, MK_CONST(Rational(0))), + MK_EXPR(kind::TO_INTEGER, n), + MK_EXPR(kind::UMINUS, + MK_EXPR(kind::TO_INTEGER, MK_EXPR(kind::UMINUS, n)))); + p.d_kind = kind::LAMBDA; + p.d_expr = MK_EXPR(kind::LAMBDA, formals, expr); } | '$round' - { Expr n = EXPR_MANAGER->mkBoundVar("N", EXPR_MANAGER->realType()); - Expr formals = MK_EXPR(CVC4::kind::BOUND_VAR_LIST, n); - Expr decPart = MK_EXPR(CVC4::kind::MINUS, n, MK_EXPR(CVC4::kind::TO_INTEGER, n)); - expr = MK_EXPR(CVC4::kind::ITE, MK_EXPR(CVC4::kind::LT, decPart, MK_CONST(Rational(1, 2))), - // if decPart < 0.5, round down - MK_EXPR(CVC4::kind::TO_INTEGER, n), - MK_EXPR(CVC4::kind::ITE, MK_EXPR(CVC4::kind::GT, decPart, MK_CONST(Rational(1, 2))), - // if decPart > 0.5, round up - MK_EXPR(CVC4::kind::TO_INTEGER, MK_EXPR(CVC4::kind::PLUS, n, MK_CONST(Rational(1)))), - // if decPart == 0.5, round to nearest even integer: - // result is: to_int(n/2 + .5) * 2 - MK_EXPR(CVC4::kind::MULT, MK_EXPR(CVC4::kind::TO_INTEGER, MK_EXPR(CVC4::kind::PLUS, MK_EXPR(CVC4::kind::DIVISION_TOTAL, n, MK_CONST(Rational(2))), MK_CONST(Rational(1, 2)))), MK_CONST(Rational(2))))); - expr = MK_EXPR(CVC4::kind::LAMBDA, formals, expr); - } - | '$to_int' { expr = EXPR_MANAGER->operatorOf(CVC4::kind::TO_INTEGER); } - | '$to_rat' { expr = EXPR_MANAGER->operatorOf(CVC4::kind::TO_REAL); } - | '$to_real' { expr = EXPR_MANAGER->operatorOf(CVC4::kind::TO_REAL); } + { + Expr n = EXPR_MANAGER->mkBoundVar("N", EXPR_MANAGER->realType()); + Expr formals = MK_EXPR(kind::BOUND_VAR_LIST, n); + Expr decPart = MK_EXPR(kind::MINUS, n, MK_EXPR(kind::TO_INTEGER, n)); + Expr expr = MK_EXPR( + kind::ITE, + MK_EXPR(kind::LT, decPart, MK_CONST(Rational(1, 2))), + // if decPart < 0.5, round down + MK_EXPR(kind::TO_INTEGER, n), + MK_EXPR(kind::ITE, + MK_EXPR(kind::GT, decPart, MK_CONST(Rational(1, 2))), + // if decPart > 0.5, round up + MK_EXPR(kind::TO_INTEGER, + MK_EXPR(kind::PLUS, n, MK_CONST(Rational(1)))), + // if decPart == 0.5, round to nearest even integer: + // result is: to_int(n/2 + .5) * 2 + MK_EXPR(kind::MULT, + MK_EXPR(kind::TO_INTEGER, + MK_EXPR(kind::PLUS, + MK_EXPR(kind::DIVISION_TOTAL, + n, + MK_CONST(Rational(2))), + MK_CONST(Rational(1, 2)))), + MK_CONST(Rational(2))))); + p.d_kind = kind::LAMBDA; + p.d_expr = MK_EXPR(kind::LAMBDA, formals, expr); + } + | '$to_int' + { + p.d_kind = kind::TO_INTEGER; + } + | '$to_rat' + { + p.d_kind = kind::TO_REAL; + } + | '$to_real' + { + p.d_kind = kind::TO_REAL; + } ; //%----Pure CNF should not use $true or $false in problems, and use $false only @@ -628,11 +775,13 @@ thfSimpleTerm[CVC4::Expr& expr] functionTerm[CVC4::Expr& expr] @declarations { std::vector args; + ParseOp p; } : plainTerm[expr] - | definedFun[expr] LPAREN_TOK arguments[args] RPAREN_TOK - { expr = EXPR_MANAGER->mkExpr(expr, args); } -// | + | definedFun[p] LPAREN_TOK arguments[args] RPAREN_TOK + { + expr = PARSER_STATE->applyParseOp(p, args); + } ; conditionalTerm[CVC4::Expr& expr] @@ -640,17 +789,19 @@ conditionalTerm[CVC4::Expr& expr] CVC4::Expr expr2, expr3; } : '$ite_t' LPAREN_TOK tffLogicFormula[expr] COMMA_TOK term[expr2] COMMA_TOK term[expr3] RPAREN_TOK - { expr = EXPR_MANAGER->mkExpr(CVC4::kind::ITE, expr, expr2, expr3); } + { expr = EXPR_MANAGER->mkExpr(kind::ITE, expr, expr2, expr3); } ; plainTerm[CVC4::Expr& expr] @declarations { std::string name; std::vector args; + ParseOp p; } - : atomicWord[name] (LPAREN_TOK arguments[args] RPAREN_TOK)? + : atomicWord[p.d_name] (LPAREN_TOK arguments[args] RPAREN_TOK)? { - PARSER_STATE->makeApplication(expr,name,args,true); + expr = args.empty() ? PARSER_STATE->parseOpToExpr(p) + : PARSER_STATE->applyParseOp(p, args); } ; @@ -837,7 +988,7 @@ thfAtomTyping[CVC4::Command*& cmd] } else { - // as yet, it's undeclared + // as of yet, it's undeclared CVC4::Expr freshExpr; if (type.isFunction()) { @@ -883,7 +1034,10 @@ thfLogicFormula[CVC4::Expr& expr] { // TODO create whatever lambda } - expr = MK_EXPR(kind::EQUAL, expr, expr2); + args.push_back(expr); + args.push_back(expr2); + ParseOp p(kind::EQUAL); + expr = PARSER_STATE->applyParseOp(p, args); if (!equal) { expr = MK_EXPR(kind::NOT, expr); @@ -892,25 +1046,18 @@ thfLogicFormula[CVC4::Expr& expr] | // Non-associative: <=> <~> ~& ~| fofBinaryNonAssoc[na] thfUnitaryFormula[expr2] { - switch(na) { - case tptp::NA_IFF: - expr = MK_EXPR(kind::EQUAL,expr,expr2); - break; - case tptp::NA_REVIFF: - expr = MK_EXPR(kind::XOR,expr,expr2); - break; - case tptp::NA_IMPLIES: - expr = MK_EXPR(kind::IMPLIES,expr,expr2); - break; - case tptp::NA_REVIMPLIES: - expr = MK_EXPR(kind::IMPLIES,expr2,expr); - break; - case tptp::NA_REVOR: - expr = MK_EXPR(kind::NOT,MK_EXPR(kind::OR,expr,expr2)); - break; - case tptp::NA_REVAND: - expr = MK_EXPR(kind::NOT,MK_EXPR(kind::AND,expr,expr2)); - break; + switch (na) + { + case tptp::NA_IFF: expr = MK_EXPR(kind::EQUAL, expr, expr2); break; + case tptp::NA_REVIFF: expr = MK_EXPR(kind::XOR, expr, expr2); break; + case tptp::NA_IMPLIES: expr = MK_EXPR(kind::IMPLIES, expr, expr2); break; + case tptp::NA_REVIMPLIES: expr = MK_EXPR(kind::IMPLIES, expr2, expr); break; + case tptp::NA_REVOR: + expr = MK_EXPR(kind::NOT, MK_EXPR(kind::OR, expr, expr2)); + break; + case tptp::NA_REVAND: + expr = MK_EXPR(kind::NOT, MK_EXPR(kind::AND, expr, expr2)); + break; } } | // N-ary and & @@ -998,7 +1145,10 @@ thfUnitaryFormula[CVC4::Expr& expr] thfLogicFormula[expr] RPAREN_TOK | NOT_TOK - { expr = EXPR_MANAGER->operatorOf(CVC4::kind::NOT); } + { + ParseOp p(kind::NOT); + expr = PARSER_STATE->parseOpToExpr(p); + } (thfUnitaryFormula[expr2] { expr = MK_EXPR(expr,expr2); })? | // Quantified thfQuantifier[kind] @@ -1146,7 +1296,7 @@ tffUnitaryFormula[CVC4::Expr& expr] expr = MK_EXPR(kind, MK_EXPR(kind::BOUND_VAR_LIST, bv), expr); } | '$ite_f' LPAREN_TOK tffLogicFormula[expr] COMMA_TOK tffLogicFormula[lhs] COMMA_TOK tffLogicFormula[rhs] RPAREN_TOK - { expr = EXPR_MANAGER->mkExpr(CVC4::kind::ITE, expr, lhs, rhs); } + { expr = EXPR_MANAGER->mkExpr(kind::ITE, expr, lhs, rhs); } | '$let_tf' LPAREN_TOK { PARSER_STATE->pushScope(); } tffLetTermDefn[lhs, rhs] COMMA_TOK tffFormula[expr] @@ -1174,7 +1324,7 @@ tffLetTermDefn[CVC4::Expr& lhs, CVC4::Expr& rhs] tffLetTermBinding[std::vector& bvlist, CVC4::Expr& lhs, CVC4::Expr& rhs] : term[lhs] EQUAL_TOK term[rhs] { PARSER_STATE->checkLetBinding(bvlist, lhs, rhs, false); - rhs = MK_EXPR(CVC4::kind::LAMBDA, MK_EXPR(CVC4::kind::BOUND_VAR_LIST, lhs.getChildren()), rhs); + rhs = MK_EXPR(kind::LAMBDA, MK_EXPR(kind::BOUND_VAR_LIST, lhs.getChildren()), rhs); lhs = lhs.getOperator(); } | LPAREN_TOK tffLetTermBinding[bvlist, lhs, rhs] RPAREN_TOK @@ -1191,7 +1341,7 @@ tffLetFormulaDefn[CVC4::Expr& lhs, CVC4::Expr& rhs] tffLetFormulaBinding[std::vector& bvlist, CVC4::Expr& lhs, CVC4::Expr& rhs] : atomicFormula[lhs] IFF_TOK tffUnitaryFormula[rhs] { PARSER_STATE->checkLetBinding(bvlist, lhs, rhs, true); - rhs = MK_EXPR(CVC4::kind::LAMBDA, MK_EXPR(CVC4::kind::BOUND_VAR_LIST, lhs.getChildren()), rhs); + rhs = MK_EXPR(kind::LAMBDA, MK_EXPR(kind::BOUND_VAR_LIST, lhs.getChildren()), rhs); lhs = lhs.getOperator(); } | LPAREN_TOK tffLetFormulaBinding[bvlist, lhs, rhs] RPAREN_TOK diff --git a/src/parser/tptp/tptp.cpp b/src/parser/tptp/tptp.cpp index 694369429..71a3e4bee 100644 --- a/src/parser/tptp/tptp.cpp +++ b/src/parser/tptp/tptp.cpp @@ -22,6 +22,7 @@ #include "api/cvc4cpp.h" #include "expr/type.h" +#include "options/options.h" #include "parser/parser.h" // ANTLR defines these, which is really bad! @@ -214,6 +215,165 @@ void Tptp::checkLetBinding(const std::vector& bvlist, Expr lhs, Expr rhs, } } +Expr Tptp::parseOpToExpr(ParseOp& p) +{ + Expr expr; + if (!p.d_expr.isNull()) + { + return p.d_expr; + } + // if it has a kind, it's a builtin one + if (p.d_kind != kind::NULL_EXPR) + { + return getExprManager()->operatorOf(p.d_kind); + } + if (isDeclared(p.d_name)) + { // already appeared + expr = getVariable(p.d_name); + } + else + { + Type t = + p.d_type == getExprManager()->booleanType() ? p.d_type : d_unsorted; + expr = mkVar(p.d_name, t, ExprManager::VAR_FLAG_GLOBAL); // levelZero + preemptCommand(new DeclareFunctionCommand(p.d_name, expr, t)); + } + return expr; +} + +Expr Tptp::applyParseOp(ParseOp& p, std::vector& args) +{ + assert(!args.empty()); + bool isBuiltinOperator = false; + // the builtin kind of the overall return expression + Kind kind = kind::NULL_EXPR; + // First phase: process the operator + ExprManager* em = getExprManager(); + // If operator already defined, just build application + if (!p.d_expr.isNull()) + { + return em->mkExpr(p.d_expr, args); + } + // Otherwise piece operator together + if (p.d_kind == kind::NULL_EXPR) + { + // A non-built-in function application, get the expression + Expr v; + if (isDeclared(p.d_name)) + { // already appeared + v = getVariable(p.d_name); + } + else + { + std::vector sorts(args.size(), d_unsorted); + Type t = p.d_type == em->booleanType() ? p.d_type : d_unsorted; + t = getExprManager()->mkFunctionType(sorts, t); + v = mkVar(p.d_name, t, ExprManager::VAR_FLAG_GLOBAL); // levelZero + preemptCommand(new DeclareFunctionCommand(p.d_name, v, t)); + } + // args might be rationals, in which case we need to create + // distinct constants of the "unsorted" sort to represent them + for (size_t i = 0; i < args.size(); ++i) + { + if (args[i].getType().isReal() + && FunctionType(v.getType()).getArgTypes()[i] == d_unsorted) + { + args[i] = convertRatToUnsorted(args[i]); + } + } + assert(!v.isNull()); + checkFunctionLike(v); + kind = getKindForFunction(v); + args.insert(args.begin(), v); + } + else + { + kind = p.d_kind; + isBuiltinOperator = true; + } + assert(kind != kind::NULL_EXPR); + // Second phase: apply the arguments to the parse op + if (isBuiltinOperator) + { + if (!em->getOptions().getUfHo() + && (kind == kind::EQUAL || kind == kind::DISTINCT)) + { + // need --uf-ho if these operators are applied over function args + for (std::vector::iterator i = args.begin(); i != args.end(); ++i) + { + if ((*i).getType().isFunction()) + { + parseError( + "Cannot apply equalty to functions unless --uf-ho is set."); + } + } + } + if (args.size() > 2) + { + if (kind == kind::INTS_DIVISION || kind == kind::XOR + || kind == kind::MINUS || kind == kind::DIVISION) + { + // Builtin operators that are not tokenized, are left associative, + // but not internally variadic must set this. + return em->mkLeftAssociative(kind, args); + } + if (kind == kind::IMPLIES) + { + /* right-associative, but CVC4 internally only supports 2 args */ + return em->mkRightAssociative(kind, args); + } + if (kind == kind::EQUAL || kind == kind::LT || kind == kind::GT + || kind == kind::LEQ || kind == kind::GEQ) + { + /* "chainable", but CVC4 internally only supports 2 args */ + return em->mkExpr(em->mkConst(Chain(kind)), args); + } + } + + if (kind::isAssociative(kind) && args.size() > em->maxArity(kind)) + { + /* Special treatment for associative operators with lots of children + */ + return em->mkAssociative(kind, args); + } + if (!strictModeEnabled() && (kind == kind::AND || kind == kind::OR) + && args.size() == 1) + { + // Unary AND/OR can be replaced with the argument. + return args[0]; + } + if (kind == kind::MINUS && args.size() == 1) + { + return em->mkExpr(kind::UMINUS, args[0]); + } + checkOperator(kind, args.size()); + return em->mkExpr(kind, args); + } + + // check if partially applied function, in this case we use HO_APPLY + if (args.size() >= 2) + { + Type argt = args[0].getType(); + if (argt.isFunction()) + { + unsigned arity = static_cast(argt).getArity(); + if (args.size() - 1 < arity) + { + if (!em->getOptions().getUfHo()) + { + parseError("Cannot partially apply functions unless --uf-ho is set."); + } + Debug("parser") << "Partial application of " << args[0]; + Debug("parser") << " : #argTypes = " << arity; + Debug("parser") << ", #args = " << args.size() - 1 << std::endl; + // must curry the partial application + return em->mkLeftAssociative(kind::HO_APPLY, args); + } + } + } + return em->mkExpr(kind, args); +} + void Tptp::forceLogic(const std::string& logic) { Parser::forceLogic(logic); @@ -269,38 +429,6 @@ Expr Tptp::convertStrToUnsorted(std::string str) { return e; } -void Tptp::makeApplication(Expr& expr, std::string& name, - std::vector& args, bool term) { - if (args.empty()) { // Its a constant - if (isDeclared(name)) { // already appeared - expr = getVariable(name); - } else { - Type t = term ? d_unsorted : getExprManager()->booleanType(); - expr = mkVar(name, t, ExprManager::VAR_FLAG_GLOBAL); // levelZero - preemptCommand(new DeclareFunctionCommand(name, expr, t)); - } - } else { // Its an application - if (isDeclared(name)) { // already appeared - expr = getVariable(name); - } else { - std::vector sorts(args.size(), d_unsorted); - Type t = term ? d_unsorted : getExprManager()->booleanType(); - t = getExprManager()->mkFunctionType(sorts, t); - expr = mkVar(name, t, ExprManager::VAR_FLAG_GLOBAL); // levelZero - preemptCommand(new DeclareFunctionCommand(name, expr, t)); - } - // args might be rationals, in which case we need to create - // distinct constants of the "unsorted" sort to represent them - for (size_t i = 0; i < args.size(); ++i) { - if (args[i].getType().isReal() && - FunctionType(expr.getType()).getArgTypes()[i] == d_unsorted) { - args[i] = convertRatToUnsorted(args[i]); - } - } - expr = getExprManager()->mkExpr(kind::APPLY_UF, expr, args); - } -} - void Tptp::mkLambdaWrapper(Expr& expr, Type argType) { std::vector lvars; diff --git a/src/parser/tptp/tptp.h b/src/parser/tptp/tptp.h index 5b3ed0807..50ed0af8f 100644 --- a/src/parser/tptp/tptp.h +++ b/src/parser/tptp/tptp.h @@ -25,6 +25,7 @@ #include #include +#include "parser/parse_op.h" #include "parser/parser.h" #include "smt/command.h" #include "util/hash.h" @@ -102,9 +103,6 @@ class Tptp : public Parser { */ void addTheory(Theory theory); - void makeApplication(Expr& expr, std::string& name, std::vector& args, - bool term); - /** creates a lambda abstraction around expression * * Given an expression expr of type argType = t1...tn -> t, creates a lambda @@ -147,6 +145,30 @@ class Tptp : public Parser { /** Check a TPTP let binding for well-formedness. */ void checkLetBinding(const std::vector& bvlist, Expr lhs, Expr rhs, bool formula); + /** + * This converts a ParseOp to expression, assuming it is a standalone term. + * + * There are three cases in TPTP: either p already has an expression, in which + * case this function just returns it, or p has just a name or a builtin kind. + */ + Expr parseOpToExpr(ParseOp& p); + /** + * Apply parse operator to list of arguments, and return the resulting + * expression. + * + * args must not be empty (otherwise the above method should have been + * called). + * + * There are three cases in TPTP: either p already has an expression, in which + * case this function just applies it to the arguments, or p has + * just a name or a builtin kind, in which case the respective operator is + * built. + * + * Note that the case of uninterpreted functions in TPTP this need not have + * been previously declared, which leads to a more convoluted processing than + * what is necessary in parsing SMT-LIB. + */ + Expr applyParseOp(ParseOp& p, std::vector& args); private: void addArithmeticOperators(); -- cgit v1.2.3