api: Add Sort::isInstantiated(). (#8425)

This further removes Sort::isUinterpretedSortParameterized().

diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp
index 5c92c9d3ad437613e0fcca238fcdb2d8097d8feb..8b16ea8bc16f27ff0815ae8e79de86ff659edb4b 100644 (file)
--- a/src/api/cpp/cvc5.cpp
+++ b/src/api/cpp/cvc5.cpp
@@ -1378,13 +1378,23 @@ Datatype Sort::getDatatype() const
 {
   CVC5_API_TRY_CATCH_BEGIN;
   CVC5_API_CHECK_NOT_NULL;
-  CVC5_API_CHECK(isDatatype()) << "Expected datatype sort.";
+  CVC5_API_CHECK(d_type->isDatatype()) << "Expected datatype sort.";
   //////// all checks before this line
   return Datatype(d_solver, d_type->getDType());
   ////////
   CVC5_API_TRY_CATCH_END;
 }
 
+bool Sort::isInstantiated() const
+{
+  CVC5_API_TRY_CATCH_BEGIN;
+  CVC5_API_CHECK_NOT_NULL;
+  //////// all checks before this line
+  return d_type->isInstantiated();
+  ////////
+  CVC5_API_TRY_CATCH_END;
+}
+
 Sort Sort::instantiate(const std::vector<Sort>& params) const
 {
   CVC5_API_TRY_CATCH_BEGIN;
@@ -1639,20 +1649,6 @@ Sort Sort::getSequenceElementSort() const
 
 /* Uninterpreted sort -------------------------------------------------- */
 
-bool Sort::isUninterpretedSortParameterized() const
-{
-  CVC5_API_TRY_CATCH_BEGIN;
-  CVC5_API_CHECK_NOT_NULL;
-  CVC5_API_CHECK(isUninterpretedSort()) << "Not an uninterpreted sort.";
-  //////// all checks before this line
-
-  /* This method is not implemented in the NodeManager, since whether a
-   * uninterpreted sort is parameterized is irrelevant for solving. */
-  return d_type->getNumChildren() > 0;
-  ////////
-  CVC5_API_TRY_CATCH_END;
-}
-
 std::vector<Sort> Sort::getUninterpretedSortParamSorts() const
 {
   CVC5_API_TRY_CATCH_BEGIN;

diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h
index c3e5b93ea226a9fa0ed97dfcc927882ed2018b15..18f66dfa8d3c9ed9af07534629381497fce1e46e 100644 (file)
--- a/src/api/cpp/cvc5.h
+++ b/src/api/cpp/cvc5.h
@@ -594,6 +594,18 @@ class CVC5_EXPORT Sort
    */
   bool isUninterpretedSortConstructor() const;
 
+  /**
+   * Is this an instantiated (parametric datatype or uninterpreted sort
+   * constructor) sort?
+   *
+   * An instantiated sort is a sort that has been constructed from
+   * instantiating a sort with sort arguments
+   * (see Sort::instantiate(const std::vector<Sort>&) const)).
+   *
+   * @return true if this is an instantiated sort
+   */
+  bool isInstantiated() const;
+
   /**
    * @return the underlying datatype of a datatype sort
    */

diff --git a/src/api/java/io/github/cvc5/api/Sort.java b/src/api/java/io/github/cvc5/api/Sort.java
index ba97057e447fd9143f49784e4bb1940f12dfa905..fac9c4679c2d9aff6c47a9c68a9cbc11ac917dde 100644 (file)
--- a/src/api/java/io/github/cvc5/api/Sort.java
+++ b/src/api/java/io/github/cvc5/api/Sort.java
@@ -362,6 +362,23 @@ public class Sort extends AbstractPointer implements Comparable<Sort>
 
   private native boolean isUninterpretedSortConstructor(long pointer);
 
+  /**
+   * Is this an instantiated (parametric datatype or uninterpreted sort
+   * constructor) sort?
+   *
+   * An instantiated sort is a sort that has been constructed from
+   * instantiating a sort with sort arguments
+   * (see Sort.instantiate()).
+   *
+   * @return true if this is an instantiated sort
+   */
+  public boolean isInstantiated()
+  {
+    return isInstantiated(pointer);
+  }
+
+  private native boolean isInstantiated(long pointer);
+
   /**
    * @return the underlying datatype of a datatype sort
    */
@@ -646,16 +663,6 @@ public class Sort extends AbstractPointer implements Comparable<Sort>
 
   /* Uninterpreted sort -------------------------------------------------- */
 
-  /**
-   * @return true if an uninterpreted sort is parameterezied
-   */
-  public boolean isUninterpretedSortParameterized()
-  {
-    return isUninterpretedSortParameterized(pointer);
-  }
-
-  private native boolean isUninterpretedSortParameterized(long pointer);
-
   /**
    * @return the parameter sorts of an uninterpreted sort
    */

diff --git a/src/api/java/jni/sort.cpp b/src/api/java/jni/sort.cpp
index a3d1f135f7ba00b4aff4a67e2dd45dd36df2904f..4d5b6986c72b2370b18c2c1df77575111775a3b6 100644 (file)
--- a/src/api/java/jni/sort.cpp
+++ b/src/api/java/jni/sort.cpp
@@ -454,6 +454,20 @@ Java_io_github_cvc5_api_Sort_isUninterpretedSortConstructor(JNIEnv* env,
   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast<jboolean>(false));
 }
 
+/*
+ * Class:     io_github_cvc5_api_Sort
+ * Method:    isInstantiated
+ * Signature: (J)Z
+ */
+JNIEXPORT jboolean JNICALL
+Java_io_github_cvc5_api_Sort_isInstantiated(JNIEnv* env, jobject, jlong pointer)
+{
+  CVC5_JAVA_API_TRY_CATCH_BEGIN;
+  Sort* current = reinterpret_cast<Sort*>(pointer);
+  return static_cast<jboolean>(current->isInstantiated());
+  CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast<jboolean>(false));
+}
+
 /*
  * Class:     io_github_cvc5_api_Sort
  * Method:    getDatatype
@@ -826,22 +840,6 @@ JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Sort_getSequenceElementSort(
   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
 }
 
-/*
- * Class:     io_github_cvc5_api_Sort
- * Method:    isUninterpretedSortParameterized
- * Signature: (J)Z
- */
-JNIEXPORT jboolean JNICALL
-Java_io_github_cvc5_api_Sort_isUninterpretedSortParameterized(JNIEnv* env,
-                                                              jobject,
-                                                              jlong pointer)
-{
-  CVC5_JAVA_API_TRY_CATCH_BEGIN;
-  Sort* current = reinterpret_cast<Sort*>(pointer);
-  return static_cast<jboolean>(current->isUninterpretedSortParameterized());
-  CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast<jboolean>(false));
-}
-
 /*
  * Class:     io_github_cvc5_api_Sort
  * Method:    getUninterpretedSortParamSorts

diff --git a/src/api/python/cvc5.pxd b/src/api/python/cvc5.pxd
index 15fd5f3e9ed48fe82a73717631c857b4ea3a85d2..f03941c27d9af437eb30d78d1da3459fe2edbf67 100644 (file)
--- a/src/api/python/cvc5.pxd
+++ b/src/api/python/cvc5.pxd
@@ -397,6 +397,7 @@ cdef extern from "api/cpp/cvc5.h" namespace "cvc5::api":
         bint isSequence() except +
         bint isUninterpretedSort() except +
         bint isUninterpretedSortConstructor() except +
+        bint isInstantiated() except +
         Datatype getDatatype() except +
         Sort instantiate(const vector[Sort]& params) except +
         Sort substitute(const vector[Sort] & es, const vector[Sort] & reps) except +
@@ -415,7 +416,6 @@ cdef extern from "api/cpp/cvc5.h" namespace "cvc5::api":
         Sort getSetElementSort() except +
         Sort getBagElementSort() except +
         Sort getSequenceElementSort() except +
-        bint isUninterpretedSortParameterized() except +
         vector[Sort] getUninterpretedSortParamSorts() except +
         size_t getUninterpretedSortConstructorArity() except +
         uint32_t getBitVectorSize() except +

diff --git a/src/api/python/cvc5.pxi b/src/api/python/cvc5.pxi
index b9734761e3a2c33592195127cbe6260fc1f4af19..23fc5fa6948fe35cf709347affba5991a840d5fd 100644 (file)
--- a/src/api/python/cvc5.pxi
+++ b/src/api/python/cvc5.pxi
@@ -2806,6 +2806,19 @@ cdef class Sort:
         """
         return self.csort.isUninterpretedSortConstructor()
 
+    def isInstantiated(self):
+        """
+            Is this an instantiated (parametric datatype or uninterpreted sort
+            constructor) sort?
+
+            An instantiated sort is a sort that has been constructed from
+            instantiating a sort parameters with sort arguments
+            (see Sort::instantiate()).
+
+            :return: True if this is an instantiated sort.
+        """
+        return self.csort.isInstantiated()
+
     def getDatatype(self):
         """
             :return: the underlying datatype of a datatype sort
@@ -3004,12 +3017,6 @@ cdef class Sort:
         sort.csort = self.csort.getSequenceElementSort()
         return sort
 
-    def isUninterpretedSortParameterized(self):
-        """
-            :return: True if an uninterpreted sort is parameterized
-        """
-        return self.csort.isUninterpretedSortParameterized()
-
     def getUninterpretedSortParamSorts(self):
         """
             :return: the parameter sorts of an uninterpreted sort

diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp
index de85dfb06b51eb32dc03ffb01102b986b34e698a..a90efd055865557cc51b5dbcc7712347c4d30a7f 100644 (file)
--- a/src/expr/type_node.cpp
+++ b/src/expr/type_node.cpp
@@ -417,6 +417,12 @@ bool TypeNode::isInstantiatedDatatype() const {
   return true;
 }
 
+bool TypeNode::isInstantiated() const
+{
+  return isInstantiatedDatatype()
+         || (isSort() && getNumChildren() > 0);
+}
+
 TypeNode TypeNode::instantiateParametricDatatype(
     const std::vector<TypeNode>& params) const
 {

diff --git a/src/expr/type_node.h b/src/expr/type_node.h
index 9882c7fc53b9d886e7d7e4e73dec8cb2e9baf6db..8f8985d8650b664ca62b094d6ac2a1c4b45a1027 100644 (file)
--- a/src/expr/type_node.h
+++ b/src/expr/type_node.h
@@ -597,6 +597,12 @@ private:
   /** Is this a fully instantiated datatype type */
   bool isInstantiatedDatatype() const;
 
+  /**
+   * Return true if this is an instantiated parametric datatype or
+   * uninterpreted sort constructor type.
+   */
+  bool isInstantiated() const;
+
   /** Is this a sygus datatype type */
   bool isSygusDatatype() const;
 

diff --git a/test/unit/api/cpp/sort_black.cpp b/test/unit/api/cpp/sort_black.cpp
index 9a9368fbc9a5b744a1c0b9cdba40d28db71e43c2..37beffa90832f4a14ecb2391af5b42ca69405377 100644 (file)
--- a/test/unit/api/cpp/sort_black.cpp
+++ b/test/unit/api/cpp/sort_black.cpp
@@ -321,6 +321,28 @@ TEST_F(TestApiBlackSort, instantiate)
   ASSERT_THROW(
       dtypeSort.instantiate(std::vector<Sort>{d_solver.getIntegerSort()}),
       CVC5ApiException);
+  // instantiate uninterpreted sort constructor
+  Sort sortConsSort = d_solver.mkUninterpretedSortConstructorSort("s", 1);
+  ASSERT_NO_THROW(
+      sortConsSort.instantiate(std::vector<Sort>{d_solver.getIntegerSort()}));
+}
+
+TEST_F(TestApiBlackSort, isInstantiated)
+{
+  Sort paramDtypeSort = create_param_datatype_sort();
+  ASSERT_FALSE(paramDtypeSort.isInstantiated());
+  Sort instParamDtypeSort =
+      paramDtypeSort.instantiate(std::vector<Sort>{d_solver.getIntegerSort()});
+  ASSERT_TRUE(instParamDtypeSort.isInstantiated());
+
+  Sort sortConsSort = d_solver.mkUninterpretedSortConstructorSort("s", 1);
+  ASSERT_FALSE(sortConsSort.isInstantiated());
+  Sort instSortConsSort =
+      sortConsSort.instantiate(std::vector<Sort>{d_solver.getIntegerSort()});
+  ASSERT_TRUE(instSortConsSort.isInstantiated());
+
+  ASSERT_FALSE(d_solver.getIntegerSort().isInstantiated());
+  ASSERT_FALSE(d_solver.mkBitVectorSort(32).isInstantiated());
 }
 
 TEST_F(TestApiBlackSort, getFunctionArity)
@@ -406,17 +428,6 @@ TEST_F(TestApiBlackSort, getSymbol)
   ASSERT_THROW(bvSort.getSymbol(), CVC5ApiException);
 }
 
-TEST_F(TestApiBlackSort, isUninterpretedSortParameterized)
-{
-  Sort uSort = d_solver.mkUninterpretedSort("u");
-  ASSERT_FALSE(uSort.isUninterpretedSortParameterized());
-  Sort sSort = d_solver.mkUninterpretedSortConstructorSort("s", 1);
-  Sort siSort = sSort.instantiate({uSort});
-  ASSERT_TRUE(siSort.isUninterpretedSortParameterized());
-  Sort bvSort = d_solver.mkBitVectorSort(32);
-  ASSERT_THROW(bvSort.isUninterpretedSortParameterized(), CVC5ApiException);
-}
-
 TEST_F(TestApiBlackSort, getUninterpretedSortParamSorts)
 {
   Sort uSort = d_solver.mkUninterpretedSort("u");

diff --git a/test/unit/api/java/SortTest.java b/test/unit/api/java/SortTest.java
index 2115c027a961a4063abf56c6a86d9e2712f0ebf0..426b67a56ddb0cb17aa5ae5cde44fe7328b40dc8 100644 (file)
--- a/test/unit/api/java/SortTest.java
+++ b/test/unit/api/java/SortTest.java
@@ -311,6 +311,25 @@ class SortTest
     Sort dtypeSort = d_solver.mkDatatypeSort(dtypeSpec);
     assertThrows(CVC5ApiException.class,
         () -> dtypeSort.instantiate(new Sort[] {d_solver.getIntegerSort()}));
+    // instantiate uninterpreted sort constructor
+    Sort sortConsSort = d_solver.mkUninterpretedSortConstructorSort("s", 1);
+    assertDoesNotThrow(() -> sortConsSort.instantiate(new Sort[] {d_solver.getIntegerSort()}));
+  }
+
+  @Test void isInstantiated() throws CVC5ApiException
+  {
+    Sort paramDtypeSort = create_param_datatype_sort();
+    assertFalse(paramDtypeSort.isInstantiated());
+    Sort instParamDtypeSort = paramDtypeSort.instantiate(new Sort[] {d_solver.getIntegerSort()});
+    assertTrue(instParamDtypeSort.isInstantiated());
+
+    Sort sortConsSort = d_solver.mkUninterpretedSortConstructorSort("s", 1);
+    assertFalse(sortConsSort.isInstantiated());
+    Sort instSortConsSort = sortConsSort.instantiate(new Sort[] {d_solver.getIntegerSort()});
+    assertTrue(instSortConsSort.isInstantiated());
+
+    assertFalse(d_solver.getIntegerSort().isInstantiated());
+    assertFalse(d_solver.mkBitVectorSort(32).isInstantiated());
   }
 
   @Test void getFunctionArity() throws CVC5ApiException
@@ -396,17 +415,6 @@ class SortTest
     assertThrows(CVC5ApiException.class, () -> bvSort.getSymbol());
   }
 
-  @Test void isUninterpretedSortParameterized() throws CVC5ApiException
-  {
-    Sort uSort = d_solver.mkUninterpretedSort("u");
-    assertFalse(uSort.isUninterpretedSortParameterized());
-    Sort sSort = d_solver.mkUninterpretedSortConstructorSort("s", 1);
-    Sort siSort = sSort.instantiate(new Sort[] {uSort});
-    assertTrue(siSort.isUninterpretedSortParameterized());
-    Sort bvSort = d_solver.mkBitVectorSort(32);
-    assertThrows(CVC5ApiException.class, () -> bvSort.isUninterpretedSortParameterized());
-  }
-
   @Test void getUninterpretedSortParamSorts() throws CVC5ApiException
   {
     Sort uSort = d_solver.mkUninterpretedSort("u");

diff --git a/test/unit/api/python/test_sort.py b/test/unit/api/python/test_sort.py
index b530f2c37f914cdba8ae00ec213781cfe175f689..a78884a9316306661d47eae8e964feec107732ea 100644 (file)
--- a/test/unit/api/python/test_sort.py
+++ b/test/unit/api/python/test_sort.py
@@ -299,7 +299,23 @@ def test_instantiate(solver):
     dtypeSort = solver.mkDatatypeSort(dtypeSpec)
     with pytest.raises(RuntimeError):
         dtypeSort.instantiate([solver.getIntegerSort()])
+    # instantiate uninterpreted sort constructor
+    sortConsSort = solver.mkUninterpretedSortConstructorSort("s", 1)
+    sortConsSort.instantiate([solver.getIntegerSort()])
 
+def test_is_instantiated(solver):
+    paramDtypeSort = create_param_datatype_sort(solver)
+    assert not paramDtypeSort.isInstantiated()
+    instParamDtypeSort = paramDtypeSort.instantiate([solver.getIntegerSort()]);
+    assert instParamDtypeSort.isInstantiated()
+
+    sortConsSort = solver.mkUninterpretedSortConstructorSort("s", 1)
+    assert not sortConsSort.isInstantiated()
+    instSortConsSort = sortConsSort.instantiate([solver.getIntegerSort()])
+    assert instSortConsSort.isInstantiated()
+
+    assert not solver.getIntegerSort().isInstantiated()
+    assert not solver.mkBitVectorSort(32).isInstantiated()
 
 def test_get_function_arity(solver):
     funSort = solver.mkFunctionSort(solver.mkUninterpretedSort("u"),
@@ -384,17 +400,6 @@ def test_get_uninterpreted_sort_name(solver):
         bvSort.getSymbol()
 
 
-def test_is_uninterpreted_sort_parameterized(solver):
-    uSort = solver.mkUninterpretedSort("u")
-    assert not uSort.isUninterpretedSortParameterized()
-    sSort = solver.mkUninterpretedSortConstructorSort("s", 1)
-    siSort = sSort.instantiate([uSort])
-    assert siSort.isUninterpretedSortParameterized()
-    bvSort = solver.mkBitVectorSort(32)
-    with pytest.raises(RuntimeError):
-        bvSort.isUninterpretedSortParameterized()
-
-
 def test_get_uninterpreted_sort_paramsorts(solver):
     uSort = solver.mkUninterpretedSort("u")
     uSort.getUninterpretedSortParamSorts()