api: Remove Sort::isParametricDatatype(). (#8405)

Previously, Sort::isParametricDatatype() returned true for both
instantiated and non-instantiated parametric datatypes.

This deletes the method, instead one can check getDatatype().isParametric(). Parametric datatypes will be distinguished from instantiated parametric datatypes via a forthcoming method Sort::isInstantiated.

Co-authored-by: ajreynol <andrew.j.reynolds@gmail.com>

diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp
index 4544fd7d2bb2510404142cb18317f307e2221535..fa9afe101230cc3cc8c9a96075a79b5e77be76e0 100644 (file)
--- a/src/api/cpp/cvc5.cpp
+++ b/src/api/cpp/cvc5.cpp
@@ -1248,16 +1248,6 @@ bool Sort::isDatatype() const
   CVC5_API_TRY_CATCH_END;
 }
 
-bool Sort::isParametricDatatype() const
-{
-  CVC5_API_TRY_CATCH_BEGIN;
-  //////// all checks before this line
-  if (!d_type->isDatatype()) return false;
-  return d_type->isParametricDatatype();
-  ////////
-  CVC5_API_TRY_CATCH_END;
-}
-
 bool Sort::isConstructor() const
 {
   CVC5_API_TRY_CATCH_BEGIN;
@@ -1400,9 +1390,9 @@ Sort Sort::instantiate(const std::vector<Sort>& params) const
   CVC5_API_TRY_CATCH_BEGIN;
   CVC5_API_CHECK_NOT_NULL;
   CVC5_API_CHECK_DOMAIN_SORTS(params);
-  CVC5_API_CHECK(isParametricDatatype() || isSortConstructor())
+  CVC5_API_CHECK(d_type->isParametricDatatype() || d_type->isSortConstructor())
       << "Expected parametric datatype or sort constructor sort.";
-  CVC5_API_CHECK(!isParametricDatatype()
+  CVC5_API_CHECK(!d_type->isParametricDatatype()
                  || d_type->getNumChildren() == params.size() + 1)
       << "Arity mismatch for instantiated parametric datatype";
   CVC5_API_CHECK(!isSortConstructor()
@@ -1714,7 +1704,7 @@ uint32_t Sort::getFloatingPointExponentSize() const
 {
   CVC5_API_TRY_CATCH_BEGIN;
   CVC5_API_CHECK_NOT_NULL;
-  CVC5_API_CHECK(isFloatingPoint()) << "Not a floating-point sort.";
+  CVC5_API_CHECK(d_type->isFloatingPoint()) << "Not a floating-point sort.";
   //////// all checks before this line
   return d_type->getFloatingPointExponentSize();
   ////////
@@ -1725,7 +1715,7 @@ uint32_t Sort::getFloatingPointSignificandSize() const
 {
   CVC5_API_TRY_CATCH_BEGIN;
   CVC5_API_CHECK_NOT_NULL;
-  CVC5_API_CHECK(isFloatingPoint()) << "Not a floating-point sort.";
+  CVC5_API_CHECK(d_type->isFloatingPoint()) << "Not a floating-point sort.";
   //////// all checks before this line
   return d_type->getFloatingPointSignificandSize();
   ////////
@@ -1738,7 +1728,8 @@ std::vector<Sort> Sort::getDatatypeParamSorts() const
 {
   CVC5_API_TRY_CATCH_BEGIN;
   CVC5_API_CHECK_NOT_NULL;
-  CVC5_API_CHECK(isParametricDatatype()) << "Not a parametric datatype sort.";
+  CVC5_API_CHECK(d_type->isParametricDatatype())
+      << "Not a parametric datatype sort.";
   //////// all checks before this line
   return typeNodeVectorToSorts(d_solver, d_type->getParamTypes());
   ////////
@@ -1749,7 +1740,7 @@ size_t Sort::getDatatypeArity() const
 {
   CVC5_API_TRY_CATCH_BEGIN;
   CVC5_API_CHECK_NOT_NULL;
-  CVC5_API_CHECK(isDatatype()) << "Not a datatype sort.";
+  CVC5_API_CHECK(d_type->isDatatype()) << "Not a datatype sort.";
   //////// all checks before this line
   return d_type->isParametricDatatype() ? d_type->getNumChildren() - 1 : 0;
   ////////
@@ -1773,7 +1764,7 @@ std::vector<Sort> Sort::getTupleSorts() const
 {
   CVC5_API_TRY_CATCH_BEGIN;
   CVC5_API_CHECK_NOT_NULL;
-  CVC5_API_CHECK(isTuple()) << "Not a tuple sort.";
+  CVC5_API_CHECK(d_type->isTuple()) << "Not a tuple sort.";
   //////// all checks before this line
   return typeNodeVectorToSorts(d_solver, d_type->getTupleTypes());
   ////////

diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h
index 16552edb7e5352b985cc1cd2649f2e201ddee26a..7a81dacb67658a178652aaf48d5cb28174516d56 100644 (file)
--- a/src/api/cpp/cvc5.h
+++ b/src/api/cpp/cvc5.h
@@ -505,16 +505,6 @@ class CVC5_EXPORT Sort
    */
   bool isDatatype() const;
 
-  /**
-   * Is this a parametric datatype sort? A parametric datatype sort is either
-   * one that is returned by a call to Solver::mkDatatypeSort() or
-   * Solver::mkDatatypeSorts() for a parametric datatype, or an instantiated
-   * datatype sort returned by Sort::instantiate() for parametric datatype
-   * sort `s`.
-   * @return true if the sort is a parametric datatype sort
-   */
-  bool isParametricDatatype() const;
-
   /**
    * Is this a constructor sort?
    * @return true if the sort is a constructor sort

diff --git a/src/api/java/io/github/cvc5/api/Sort.java b/src/api/java/io/github/cvc5/api/Sort.java
index 61afb909a5909b787c028a3afd4be4a3f1894d7a..e600fbaeb49a74c177be8409a6caffd6a229b86b 100644 (file)
--- a/src/api/java/io/github/cvc5/api/Sort.java
+++ b/src/api/java/io/github/cvc5/api/Sort.java
@@ -199,17 +199,6 @@ public class Sort extends AbstractPointer implements Comparable<Sort>
 
   private native boolean isDatatype(long pointer);
 
-  /**
-   * Is this a parametric datatype sort?
-   * @return true if the sort is a parametric datatype sort
-   */
-  public boolean isParametricDatatype()
-  {
-    return isParametricDatatype(pointer);
-  }
-
-  private native boolean isParametricDatatype(long pointer);
-
   /**
    * Is this a constructor sort?
    * @return true if the sort is a constructor sort

diff --git a/src/api/java/jni/sort.cpp b/src/api/java/jni/sort.cpp
index 67e143c5c01408b0859862b63041bb4b5c43dbd9..12ce60ae069aa8c83a053098ce2f5bcadcea26c5 100644 (file)
--- a/src/api/java/jni/sort.cpp
+++ b/src/api/java/jni/sort.cpp
@@ -249,20 +249,6 @@ Java_io_github_cvc5_api_Sort_isDatatype(JNIEnv* env, jobject, jlong pointer)
   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast<jboolean>(false));
 }
 
-/*
- * Class:     io_github_cvc5_api_Sort
- * Method:    isParametricDatatype
- * Signature: (J)Z
- */
-JNIEXPORT jboolean JNICALL Java_io_github_cvc5_api_Sort_isParametricDatatype(
-    JNIEnv* env, jobject, jlong pointer)
-{
-  CVC5_JAVA_API_TRY_CATCH_BEGIN;
-  Sort* current = reinterpret_cast<Sort*>(pointer);
-  return static_cast<jboolean>(current->isParametricDatatype());
-  CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast<jboolean>(false));
-}
-
 /*
  * Class:     io_github_cvc5_api_Sort
  * Method:    isConstructor

diff --git a/src/api/python/cvc5.pxd b/src/api/python/cvc5.pxd
index a5ca0470e5bf8388d1536e7f5063b5fffc2bcc4d..f923a0263bc517303d2f54b44e93d38bc69898c6 100644 (file)
--- a/src/api/python/cvc5.pxd
+++ b/src/api/python/cvc5.pxd
@@ -387,7 +387,6 @@ cdef extern from "api/cpp/cvc5.h" namespace "cvc5::api":
         bint isBitVector() except +
         bint isFloatingPoint() except +
         bint isDatatype() except +
-        bint isParametricDatatype() except +
         bint isConstructor() except +
         bint isSelector() except +
         bint isTester() except +

diff --git a/src/api/python/cvc5.pxi b/src/api/python/cvc5.pxi
index cece9c3fbb6f5aa6faf3fb72e9f7cd82f80d9b64..963ab70b8a17da644807b2bd80f89beebe2be143 100644 (file)
--- a/src/api/python/cvc5.pxi
+++ b/src/api/python/cvc5.pxi
@@ -2655,14 +2655,6 @@ cdef class Sort:
         """
         return self.csort.isDatatype()
 
-    def isParametricDatatype(self):
-        """
-            Is this a parametric datatype sort?
-
-            :return: True if the sort is a parametric datatype sort.
-        """
-        return self.csort.isParametricDatatype()
-
     def isConstructor(self):
         """
             Is this a constructor sort?

diff --git a/src/expr/symbol_table.cpp b/src/expr/symbol_table.cpp
index 66b690a893c12767ef45f6ce63a3b257c163ba6b..7aabb20557466f8e04907f9aa96aefa731fd978c 100644 (file)
--- a/src/expr/symbol_table.cpp
+++ b/src/expr/symbol_table.cpp
@@ -485,8 +485,9 @@ api::Sort SymbolTable::Implementation::lookupType(
   }
   if (p.second.isDatatype())
   {
-    PrettyCheckArgument(
-        p.second.isParametricDatatype(), name, "expected parametric datatype");
+    PrettyCheckArgument(p.second.getDatatype().isParametric(),
+                        name,
+                        "expected parametric datatype");
     return p.second.instantiate(params);
   }
   bool isSortConstructor = p.second.isSortConstructor();

diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp
index acb8b78a51d7fc9309bcffe62c4d8fa3893b6a0c..9c38772654475e6b9c99df609858f37014773a43 100644 (file)
--- a/src/parser/parser.cpp
+++ b/src/parser/parser.cpp
@@ -384,9 +384,9 @@ std::vector<api::Sort> Parser::bindMutualDatatypeTypes(
       if (isDeclared(name, SYM_SORT)) {
         throw ParserException(name + " already declared");
       }
-      if (t.isParametricDatatype())
+      if (dt.isParametric())
       {
-        std::vector<api::Sort> paramTypes = t.getDatatypeParamSorts();
+        std::vector<api::Sort> paramTypes = dt.getParameters();
         defineType(name, paramTypes, t);
       }
       else
@@ -566,11 +566,16 @@ api::Term Parser::applyTypeAscription(api::Term t, api::Sort s)
   {
     // Type ascriptions only have an effect on the node structure if this is a
     // parametric datatype.
-    if (s.isParametricDatatype())
+    // get the datatype that t belongs to
+    api::Sort etyped = etype.getConstructorCodomainSort();
+    api::Datatype d = etyped.getDatatype();
+    // Note that we check whether the datatype is parametric, and not whether
+    // etyped is a parametric datatype, since e.g. the smt2 parser constructs
+    // an arbitrary instantitated constructor term before it is resolved.
+    // Hence, etyped is an instantiated datatype type, but we correctly
+    // check if its datatype is parametric.
+    if (d.isParametric())
     {
-      // get the datatype that t belongs to
-      api::Sort etyped = etype.getConstructorCodomainSort();
-      api::Datatype d = etyped.getDatatype();
       // lookup by name
       api::DatatypeConstructor dc = d.getConstructor(t.toString());
       // ask the constructor for the specialized constructor term
@@ -582,8 +587,7 @@ api::Term Parser::applyTypeAscription(api::Term t, api::Sort s)
     {
       std::stringstream ss;
       ss << "Type ascription on constructor not satisfied, term " << t
-         << " expected sort " << s << " but has sort "
-         << t.getSort().getConstructorCodomainSort();
+         << " expected sort " << s << " but has sort " << etyped;
       parseError(ss.str());
     }
     return t;

diff --git a/test/unit/api/cpp/sort_black.cpp b/test/unit/api/cpp/sort_black.cpp
index bcf57ef2db6af6f18e2351488d5b2fc239976b31..40e00d996db8662eb578ece0c04e4b8f46583c59 100644 (file)
--- a/test/unit/api/cpp/sort_black.cpp
+++ b/test/unit/api/cpp/sort_black.cpp
@@ -144,13 +144,6 @@ TEST_F(TestApiBlackSort, isDatatype)
   ASSERT_NO_THROW(Sort().isDatatype());
 }
 
-TEST_F(TestApiBlackSort, isParametricDatatype)
-{
-  Sort param_dt_sort = create_param_datatype_sort();
-  ASSERT_TRUE(param_dt_sort.isParametricDatatype());
-  ASSERT_NO_THROW(Sort().isParametricDatatype());
-}
-
 TEST_F(TestApiBlackSort, isConstructor)
 {
   Sort dt_sort = create_datatype_sort();

diff --git a/test/unit/api/java/SortTest.java b/test/unit/api/java/SortTest.java
index f1343366bbe5d41aa13040490edd5a716ea16168..87016a0e348259487507220368f8be3b40bd8a3a 100644 (file)
--- a/test/unit/api/java/SortTest.java
+++ b/test/unit/api/java/SortTest.java
@@ -147,13 +147,6 @@ class SortTest
     assertDoesNotThrow(() -> d_solver.getNullSort().isDatatype());
   }
 
-  @Test void isParametricDatatype() throws CVC5ApiException
-  {
-    Sort param_dt_sort = create_param_datatype_sort();
-    assertTrue(param_dt_sort.isParametricDatatype());
-    assertDoesNotThrow(() -> d_solver.getNullSort().isParametricDatatype());
-  }
-
   @Test void isConstructor() throws CVC5ApiException
   {
     Sort dt_sort = create_datatype_sort();

diff --git a/test/unit/api/python/test_sort.py b/test/unit/api/python/test_sort.py
index f552a3eb200bde2a7ea2aba7885776cb919f6bf8..83c60b312dd554f7a701c5bb1290433fe40a7cb5 100644 (file)
--- a/test/unit/api/python/test_sort.py
+++ b/test/unit/api/python/test_sort.py
@@ -133,12 +133,6 @@ def test_is_datatype(solver):
     Sort(solver).isDatatype()
 
 
-def test_is_parametric_datatype(solver):
-    param_dt_sort = create_param_datatype_sort(solver)
-    assert param_dt_sort.isParametricDatatype()
-    Sort(solver).isParametricDatatype()
-
-
 def test_is_constructor(solver):
     dt_sort = create_datatype_sort(solver)
     dt = dt_sort.getDatatype()