From cb49e0143ac7b71a671b238cae6d0e63c0e90d2e Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Tue, 29 Mar 2022 14:37:22 -0500
Subject: [PATCH] Make ensureTermSort private (#8436)

This method was used to correct a limitation in the old API regarding parsing decimals. It should not be a public API method.
---
 src/api/cpp/cvc5.h                          | 26 ++++++++++-----------
 src/api/java/io/github/cvc5/api/Solver.java | 20 ----------------
 src/api/java/jni/solver.cpp                 | 17 --------------
 src/parser/smt2/Smt2.g                      |  3 +--
 4 files changed, 13 insertions(+), 53 deletions(-)

diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h
index 9c7bc0c98..3576f1f00 100644
--- a/src/api/cpp/cvc5.h
+++ b/src/api/cpp/cvc5.h
@@ -4600,20 +4600,6 @@ class CVC5_EXPORT Solver
    */
   void setOption(const std::string& option, const std::string& value) const;
 
-  /**
-   * If needed, convert this term to a given sort.
-   *
-   * @note The sort of the term must be convertible into the target sort.
-   *       Currently only Int to Real conversions are supported.
-   *
-   * @warning This method is experimental and may change in future versions.
-   *
-   * @param t the term
-   * @param s the target sort
-   * @return the term wrapped into a sort conversion if needed
-   */
-  Term ensureTermSort(const Term& t, const Sort& s) const;
-
   /**
    * Append \p symbol to the current list of universal variables.
    *
@@ -4961,6 +4947,18 @@ class CVC5_EXPORT Solver
   /** Check whether string s is a valid decimal integer. */
   bool isValidInteger(const std::string& s) const;
 
+  /**
+   * If needed, convert this term to a given sort.
+   * 
+   * The sort of the term must be convertible into the target sort.
+   * Currently only Int to Real conversions are supported.
+   *
+   * @param t the term
+   * @param s the target sort
+   * @return the term wrapped into a sort conversion if needed
+   */
+  Term ensureTermSort(const Term& t, const Sort& s) const;
+
   /**
    * Check that the given term is a valid closed term, which can be used as an
    * argument to, e.g., assert, get-value, block-model-values, etc.
diff --git a/src/api/java/io/github/cvc5/api/Solver.java b/src/api/java/io/github/cvc5/api/Solver.java
index f4468ba3e..4b4c2ccc8 100644
--- a/src/api/java/io/github/cvc5/api/Solver.java
+++ b/src/api/java/io/github/cvc5/api/Solver.java
@@ -2508,26 +2508,6 @@ public class Solver implements IPointer, AutoCloseable
 
   private native void setOption(long pointer, String option, String value);
 
-  /**
-   * If needed, convert this term to a given sort.
-   *
-   * @apiNote The sort of the term must be convertible into the target sort.
-   *          Currently only Int to Real conversions are supported.
-   *
-   * @apiNote This method is experimental and may change in future versions.
-   *
-   * @param t the term
-   * @param s the target sort
-   * @return the term wrapped into a sort conversion if needed
-   */
-  public Term ensureTermSort(Term t, Sort s)
-  {
-    long termPointer = ensureTermSort(pointer, t.getPointer(), s.getPointer());
-    return new Term(this, termPointer);
-  }
-
-  private native long ensureTermSort(long pointer, long termPointer, long sortPointer);
-
   /**
    * Append \p symbol to the current list of universal variables.
    * @param sort the sort of the universal variable
diff --git a/src/api/java/jni/solver.cpp b/src/api/java/jni/solver.cpp
index 7eccbf260..bb7d816fe 100644
--- a/src/api/java/jni/solver.cpp
+++ b/src/api/java/jni/solver.cpp
@@ -2385,23 +2385,6 @@ JNIEXPORT void JNICALL Java_io_github_cvc5_api_Solver_setOption(
   CVC5_JAVA_API_TRY_CATCH_END(env);
 }
 
-/*
- * Class:     io_github_cvc5_api_Solver
- * Method:    ensureTermSort
- * Signature: (JJJ)J
- */
-JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_ensureTermSort(
-    JNIEnv* env, jobject, jlong pointer, jlong termPointer, jlong sortPointer)
-{
-  CVC5_JAVA_API_TRY_CATCH_BEGIN;
-  Solver* solver = reinterpret_cast<Solver*>(pointer);
-  Term* term = reinterpret_cast<Term*>(termPointer);
-  Sort* sort = reinterpret_cast<Sort*>(sortPointer);
-  Term* retPointer = new Term(solver->ensureTermSort(*term, *sort));
-  return reinterpret_cast<jlong>(retPointer);
-  CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
-}
-
 /*
  * Class:     io_github_cvc5_api_Solver
  * Method:    declareSygusVar
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index ee95bb080..57abe495f 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -1706,8 +1706,7 @@ termAtomic[cvc5::api::Term& atomTerm]
   | DECIMAL_LITERAL
     {
       std::string realStr = AntlrInput::tokenText($DECIMAL_LITERAL);
-      atomTerm = SOLVER->ensureTermSort(SOLVER->mkReal(realStr),
-                                        SOLVER->getRealSort());
+      atomTerm = SOLVER->mkReal(realStr);
     }
 
   // Constants using indexed identifiers, e.g. (_ +oo 8 24) (positive infinity
-- 
2.30.2