diff options
| author | Haniel Barbosa <hanielbbarbosa@gmail.com> | 2020-02-17 13:11:17 -0300 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-02-17 10:11:17 -0600 |
| commit | 27e1a5835139d5107010475cb951a1aa1350e7f4 (patch) | |
| tree | bf4b71b0d00b57565e8fb4f306918b4cd77df749 /src/parser/smt2/Smt2.g | |
| parent | ed27cf0f854e014922f9690d967c5ff9aa73693c (diff) | |
Using ParseOp in TPTP (#3764)
Diffstat (limited to 'src/parser/smt2/Smt2.g')
| -rw-r--r-- | src/parser/smt2/Smt2.g | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 3a6b444cc..6a045797a 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -80,8 +80,8 @@ using namespace CVC4::parser; #include <memory> #include "parser/antlr_tracing.h" -#include "parser/parser.h" #include "parser/parse_op.h" +#include "parser/parser.h" #include "smt/command.h" namespace CVC4 { @@ -1410,8 +1410,8 @@ extendedCommand[std::unique_ptr<CVC4::Command>* cmd] { cmd->reset(new GetAbductCommand(name,e, t)); } - | DECLARE_HEAP LPAREN_TOK - sortSymbol[t,CHECK_DECLARED] + | DECLARE_HEAP LPAREN_TOK + sortSymbol[t, CHECK_DECLARED] sortSymbol[t, CHECK_DECLARED] // We currently do nothing with the type information declared for the heap. { cmd->reset(new EmptyCommand()); } @@ -1695,8 +1695,8 @@ termNonVariable[CVC4::Expr& expr, CVC4::Expr& expr2] RPAREN_TOK | LPAREN_TOK qualIdentifier[p] termList[args,expr] RPAREN_TOK - { - expr = PARSER_STATE->applyParseOp(p,args); + { + expr = PARSER_STATE->applyParseOp(p, args); } | /* a let or sygus let binding */ LPAREN_TOK ( |