diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-02-27 17:06:02 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-02-27 17:06:02 -0600 |
commit | 5c844f064cf6394030918c32f42d0764703b9786 (patch) | |
tree | 009be2796a9c1236c23f569c0c744b446d52e622 /src/parser/tptp | |
parent | cc9a1b02cb8b1920c2a16825b3ff58acdef4dce8 (diff) |
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.
Diffstat (limited to 'src/parser/tptp')
-rw-r--r-- | src/parser/tptp/Tptp.g | 2 | ||||
-rw-r--r-- | src/parser/tptp/tptp.cpp | 44 |
2 files changed, 13 insertions, 33 deletions
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<Expr>& args) { + if (Debug.isOn("parser")) + { + Debug("parser") << "applyParseOp: " << p << " to:" << std::endl; + for (std::vector<Expr>::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<Expr>& 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<Expr>& 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<Expr>& 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(); } } } |