diff options
| author | Haniel Barbosa <hanielbbarbosa@gmail.com> | 2021-01-07 18:10:05 -0300 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-01-07 18:10:05 -0300 |
| commit | 2043e2a4f57942b6b81ae437de8a2aa00ffcd32f (patch) | |
| tree | 538af86926fea0fdaf50e016ced5e7f37cec37a1 /src/parser | |
| parent | 94c687bb12f3ba89225886b3b3eeea3f0dfdfd0a (diff) | |
Remove dependency on expression layer in TPTP parser (#5753)
Diffstat (limited to 'src/parser')
| -rw-r--r-- | src/parser/tptp/Tptp.g | 15 |
1 files changed, 10 insertions, 5 deletions
diff --git a/src/parser/tptp/Tptp.g b/src/parser/tptp/Tptp.g index 0c16e472d..460156c37 100644 --- a/src/parser/tptp/Tptp.g +++ b/src/parser/tptp/Tptp.g @@ -102,9 +102,6 @@ using namespace CVC4::parser; #include "api/cvc4cpp.h" #include "base/output.h" -#include "expr/expr.h" -#include "expr/kind.h" -#include "expr/type.h" #include "parser/antlr_input.h" #include "parser/parser.h" #include "parser/tptp/tptp.h" @@ -1432,7 +1429,11 @@ tffLetTermBinding[std::vector<CVC4::api::Term> & bvlist, PARSER_STATE->checkLetBinding(bvlist, lhs, rhs, false); std::vector<api::Term> lchildren(++lhs.begin(), lhs.end()); rhs = MK_TERM(api::LAMBDA, MK_TERM(api::BOUND_VAR_LIST, lchildren), rhs); - lhs = api::Term(SOLVER, lhs.getExpr().getOperator()); + // since lhs is always APPLY_UF (otherwise we'd have had a parser error in + // checkLetBinding) the function to be replaced is always the first + // argument. Note that the way in which lchildren is built above is also + // relying on this. + lhs = lhs[0]; } | LPAREN_TOK tffLetTermBinding[bvlist, lhs, rhs] RPAREN_TOK ; @@ -1454,7 +1455,11 @@ tffLetFormulaBinding[std::vector<CVC4::api::Term> & bvlist, PARSER_STATE->checkLetBinding(bvlist, lhs, rhs, true); std::vector<api::Term> lchildren(++lhs.begin(), lhs.end()); rhs = MK_TERM(api::LAMBDA, MK_TERM(api::BOUND_VAR_LIST, lchildren), rhs); - lhs = api::Term(SOLVER, lhs.getExpr().getOperator()); + // since lhs is always APPLY_UF (otherwise we'd have had a parser error in + // checkLetBinding) the function to be replaced is always the first + // argument. Note that the way in which lchildren is built above is also + // relying on this. + lhs = lhs[0]; } | LPAREN_TOK tffLetFormulaBinding[bvlist, lhs, rhs] RPAREN_TOK ; |