From cc9a1b02cb8b1920c2a16825b3ff58acdef4dce8 Mon Sep 17 00:00:00 2001 From: Haniel Barbosa Date: Thu, 27 Feb 2020 19:34:42 -0300 Subject: [PATCH] Changing TPTP parser to accomodate new API (#3837) Removing dependency of kinds corresponding to expressions. --- src/parser/tptp/Tptp.g | 291 +++++++++++++++++++++++++++------------ src/parser/tptp/tptp.cpp | 46 ++++--- src/parser/tptp/tptp.h | 8 +- 3 files changed, 228 insertions(+), 117 deletions(-) diff --git a/src/parser/tptp/Tptp.g b/src/parser/tptp/Tptp.g index bb9600061..c4b4ddbc0 100644 --- a/src/parser/tptp/Tptp.g +++ b/src/parser/tptp/Tptp.g @@ -148,6 +148,7 @@ parseCommand returns [CVC4::Command* cmd = NULL] Expr expr; Tptp::FormulaRole fr; std::string name, inclSymbol; + ParseOp p; } : CNF_TOK LPAREN_TOK nameN[name] COMMA_TOK formulaRole[fr] COMMA_TOK { PARSER_STATE->setCnf(true); @@ -209,9 +210,14 @@ parseCommand returns [CVC4::Command* cmd = NULL] ( TYPE_TOK COMMA_TOK thfAtomTyping[cmd] | formulaRole[fr] COMMA_TOK { PARSER_STATE->setCnf(false); PARSER_STATE->setFof(false); } - thfLogicFormula[expr] (COMMA_TOK anything*)? + thfLogicFormula[p] (COMMA_TOK anything*)? { - Expr aexpr = PARSER_STATE->getAssertionExpr(fr,expr); + if (p.d_expr.isNull()) + { + PARSER_STATE->parseError("Top level expression must be a formula"); + } + expr = p.d_expr; + Expr aexpr = PARSER_STATE->getAssertionExpr(fr, expr); if (!aexpr.isNull()) { // set the expression name (e.g. used with unsat core printing) @@ -220,7 +226,8 @@ parseCommand returns [CVC4::Command* cmd = NULL] PARSER_STATE->preemptCommand(csen); } // make the command to assert the formula - cmd = PARSER_STATE->makeAssertCommand(fr, aexpr, /* cnf == */ false, true); + cmd = PARSER_STATE->makeAssertCommand( + fr, aexpr, /* cnf == */ false, true); } ) RPAREN_TOK DOT_TOK | INCLUDE_TOK LPAREN_TOK unquotedFileName[name] @@ -368,7 +375,7 @@ atomicFormula[CVC4::Expr& expr] expr = MK_EXPR(kind::NOT, expr); } } - )? + ) | (simpleTerm[expr] | letTerm[expr] | conditionalTerm[expr]) ( equalOp[equal] term[expr2] @@ -383,55 +390,55 @@ atomicFormula[CVC4::Expr& expr] } } )? - | definedPred[p] (LPAREN_TOK arguments[args] RPAREN_TOK)? + | definedPred[p] (LPAREN_TOK arguments[args] RPAREN_TOK) { p.d_type = EXPR_MANAGER->booleanType(); - expr = args.empty() ? PARSER_STATE->parseOpToExpr(p) - : PARSER_STATE->applyParseOp(p, args); + expr = PARSER_STATE->applyParseOp(p, args); } | definedProp[expr] ; -thfAtomicFormula[CVC4::Expr& expr] +thfAtomicFormula[CVC4::ParseOp& p] @declarations { Expr expr2; std::string name; std::vector args; bool equal; - ParseOp p; } : atomicWord[p.d_name] (LPAREN_TOK arguments[args] RPAREN_TOK)? { - expr = args.empty() ? PARSER_STATE->parseOpToExpr(p) - : PARSER_STATE->applyParseOp(p, args); + p.d_expr = args.empty() ? PARSER_STATE->parseOpToExpr(p) + : PARSER_STATE->applyParseOp(p, args); } | definedFun[p] ( LPAREN_TOK arguments[args] RPAREN_TOK equalOp[equal] term[expr2] { - expr = PARSER_STATE->applyParseOp(p, args); + p.d_expr = PARSER_STATE->applyParseOp(p, args); args.clear(); - args.push_back(expr); + args.push_back(p.d_expr); args.push_back(expr2); ParseOp p1(kind::EQUAL); - expr = PARSER_STATE->applyParseOp(p1, args); + p.d_expr = PARSER_STATE->applyParseOp(p1, args); if (!equal) { - expr = MK_EXPR(kind::NOT, expr); + p.d_expr = MK_EXPR(kind::NOT, p.d_expr); } } )? - | thfSimpleTerm[expr] - | letTerm[expr] - | conditionalTerm[expr] + | thfSimpleTerm[p.d_expr] + | letTerm[p.d_expr] + | conditionalTerm[p.d_expr] | thfDefinedPred[p] (LPAREN_TOK arguments[args] RPAREN_TOK)? { p.d_type = EXPR_MANAGER->booleanType(); - expr = args.empty() ? PARSER_STATE->parseOpToExpr(p) - : PARSER_STATE->applyParseOp(p, args); + if (!args.empty()) + { + p.d_expr = PARSER_STATE->applyParseOp(p, args); + } } - | definedProp[expr] + | definedProp[p.d_expr] ; //%----Using removes a reduce/reduce ambiguity in lex/yacc. @@ -463,7 +470,8 @@ definedPred[CVC4::ParseOp& p] // 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 n = EXPR_MANAGER->mkBoundVar("N", EXPR_MANAGER->realType()); Expr q = EXPR_MANAGER->mkBoundVar("Q", EXPR_MANAGER->integerType()); Expr qr = MK_EXPR(kind::TO_REAL, q); Expr r = EXPR_MANAGER->mkBoundVar("R", EXPR_MANAGER->integerType()); @@ -1004,74 +1012,126 @@ thfAtomTyping[CVC4::Command*& cmd] ) ; -thfLogicFormula[CVC4::Expr& expr] +thfLogicFormula[CVC4::ParseOp& p] @declarations { tptp::NonAssoc na; - std::vector< Expr > args; + std::vector args; + std::vector p_args; Expr expr2; bool equal; + ParseOp p1; } //prefix unary formula case // ~ - : thfUnitaryFormula[expr] + : thfUnitaryFormula[p] ( // Equality: = equalOp[equal] - thfUnitaryFormula[expr2] + thfUnitaryFormula[p1] { - if (expr.getKind() == kind::BUILTIN && expr2.getKind() != kind::BUILTIN) + if (p.d_expr.isNull() && !p1.d_expr.isNull()) { - // make expr with a lambda of the same type as expr - PARSER_STATE->mkLambdaWrapper(expr, expr2.getType()); + // make p.d_expr with a lambda of the same type as p1.d_expr + p.d_expr = + PARSER_STATE->mkLambdaWrapper(p.d_kind, p1.d_expr.getType()); } - else if (expr2.getKind() == kind::BUILTIN - && expr.getKind() != kind::BUILTIN) + else if (p1.d_expr.isNull() && !p.d_expr.isNull()) { - // make expr2 with a lambda of the same type as expr - PARSER_STATE->mkLambdaWrapper(expr2, expr.getType()); + // make p1.d_expr with a lambda of the same type as p.d_expr + p1.d_expr = + PARSER_STATE->mkLambdaWrapper(p1.d_kind, p.d_expr.getType()); } - else if (expr.getKind() == kind::BUILTIN - && expr2.getKind() == kind::BUILTIN) + else if (p.d_expr.isNull() && p1.d_expr.isNull()) { - // TODO create whatever lambda + // Without a reference type it's not possible in general to know what + // the lambda wrapping should be, so we fail in these cases + UNSUPPORTED("Equality between theory functions"); } - args.push_back(expr); - args.push_back(expr2); - ParseOp p(kind::EQUAL); - expr = PARSER_STATE->applyParseOp(p, args); + args.push_back(p.d_expr); + args.push_back(p1.d_expr); + p.d_expr = MK_EXPR(kind::EQUAL, args); if (!equal) { - expr = MK_EXPR(kind::NOT, expr); + p.d_expr = MK_EXPR(kind::NOT, p.d_expr); } } | // Non-associative: <=> <~> ~& ~| - fofBinaryNonAssoc[na] thfUnitaryFormula[expr2] + fofBinaryNonAssoc[na] thfUnitaryFormula[p1] { + if (p.d_expr.isNull() || p1.d_expr.isNull()) + { + PARSER_STATE->parseError( + "Non-associative operator must be applied to formulas"); + } 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_IFF: + p.d_expr = MK_EXPR(kind::EQUAL, p.d_expr, p1.d_expr); + break; + case tptp::NA_REVIFF: + p.d_expr = MK_EXPR(kind::XOR, p.d_expr, p1.d_expr); + break; + case tptp::NA_IMPLIES: + p.d_expr = MK_EXPR(kind::IMPLIES, p.d_expr, p1.d_expr); + break; + case tptp::NA_REVIMPLIES: + p.d_expr = MK_EXPR(kind::IMPLIES, p1.d_expr, p.d_expr); + break; case tptp::NA_REVOR: - expr = MK_EXPR(kind::NOT, MK_EXPR(kind::OR, expr, expr2)); + p.d_expr = + MK_EXPR(kind::NOT, MK_EXPR(kind::OR, p.d_expr, p1.d_expr)); break; case tptp::NA_REVAND: - expr = MK_EXPR(kind::NOT, MK_EXPR(kind::AND, expr, expr2)); + p.d_expr = + MK_EXPR(kind::NOT, MK_EXPR(kind::AND, p.d_expr, p1.d_expr)); break; } } | // N-ary and & - ( { args.push_back(expr); } - ( AND_TOK thfUnitaryFormula[expr] { args.push_back(expr); } )+ + ( + { + if (p.d_expr.isNull()) + { + PARSER_STATE->parseError("AND must be applied to a formula"); + } + args.push_back(p.d_expr); + p = ParseOp(); + } + ( AND_TOK thfUnitaryFormula[p] + { + if (p.d_expr.isNull()) + { + PARSER_STATE->parseError("AND must be applied to a formula"); + } + args.push_back(p.d_expr); + p = ParseOp(); + } + )+ { - expr = MK_EXPR_ASSOCIATIVE(kind::AND, args); + p.d_expr = MK_EXPR_ASSOCIATIVE(kind::AND, args); } ) | // N-ary or | - ( { args.push_back(expr); } - ( OR_TOK thfUnitaryFormula[expr] { args.push_back(expr); } )+ + ( + { + if (p.d_expr.isNull()) + { + PARSER_STATE->parseError("OR must be applied to a formula"); + } + args.push_back(p.d_expr); + p = ParseOp(); + } + ( OR_TOK thfUnitaryFormula[p] + { + if (p.d_expr.isNull()) + { + PARSER_STATE->parseError("OR must be applied to a formula"); + } + args.push_back(p.d_expr); + p = ParseOp(); + } + )+ { - expr = MK_EXPR_ASSOCIATIVE(kind::OR, args); + p.d_expr = MK_EXPR_ASSOCIATIVE(kind::OR, args); } ) | // N-ary @ | @@ -1080,10 +1140,17 @@ thfLogicFormula[CVC4::Expr& expr] // ^ [X] : ^ [Y] : f @ g (where f is a and g is a // ) should be parsed as: (^ [X] : (^ [Y] : f)) @ g. // That is, g is not in the scope of either lambda. - { args.push_back(expr); } + { + p_args.push_back(p); + p = ParseOp(); + } ( APP_TOK ( - thfUnitaryFormula[expr] { args.push_back(expr); } + thfUnitaryFormula[p] + { + p_args.push_back(p); + p = ParseOp(); + } | LBRACK_TOK { UNSUPPORTED("Tuple terms"); } thfTupleForm[args] @@ -1091,32 +1158,45 @@ thfLogicFormula[CVC4::Expr& expr] ) )+ { - expr = args[0]; - // also add case for total applications - if (expr.getKind() == kind::BUILTIN) + if (p_args[0].d_expr.isNull()) { - args.erase(args.begin()); - expr = EXPR_MANAGER->mkExpr(expr, args); + for (unsigned i = 1, size = p_args.size(); i < size; ++i) + { + if (p_args[i].d_expr.isNull()) + { + PARSER_STATE->parseError( + "Application chains with defined symbol heads and at least " + "one defined symbol as argument are unsupported."); + } + args.push_back(p_args[i].d_expr); + } + p.d_expr = PARSER_STATE->applyParseOp(p_args[0], args); } else { - // check if any argument is a bultin node, e.g. "~", and create a + p.d_expr = p_args[0].d_expr; + // check if any argument is a defined function, e.g. "~", and create a // lambda wrapper then, e.g. (\lambda x. ~ x) - for (unsigned i = 1; i < args.size(); ++i) + for (unsigned i = 1, size = p_args.size(); i < size; ++i) { - // create a lambda wrapper, e.g. (\lambda x. ~ x) - if (args[i].getKind() != kind::BUILTIN) + if (!p_args[i].d_expr.isNull()) { + args.push_back(p_args[i].d_expr); continue; } - PARSER_STATE->mkLambdaWrapper( - args[i], - (static_cast(args[0].getType())) - .getArgTypes()[i - 1]); + // create a lambda wrapper, e.g. (\lambda x. ~ x). + // + // The type is determined by the first element of the application + // chain, which must be a function of type t1...tn -> t, so the + // lambda must have type ti + args.push_back(PARSER_STATE->mkLambdaWrapper( + p_args[i].d_kind, + (static_cast(p.d_expr.getType())) + .getArgTypes()[i - 1])); } - for (unsigned i = 1; i < args.size(); ++i) + for (unsigned i = 0, size = args.size(); i < size; ++i) { - expr = MK_EXPR(kind::HO_APPLY, expr, args[i]); + p.d_expr = MK_EXPR(kind::HO_APPLY, p.d_expr, args[i]); } } } @@ -1125,48 +1205,77 @@ thfLogicFormula[CVC4::Expr& expr] thfTupleForm[std::vector& args] @declarations { - Expr expr; + ParseOp p; } - : thfUnitaryFormula[expr] - { args.push_back(expr); } - ( COMMA_TOK thfUnitaryFormula[expr] { args.push_back(expr); } )+ + : thfUnitaryFormula[p] + { + if (p.d_expr.isNull()) + { + PARSER_STATE->parseError("TUPLE element must be a formula"); + } + args.push_back(p.d_expr); + } + ( COMMA_TOK thfUnitaryFormula[p] + { + if (p.d_expr.isNull()) + { + PARSER_STATE->parseError("TUPLE element must be a formula"); + } + args.push_back(p.d_expr); + } + )+ ; -thfUnitaryFormula[CVC4::Expr& expr] +thfUnitaryFormula[CVC4::ParseOp& p] @declarations { Kind kind; std::vector< Expr > bv; - Expr expr2; + Expr expr; bool equal; + ParseOp p1; } - : variable[expr] - | thfAtomicFormula[expr] + : variable[p.d_expr] + | thfAtomicFormula[p] | LPAREN_TOK - thfLogicFormula[expr] + thfLogicFormula[p] RPAREN_TOK | NOT_TOK { - ParseOp p(kind::NOT); - expr = PARSER_STATE->parseOpToExpr(p); + p.d_kind = kind::NOT; } - (thfUnitaryFormula[expr2] { expr = MK_EXPR(expr,expr2); })? + ( + thfUnitaryFormula[p1] + { + if (p1.d_expr.isNull()) + { + PARSER_STATE->parseError("NOT must be applied to a formula"); + } + std::vector args{p1.d_expr}; + p.d_expr = PARSER_STATE->applyParseOp(p, args); + } + )? | // Quantified - thfQuantifier[kind] + thfQuantifier[p.d_kind] LBRACK_TOK {PARSER_STATE->pushScope();} thfBindVariable[expr] { bv.push_back(expr); } ( COMMA_TOK thfBindVariable[expr] - { - bv.push_back(expr); - } - )* + { + bv.push_back(expr); + } + )* RBRACK_TOK COLON_TOK - thfUnitaryFormula[expr] + thfUnitaryFormula[p1] { + if (p1.d_expr.isNull()) + { + PARSER_STATE->parseError("In scope of binder there must be a formula."); + } + expr = p1.d_expr; PARSER_STATE->popScope(); - // handle lambda case, in which return type must be flattened and the + // handle lambda case, in which case return type must be flattened and the // auxiliary variables introduced in the proccess must be added no the // variable list // @@ -1183,7 +1292,7 @@ thfUnitaryFormula[CVC4::Expr& expr] // add variables to BOUND_VAR_LIST bv.insert(bv.end(), flattenVars.begin(), flattenVars.end()); } - expr = MK_EXPR(kind, MK_EXPR(kind::BOUND_VAR_LIST, bv), expr); + p.d_expr = MK_EXPR(p.d_kind, MK_EXPR(kind::BOUND_VAR_LIST, bv), expr); } ; diff --git a/src/parser/tptp/tptp.cpp b/src/parser/tptp/tptp.cpp index 2b1edf15b..006f20a61 100644 --- a/src/parser/tptp/tptp.cpp +++ b/src/parser/tptp/tptp.cpp @@ -222,11 +222,9 @@ Expr Tptp::parseOpToExpr(ParseOp& p) { 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 it has a kind, it's a builtin one and this function should not have been + // called + assert(p.d_kind == kind::NULL_EXPR); if (isDeclared(p.d_name)) { // already appeared expr = getVariable(p.d_name); @@ -244,17 +242,19 @@ Expr Tptp::parseOpToExpr(ParseOp& p) 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); + // this happens with some arithmetic kinds, which are wrapped around + // lambdas. + args.insert(args.begin(), p.d_expr); + return em->mkExpr(kind::APPLY_UF, args); } - // Otherwise piece operator together + bool isBuiltinKind = false; + // the builtin kind of the overall return expression + Kind kind = kind::NULL_EXPR; + // First phase: piece operator together if (p.d_kind == kind::NULL_EXPR) { // A non-built-in function application, get the expression @@ -289,11 +289,11 @@ Expr Tptp::applyParseOp(ParseOp& p, std::vector& args) else { kind = p.d_kind; - isBuiltinOperator = true; + isBuiltinKind = true; } assert(kind != kind::NULL_EXPR); - // Second phase: apply the arguments to the parse op - if (isBuiltinOperator) + // Second phase: apply parse op to the arguments + if (isBuiltinKind) { if (!em->getOptions().getUfHo() && (kind == kind::EQUAL || kind == kind::DISTINCT)) @@ -308,6 +308,7 @@ Expr Tptp::applyParseOp(ParseOp& p, std::vector& args) } } } + if (args.size() > 2) { if (kind == kind::INTS_DIVISION || kind == kind::XOR @@ -429,26 +430,27 @@ Expr Tptp::convertStrToUnsorted(std::string str) { return e; } -void Tptp::mkLambdaWrapper(Expr& expr, Type argType) +Expr Tptp::mkLambdaWrapper(Kind k, Type argType) { + Debug("parser") << "mkLambdaWrapper: kind " << k << " and type " << argType + << "\n"; std::vector lvars; std::vector domainTypes = (static_cast(argType)).getArgTypes(); + ExprManager* em = getExprManager(); for (unsigned i = 0, size = domainTypes.size(); i < size; ++i) { // the introduced variable is internal (not parsable) std::stringstream ss; ss << "_lvar_" << i; - Expr v = getExprManager()->mkBoundVar(ss.str(), domainTypes[i]); + Expr v = em->mkBoundVar(ss.str(), domainTypes[i]); lvars.push_back(v); } // apply body of lambda to variables - Expr wrapper = getExprManager()->mkExpr( - kind::LAMBDA, - getExprManager()->mkExpr(kind::BOUND_VAR_LIST, lvars), - getExprManager()->mkExpr(expr, lvars)); - - expr = wrapper; + Expr wrapper = em->mkExpr(kind::LAMBDA, + em->mkExpr(kind::BOUND_VAR_LIST, lvars), + em->mkExpr(k, lvars)); + return wrapper; } Expr Tptp::getAssertionExpr(FormulaRole fr, Expr expr) { diff --git a/src/parser/tptp/tptp.h b/src/parser/tptp/tptp.h index 50ed0af8f..23791ea0c 100644 --- a/src/parser/tptp/tptp.h +++ b/src/parser/tptp/tptp.h @@ -103,13 +103,13 @@ class Tptp : public Parser { */ void addTheory(Theory theory); - /** creates a lambda abstraction around expression + /** creates a lambda abstraction around application of given kind * - * Given an expression expr of type argType = t1...tn -> t, creates a lambda + * Given a kind k and type argType = t1...tn -> t, creates a lambda * expression - * (lambda x1:t1,...,xn:tn . (expr x)) : t + * (lambda x1:t1,...,xn:tn . (k x1 ... xn)) : t */ - void mkLambdaWrapper(Expr& expr, Type argType); + Expr mkLambdaWrapper(Kind k, Type argType); /** get assertion expression, based on the formula role. * expr should have Boolean type. -- 2.30.2