From e7fd317234408618bb0c5fb3c4511bdd47f200e7 Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Mon, 9 May 2022 13:29:35 -0500
Subject: [PATCH] Do not depend on subtyping for APPLY_UF in TPTP parser
 (#8737)

---
 src/parser/tptp/tptp.cpp | 28 ++++++++++++++++++++++++++--
 src/parser/tptp/tptp.h   |  4 ++++
 2 files changed, 30 insertions(+), 2 deletions(-)

diff --git a/src/parser/tptp/tptp.cpp b/src/parser/tptp/tptp.cpp
index 7da9380e1..dd6ba53cd 100644
--- a/src/parser/tptp/tptp.cpp
+++ b/src/parser/tptp/tptp.cpp
@@ -268,6 +268,24 @@ cvc5::Term Tptp::isTptpDeclared(const std::string& name)
   return cvc5::Term();
 }
 
+Term Tptp::makeApplyUf(std::vector<Term>& args)
+{
+  std::vector<Sort> argSorts = args[0].getSort().getFunctionDomainSorts();
+  if (argSorts.size() + 1 != args.size())
+  {
+    // arity mismatch
+    parseError("Applying function to wrong number of arguments");
+  }
+  for (size_t i = 0, nargs = argSorts.size(); i < nargs; i++)
+  {
+    if (argSorts[i].isReal() && args[i + 1].getSort().isInteger())
+    {
+      args[i + 1] = d_solver->mkTerm(TO_REAL, {args[i + 1]});
+    }
+  }
+  return d_solver->mkTerm(APPLY_UF, args);
+}
+
 cvc5::Term Tptp::applyParseOp(ParseOp& p, std::vector<cvc5::Term>& args)
 {
   if (TraceIsOn("parser"))
@@ -286,7 +304,7 @@ cvc5::Term Tptp::applyParseOp(ParseOp& p, std::vector<cvc5::Term>& args)
     // this happens with some arithmetic kinds, which are wrapped around
     // lambdas.
     args.insert(args.begin(), p.d_expr);
-    return d_solver->mkTerm(cvc5::APPLY_UF, args);
+    return makeApplyUf(args);
   }
   bool isBuiltinKind = false;
   // the builtin kind of the overall return expression
@@ -408,6 +426,11 @@ cvc5::Term Tptp::applyParseOp(ParseOp& p, std::vector<cvc5::Term>& args)
         // must curry the partial application
         return d_solver->mkTerm(cvc5::HO_APPLY, args);
       }
+      else if (kind == APPLY_UF)
+      {
+        // ensure subtyping is not used
+        return makeApplyUf(args);
+      }
     }
   }
   return d_solver->mkTerm(kind, args);
@@ -520,7 +543,8 @@ cvc5::Term Tptp::convertRatToUnsorted(cvc5::Term expr)
   // Add the inverse in order to show that over the elements that
   // appear in the problem there is a bijection between unsorted and
   // rational
-  cvc5::Term ret = d_solver->mkTerm(cvc5::APPLY_UF, {d_rtu_op, expr});
+  std::vector<Term> args = {d_rtu_op, expr};
+  Term ret = makeApplyUf(args);
   if (d_r_converted.find(expr) == d_r_converted.end()) {
     d_r_converted.insert(expr);
     if (expr.getSort().isInteger())
diff --git a/src/parser/tptp/tptp.h b/src/parser/tptp/tptp.h
index db1ed03e9..5a0c45844 100644
--- a/src/parser/tptp/tptp.h
+++ b/src/parser/tptp/tptp.h
@@ -182,6 +182,10 @@ class Tptp : public Parser {
   void addArithmeticOperators();
   /** is the name declared, if so, return the term for that name */
   cvc5::Term isTptpDeclared(const std::string& name);
+  /**
+   * Make APPLY_UF from arguments, which ensures that subyping is not used.
+   */
+  Term makeApplyUf(std::vector<Term>& args);
 
   // In CNF variable are implicitly binded
   // d_freevar collect them
-- 
2.30.2