From: Andrew Reynolds Date: Thu, 27 Feb 2020 23:06:02 +0000 (-0600) Subject: Refactor operator applications in the parser (#3831) X-Git-Tag: cvc5-1.0.0~3581 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=5c844f064cf6394030918c32f42d0764703b9786;p=cvc5.git Refactor operator applications in the parser (#3831) This PR refactors how a term is constructed based on information regarding an operator (ParseOp) and its arguments. It also makes a few miscellaneous fixes. This includes: Indexed ops are carried in ParseOp via api::Op not Expr, getKindForFunction is limited to "APPLY" kinds from the new API, The TPTP/SMT2 parsers rely on mkTermInternal for handling associativity. TPTP should use DIVISION not DIVISION_TOTAL. This is in preparation for parser migration. These are the essential behavioral changes required for using the new API for the majority of the parser. --- diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g index 33ca7bcf2..94904f6d9 100644 --- a/src/parser/cvc/Cvc.g +++ b/src/parser/cvc/Cvc.g @@ -1780,8 +1780,9 @@ postfixTerm[CVC4::Expr& f] | LPAREN { args.push_back(f); } formula[f] { args.push_back(f); } ( COMMA formula[f] { args.push_back(f); } )* RPAREN - // TODO: check arity - { Kind k = PARSER_STATE->getKindForFunction(args.front()); + { + PARSER_STATE->checkFunctionLike(args.front()); + Kind k = PARSER_STATE->getKindForFunction(args.front()); Debug("parser") << "expr is " << args.front() << std::endl; Debug("parser") << "kind is " << k << std::endl; f = MK_EXPR(k, args); diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp index d2577433e..5beec6565 100644 --- a/src/parser/parser.cpp +++ b/src/parser/parser.cpp @@ -138,11 +138,6 @@ Expr Parser::getExpressionForNameAndType(const std::string& name, Type t) { } Kind Parser::getKindForFunction(Expr fun) { - Kind k = getExprManager()->operatorToKind(fun); - if (k != UNDEFINED_KIND) - { - return k; - } Type t = fun.getType(); if (t.isFunction()) { diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index caa3e471f..a47d58944 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -1973,8 +1973,7 @@ identifier[CVC4::ParseOp& p] } | sym=SIMPLE_SYMBOL nonemptyNumeralList[numerals] { - p.d_expr = PARSER_STATE->mkIndexedOp(AntlrInput::tokenText($sym), numerals) - .getExpr(); + p.d_op = PARSER_STATE->mkIndexedOp(AntlrInput::tokenText($sym), numerals); } ) RPAREN_TOK diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index 48c1c96c7..ef13d379e 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -1634,13 +1634,13 @@ Expr Smt2::applyParseOp(ParseOp& p, std::vector& args) // First phase: process the operator if (Debug.isOn("parser")) { - Debug("parser") << "Apply parse op to:" << std::endl; - Debug("parser") << "args has size " << args.size() << std::endl; + Debug("parser") << "applyParseOp: " << p << " to:" << std::endl; for (std::vector::iterator i = args.begin(); i != args.end(); ++i) { Debug("parser") << "++ " << *i << std::endl; } } + api::Op op; if (p.d_kind != kind::NULL_EXPR) { // It is a special case, e.g. tupSel or array constant specification. @@ -1659,6 +1659,11 @@ Expr Smt2::applyParseOp(ParseOp& p, std::vector& args) kind = fkind; } } + else if (!p.d_op.isNull()) + { + // it was given an operator + op = p.d_op; + } else { isBuiltinOperator = isOperatorEnabled(p.d_name); @@ -1808,37 +1813,8 @@ Expr Smt2::applyParseOp(ParseOp& p, std::vector& args) } } } - if (args.size() > 2) - { - if (kind == kind::INTS_DIVISION || kind == kind::XOR - || kind == kind::MINUS || kind == kind::DIVISION - || (kind == kind::BITVECTOR_XNOR && v2_6())) - { - // Builtin operators that are not tokenized, are left associative, - // but not internally variadic must set this. - return em->mkLeftAssociative(kind, args); - } - else if (kind == kind::IMPLIES) - { - /* right-associative, but CVC4 internally only supports 2 args */ - return em->mkRightAssociative(kind, args); - } - else 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->mkChain(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); - } - else if (!strictModeEnabled() && (kind == kind::AND || kind == kind::OR) - && args.size() == 1) + if (!strictModeEnabled() && (kind == kind::AND || kind == kind::OR) + && args.size() == 1) { // Unary AND/OR can be replaced with the argument. return args[0]; @@ -1847,11 +1823,11 @@ Expr Smt2::applyParseOp(ParseOp& p, std::vector& args) { return em->mkExpr(kind::UMINUS, args[0]); } - else - { - checkOperator(kind, args.size()); - return em->mkExpr(kind, args); - } + api::Term ret = + d_solver->mkTerm(intToExtKind(kind), api::exprVectorToTerms(args)); + Debug("parser") << "applyParseOp: return default builtin " << ret + << std::endl; + return ret.getExpr(); } if (args.size() >= 2) @@ -1875,6 +1851,12 @@ Expr Smt2::applyParseOp(ParseOp& p, std::vector& args) } } } + if (!op.isNull()) + { + api::Term ret = d_solver->mkTerm(op, api::exprVectorToTerms(args)); + Debug("parser") << "applyParseOp: return op : " << ret << std::endl; + return ret.getExpr(); + } if (kind == kind::NULL_EXPR) { std::vector eargs(args.begin() + 1, args.end()); diff --git a/src/parser/tptp/Tptp.g b/src/parser/tptp/Tptp.g index c4b4ddbc0..873fde25c 100644 --- a/src/parser/tptp/Tptp.g +++ b/src/parser/tptp/Tptp.g @@ -595,7 +595,7 @@ definedFun[CVC4::ParseOp& p] } | '$quotient' { - p.d_kind = kind::DIVISION_TOTAL; + p.d_kind = kind::DIVISION; } | ( '$quotient_e' { remainder = false; } | '$remainder_e' { remainder = true; } diff --git a/src/parser/tptp/tptp.cpp b/src/parser/tptp/tptp.cpp index 006f20a61..d18e4a778 100644 --- a/src/parser/tptp/tptp.cpp +++ b/src/parser/tptp/tptp.cpp @@ -241,6 +241,14 @@ Expr Tptp::parseOpToExpr(ParseOp& p) Expr Tptp::applyParseOp(ParseOp& p, std::vector& args) { + if (Debug.isOn("parser")) + { + Debug("parser") << "applyParseOp: " << p << " to:" << std::endl; + for (std::vector::iterator i = args.begin(); i != args.end(); ++i) + { + Debug("parser") << "++ " << *i << std::endl; + } + } assert(!args.empty()); ExprManager* em = getExprManager(); // If operator already defined, just build application @@ -308,35 +316,6 @@ Expr Tptp::applyParseOp(ParseOp& p, std::vector& args) } } } - - 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->mkChain(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) { @@ -347,8 +326,8 @@ Expr Tptp::applyParseOp(ParseOp& p, std::vector& args) { return em->mkExpr(kind::UMINUS, args[0]); } - checkOperator(kind, args.size()); - return em->mkExpr(kind, args); + return d_solver->mkTerm(intToExtKind(kind), api::exprVectorToTerms(args)) + .getExpr(); } // check if partially applied function, in this case we use HO_APPLY @@ -368,7 +347,8 @@ Expr Tptp::applyParseOp(ParseOp& p, std::vector& args) 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 d_solver->mkTerm(api::HO_APPLY, api::exprVectorToTerms(args)) + .getExpr(); } } }