From: Haniel Barbosa <hanielbbarbosa@gmail.com>
Date: Thu, 7 Jan 2021 21:10:05 +0000 (-0300)
Subject: Remove dependency on expression layer in TPTP parser (#5753)
X-Git-Tag: cvc5-1.0.0~2395
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=2043e2a4f57942b6b81ae437de8a2aa00ffcd32f;p=cvc5.git

Remove dependency on expression layer in TPTP parser (#5753)
---

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
   ;