api: Add Sort::getUninterpretedSortConstructor(). (#8459)

This further introduces TypeNode::isInstantiatedUninterpretedSort().

diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp
index a0604537c1b895b9a3bdfb04ed6800f286cbb6b4..1d1e0f5ec388d41bd2835b4c2b0fb7cea48b2306 100644 (file)
--- a/src/api/cpp/cvc5.cpp
+++ b/src/api/cpp/cvc5.cpp
@@ -1386,6 +1386,18 @@ bool Sort::isUninterpretedSortConstructor() const
   CVC5_API_TRY_CATCH_END;
 }
 
+Sort Sort::getUninterpretedSortConstructor() const
+{
+  CVC5_API_TRY_CATCH_BEGIN;
+  CVC5_API_CHECK_NOT_NULL;
+  CVC5_API_CHECK(d_type->isInstantiatedUninterpretedSort())
+      << "Expected instantiated uninterpreted sort.";
+  //////// all checks before this line
+  return Sort(d_solver, d_type->getUninterpretedSortConstructor());
+  ////////
+  CVC5_API_TRY_CATCH_END;
+}
+
 Datatype Sort::getDatatype() const
 {
   CVC5_API_TRY_CATCH_BEGIN;

diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h
index 2ca093399999262c956e98850aa12b04ae418e57..d3b8fab56b7f4e6454e0e5a000f2a2b1d140707b 100644 (file)
--- a/src/api/cpp/cvc5.h
+++ b/src/api/cpp/cvc5.h
@@ -585,6 +585,14 @@ class CVC5_EXPORT Sort
    */
   bool isInstantiated() const;
 
+  /**
+   * Get the associated uninterpreted sort constructor of an instantiated
+   * uninterpreted sort.
+   *
+   * @return the uninterpreted sort constructor sort
+   */
+  Sort getUninterpretedSortConstructor() const;
+
   /**
    * @return the underlying datatype of a datatype sort
    */
@@ -758,7 +766,7 @@ class CVC5_EXPORT Sort
    */
   bool isUninterpretedSortParameterized() const;
 
-  /* Sort constructor sort ----------------------------------------------- */
+  /* Uninterpreted sort constructor sort --------------------------------- */
 
   /**
    * @return the arity of an uninterpreted sort 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 a8199330252c44e7a847719ca441197e6cf38f63..9f4cd1c9e7ce0711579edfcaf92efc3ee0cd7dac 100644 (file)
--- a/src/api/java/io/github/cvc5/api/Sort.java
+++ b/src/api/java/io/github/cvc5/api/Sort.java
@@ -379,6 +379,20 @@ public class Sort extends AbstractPointer implements Comparable<Sort>
 
   private native boolean isInstantiated(long pointer);
 
+  /**
+   * Get the associated uninterpreted sort constructor of an instantiated
+   * uninterpreted sort.
+   *
+   * @return the uninterpreted sort constructor sort
+   */
+  public Sort getUninterpretedSortConstructor()
+  {
+    long sortPointer = getUninterpretedSortConstructor(pointer);
+    return new Sort(solver, sortPointer);
+  }
+
+  private native long getUninterpretedSortConstructor(long pointer);
+
   /**
    * @return the underlying datatype of a datatype sort
    */

diff --git a/src/api/java/jni/sort.cpp b/src/api/java/jni/sort.cpp
index 0fc9f4574ce88c4cc910cb37f18fc23bc107204b..5f7d7302ac9581ff7976e3e4f21f9aac77d11fe3 100644 (file)
--- a/src/api/java/jni/sort.cpp
+++ b/src/api/java/jni/sort.cpp
@@ -492,6 +492,23 @@ Java_io_github_cvc5_api_Sort_getInstantiatedParameters(JNIEnv* env,
   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, nullptr);
 }
 
+/*
+ * Class:     io_github_cvc5_api_Sort
+ * Method:    getUninterpretedSortConstructor
+ * Signature: (J)J
+ */
+JNIEXPORT jlong JNICALL
+Java_io_github_cvc5_api_Sort_getUninterpretedSortConstructor(JNIEnv* env,
+                                                             jobject,
+                                                             jlong pointer)
+{
+  CVC5_JAVA_API_TRY_CATCH_BEGIN;
+  Sort* current = reinterpret_cast<Sort*>(pointer);
+  Sort* retPointer = new Sort(current->getUninterpretedSortConstructor());
+  return reinterpret_cast<jlong>(retPointer);
+  CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
+}
+
 /*
  * Class:     io_github_cvc5_api_Sort
  * Method:    getDatatype

diff --git a/src/api/python/cvc5.pxd b/src/api/python/cvc5.pxd
index ad354bb846a52d297eee0cb65ae00ac5e867b949..40a7b613f415f6b56c68195370c0fce4b3349f45 100644 (file)
--- a/src/api/python/cvc5.pxd
+++ b/src/api/python/cvc5.pxd
@@ -398,6 +398,7 @@ cdef extern from "api/cpp/cvc5.h" namespace "cvc5":
         bint isUninterpretedSort() except +
         bint isUninterpretedSortConstructor() except +
         bint isInstantiated() except +
+        Sort getUninterpretedSortConstructor() except +
         Datatype getDatatype() except +
         Sort instantiate(const vector[Sort]& params) except +
         vector[Sort] getInstantiatedParameters() except +

diff --git a/src/api/python/cvc5.pxi b/src/api/python/cvc5.pxi
index a8e5b13ef30713dcb0335361e995e3204889f65f..24f6f23b5747504c8caef86fd7b9cf348e1371b0 100644 (file)
--- a/src/api/python/cvc5.pxi
+++ b/src/api/python/cvc5.pxi
@@ -2919,6 +2919,17 @@ cdef class Sort:
         """
         return self.csort.isInstantiated()
 
+    def getUninterpretedSortConstructor(self):
+        """
+            Get the associated uninterpreted sort constructor of an
+            instantiated uninterpreted sort.
+
+            :return: the uninterpreted sort constructor sort
+        """
+        cdef Sort sort = Sort(self.solver)
+        sort.csort = self.csort.getUninterpretedSortConstructor()
+        return sort
+
     def getDatatype(self):
         """
             :return: the underlying datatype of a datatype sort

diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp
index 9b4fd46c103198d08ba539a16c944cc0c4927b4a..e84a7046d43994ab720a48e750e01ca9fd8925dd 100644 (file)
--- a/src/expr/type_node.cpp
+++ b/src/expr/type_node.cpp
@@ -422,10 +422,14 @@ bool TypeNode::isInstantiatedDatatype() const {
   return true;
 }
 
+bool TypeNode::isInstantiatedUninterpretedSort() const
+{
+  return isUninterpretedSort() && getNumChildren() > 0;
+}
+
 bool TypeNode::isInstantiated() const
 {
-  return isInstantiatedDatatype()
-         || (isUninterpretedSort() && getNumChildren() > 0);
+  return isInstantiatedDatatype() || isInstantiatedUninterpretedSort();
 }
 
 TypeNode TypeNode::instantiate(const std::vector<TypeNode>& params) const
@@ -461,6 +465,14 @@ std::string TypeNode::getName() const
   return getAttribute(expr::VarNameAttr());
 }
 
+TypeNode TypeNode::getUninterpretedSortConstructor() const
+{
+  Assert(isInstantiatedUninterpretedSort());
+  NodeBuilder nb(kind::SORT_TYPE);
+  nb << NodeManager::operatorFromType(*this);
+  return nb.constructTypeNode();
+}
+
 bool TypeNode::isParameterInstantiatedDatatype(size_t n) const
 {
   Assert(getKind() == kind::PARAMETRIC_DATATYPE);

diff --git a/src/expr/type_node.h b/src/expr/type_node.h
index 495f5b383ade030a6dc107c18055b8279e37b1f0..d8e7abd3839fc933c13949f499d2c00fc23b8f3f 100644 (file)
--- a/src/expr/type_node.h
+++ b/src/expr/type_node.h
@@ -370,7 +370,7 @@ private:
   }
 
   /**
-   * Very basic pretty printer for Node.
+   * Very basic pretty printer for TypeNode.
    *
    * @param out output stream to print to.
    * @param indent number of spaces to indent the formula by.
@@ -603,6 +603,12 @@ private:
   /** Is this a fully instantiated datatype type */
   bool isInstantiatedDatatype() const;
 
+  /**
+   * Is this an uninterpreted sort constructed from instantiating an
+   * uninterpreted sort constructor?
+   */
+  bool isInstantiatedUninterpretedSort() const;
+
   /**
    * Return true if this is an instantiated parametric datatype or
    * uninterpreted sort constructor type.
@@ -671,6 +677,14 @@ private:
    */
   std::string getName() const;
 
+  /**
+   * Get the uninterpreted sort constructor type this instantiated
+   * uninterpreted sort has been constructed from.
+   *
+   * Asserts that this is an instantiated uninterpreted sort.
+   */
+  TypeNode getUninterpretedSortConstructor() const;
+
   /** Get the most general base type of the type */
   TypeNode getBaseType() const;
 

diff --git a/test/unit/api/cpp/sort_black.cpp b/test/unit/api/cpp/sort_black.cpp
index 35c32e030eafa2c9efbb0c80268ce0c4d2ef6bab..759fd154359f88f9ccbfe0950a6b3edb9021c677 100644 (file)
--- a/test/unit/api/cpp/sort_black.cpp
+++ b/test/unit/api/cpp/sort_black.cpp
@@ -386,6 +386,20 @@ TEST_F(TestApiBlackSort, getInstantiatedParameters)
   ASSERT_THROW(bvSort.getInstantiatedParameters(), CVC5ApiException);
 }
 
+TEST_F(TestApiBlackSort, getUninterpretedSortConstructor)
+{
+  Sort intSort = d_solver.getIntegerSort();
+  Sort realSort = d_solver.getRealSort();
+  Sort boolSort = d_solver.getBooleanSort();
+  Sort bvSort = d_solver.mkBitVectorSort(8);
+  Sort sortConsSort = d_solver.mkUninterpretedSortConstructorSort("s", 4);
+  ASSERT_THROW(sortConsSort.getUninterpretedSortConstructor(),
+               CVC5ApiException);
+  Sort instSortConsSort =
+      sortConsSort.instantiate({boolSort, intSort, bvSort, realSort});
+  ASSERT_EQ(sortConsSort, instSortConsSort.getUninterpretedSortConstructor());
+}
+
 TEST_F(TestApiBlackSort, getFunctionArity)
 {
   Sort funSort = d_solver.mkFunctionSort(d_solver.mkUninterpretedSort("u"),

diff --git a/test/unit/api/java/SortTest.java b/test/unit/api/java/SortTest.java
index e2b3ff5aeee3d03decb5a5f7c83c98300331bdf8..b8071b77c2cde9650fa9cba119451f1925c6a257 100644 (file)
--- a/test/unit/api/java/SortTest.java
+++ b/test/unit/api/java/SortTest.java
@@ -379,6 +379,19 @@ class SortTest
     assertThrows(CVC5ApiException.class, () -> bvSort.getInstantiatedParameters());
   }
 
+  @Test void getUninterpretedSortConstructor() throws CVC5ApiException
+  {
+    Sort intSort = d_solver.getIntegerSort();
+    Sort realSort = d_solver.getRealSort();
+    Sort boolSort = d_solver.getBooleanSort();
+    Sort bvSort = d_solver.mkBitVectorSort(8);
+    Sort sortConsSort = d_solver.mkUninterpretedSortConstructorSort("s", 4);
+    assertThrows(CVC5ApiException.class, () -> sortConsSort.getUninterpretedSortConstructor());
+    Sort instSortConsSort =
+        sortConsSort.instantiate(new Sort[] {boolSort, intSort, bvSort, realSort});
+    assertEquals(sortConsSort, instSortConsSort.getUninterpretedSortConstructor());
+  }
+
   @Test void getFunctionArity() throws CVC5ApiException
   {
     Sort funSort =

diff --git a/test/unit/api/python/test_sort.py b/test/unit/api/python/test_sort.py
index 4c7743db940df9ab313ca38afdeccfdde7b3c94f..ab237505902d4becba0d61c641ef0aa02037f7a7 100644 (file)
--- a/test/unit/api/python/test_sort.py
+++ b/test/unit/api/python/test_sort.py
@@ -366,6 +366,18 @@ def test_get_instantiated_parameters(solver):
     with pytest.raises(RuntimeError):
         bvSort.getInstantiatedParameters()
 
+def test_get_uninterpreted_sort_constructor(solver):
+    intSort = solver.getIntegerSort()
+    realSort = solver.getRealSort()
+    boolSort = solver.getBooleanSort()
+    bvSort = solver.mkBitVectorSort(8)
+    sortConsSort = solver.mkUninterpretedSortConstructorSort("s", 4)
+    with pytest.raises(RuntimeError):
+        sortConsSort.getUninterpretedSortConstructor()
+    instSortConsSort = \
+        sortConsSort.instantiate([boolSort, intSort, bvSort, realSort]);
+    assert sortConsSort == instSortConsSort.getUninterpretedSortConstructor()
+
 def test_get_function_arity(solver):
     funSort = solver.mkFunctionSort(solver.mkUninterpretedSort("u"),
                                     solver.getIntegerSort())