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/cvc/Cvc.g | |
| 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/cvc/Cvc.g')
| -rw-r--r-- | src/parser/cvc/Cvc.g | 5 |
1 files changed, 3 insertions, 2 deletions
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); |