From 2043e2a4f57942b6b81ae437de8a2aa00ffcd32f Mon Sep 17 00:00:00 2001 From: Haniel Barbosa Date: Thu, 7 Jan 2021 18:10:05 -0300 Subject: [PATCH] Remove dependency on expression layer in TPTP parser (#5753) --- src/parser/tptp/Tptp.g | 15 ++++++++++----- 1 file 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 & bvlist, PARSER_STATE->checkLetBinding(bvlist, lhs, rhs, false); std::vector 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 & bvlist, PARSER_STATE->checkLetBinding(bvlist, lhs, rhs, true); std::vector 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 ; -- 2.30.2