api: Add Sort::hasSymbol() and Sort::getSymbol(). (#7825)

diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp
index 4202a7fabe2886621dafe4134b4b620e5d38e529..a9f7d884a0ae0e78b1a67be249fedcf8f666d9ac 100644 (file)
--- a/src/api/cpp/cvc5.cpp
+++ b/src/api/cpp/cvc5.cpp
@@ -1111,6 +1111,29 @@ bool Sort::operator>=(const Sort& s) const
   CVC5_API_TRY_CATCH_END;
 }
 
+bool Sort::hasSymbol() const
+{
+  CVC5_API_TRY_CATCH_BEGIN;
+  CVC5_API_CHECK_NOT_NULL;
+  //////// all checks before this line
+  return d_type->hasAttribute(expr::VarNameAttr());
+  ////////
+  CVC5_API_TRY_CATCH_END;
+}
+
+std::string Sort::getSymbol() const
+{
+  CVC5_API_TRY_CATCH_BEGIN;
+  CVC5_API_CHECK_NOT_NULL;
+  CVC5_API_CHECK(d_type->hasAttribute(expr::VarNameAttr()))
+      << "Invalid call to '" << __PRETTY_FUNCTION__
+      << "', expected the sort to have a symbol.";
+  //////// all checks before this line
+  return d_type->getAttribute(expr::VarNameAttr());
+  ////////
+  CVC5_API_TRY_CATCH_END;
+}
+
 bool Sort::isNull() const
 {
   CVC5_API_TRY_CATCH_BEGIN;

diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h
index ec7b92088571ed36574bd25f42151656ed8e8ab1..a4ba3ee90578dffa5d10a2661f46ac58feb84aab 100644 (file)
--- a/src/api/cpp/cvc5.h
+++ b/src/api/cpp/cvc5.h
@@ -375,6 +375,17 @@ class CVC5_EXPORT Sort
    */
   bool operator>=(const Sort& s) const;
 
+  /**
+   * @return true if the sort has a symbol.
+   */
+  bool hasSymbol() const;
+
+  /**
+   * Asserts hasSymbol().
+   * @return the raw symbol of the sort.
+   */
+  std::string getSymbol() const;
+
   /**
    * @return true if this Sort is a null sort.
    */

diff --git a/src/api/java/io/github/cvc5/api/Sort.java b/src/api/java/io/github/cvc5/api/Sort.java
index 6bd87a9af36ad81dcc508a51e924deee07fa4807..d8c162c10279be2fbc59adc113e94d1dbcb16da9 100644 (file)
--- a/src/api/java/io/github/cvc5/api/Sort.java
+++ b/src/api/java/io/github/cvc5/api/Sort.java
@@ -69,6 +69,27 @@ public class Sort extends AbstractPointer implements Comparable<Sort>
 
   private native int compareTo(long pointer1, long pointer2);
 
+  /**
+   * @return true if the sort has a symbol.
+   */
+  public boolean hasSymbol()
+  {
+    return hasSymbol(pointer);
+  }
+
+  private native boolean hasSymbol(long pointer);
+
+  /**
+   * Asserts hasSymbol().
+   * @return the raw symbol of the symbol.
+   */
+  public String getSymbol()
+  {
+    return getSymbol(pointer);
+  }
+
+  private native String getSymbol(long pointer);
+
   /**
    * @return true if this Sort is a null sort.
    */

diff --git a/src/api/java/jni/sort.cpp b/src/api/java/jni/sort.cpp
index 2c7ee4fd0f39c2aad740d69a1f173d7f0a04ea60..ea3a70bd421c47c26cb07efb331d52629882a98b 100644 (file)
--- a/src/api/java/jni/sort.cpp
+++ b/src/api/java/jni/sort.cpp
@@ -73,6 +73,36 @@ JNIEXPORT jint JNICALL Java_io_github_cvc5_api_Sort_compareTo(JNIEnv* env,
   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
 }
 
+/*
+ * Class:     io_github_cvc5_api_Sort
+ * Method:    hasSymbol
+ * Signature: (J)Z
+ */
+JNIEXPORT jboolean JNICALL Java_io_github_cvc5_api_Sort_hasSymbol(JNIEnv* env,
+                                                                  jobject,
+                                                                  jlong pointer)
+{
+  CVC5_JAVA_API_TRY_CATCH_BEGIN;
+  Sort* current = reinterpret_cast<Sort*>(pointer);
+  return static_cast<jboolean>(current->hasSymbol());
+  CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast<jboolean>(false));
+}
+
+/*
+ * Class:     io_github_cvc5_api_Sort
+ * Method:    getSymbol
+ * Signature: (J)Ljava/lang/String;
+ */
+JNIEXPORT jstring JNICALL Java_io_github_cvc5_api_Sort_getSymbol(JNIEnv* env,
+                                                                 jobject,
+                                                                 jlong pointer)
+{
+  CVC5_JAVA_API_TRY_CATCH_BEGIN;
+  Sort* current = reinterpret_cast<Sort*>(pointer);
+  return env->NewStringUTF(current->getSymbol().c_str());
+  CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, nullptr);
+}
+
 /*
  * Class:     io_github_cvc5_api_Sort
  * Method:    isNull

diff --git a/src/api/python/cvc5.pxd b/src/api/python/cvc5.pxd
index 2baed575a8c8fda6286f2798869f69e19a46550e..8b9a88adcf843bcf04d932d2a9a171ed6743df10 100644 (file)
--- a/src/api/python/cvc5.pxd
+++ b/src/api/python/cvc5.pxd
@@ -311,6 +311,8 @@ cdef extern from "api/cpp/cvc5.h" namespace "cvc5::api":
         bint operator>(const Sort&) except +
         bint operator<=(const Sort&) except +
         bint operator>=(const Sort&) except +
+        bint hasSymbol() except +
+        string getSymbol() except +
         bint isNull() except +
         bint isBoolean() except +
         bint isInteger() except +

diff --git a/src/api/python/cvc5.pxi b/src/api/python/cvc5.pxi
index 5c75047ef79d9a73c9dd16105b0129f28a546d73..2bf72e913531a4b1797a8b53bfb42eaaa49c792e 100644 (file)
--- a/src/api/python/cvc5.pxi
+++ b/src/api/python/cvc5.pxi
@@ -2237,6 +2237,18 @@ cdef class Sort:
     def __hash__(self):
         return csorthash(self.csort)
 
+    def hasSymbol(self):
+        """:return: True iff this sort has a symbol."""
+        return self.csort.hasSymbol()
+
+    def getSymbol(self):
+        """
+        Asserts :py:meth:`hasSymbol()`.
+
+        :return: the raw symbol of the sort.
+        """
+        return self.csort.getSymbol().decode()
+
     def isNull(self):
         """:return: True if this Sort is a null sort."""
         return self.csort.isNull()
@@ -2883,10 +2895,10 @@ cdef class Term:
 
     def getSymbol(self):
         """
-          Asserts :py:meth:`hasSymbol()`.
+        Asserts :py:meth:`hasSymbol()`.
 
-          :return: the raw symbol of the term.
-       """
+        :return: the raw symbol of the term.
+        """
         return self.cterm.getSymbol().decode()
 
     def isNull(self):

diff --git a/test/unit/api/cpp/sort_black.cpp b/test/unit/api/cpp/sort_black.cpp
index d0c755cf76c7ff520fa14acb9c8b82f1d3476881..108b2467093fcda0695613aee181d40ceeb71359 100644 (file)
--- a/test/unit/api/cpp/sort_black.cpp
+++ b/test/unit/api/cpp/sort_black.cpp
@@ -61,6 +61,24 @@ TEST_F(TestApiBlackSort, operators_comparison)
   ASSERT_NO_THROW(d_solver.getIntegerSort() >= Sort());
 }
 
+TEST_F(TestApiBlackSort, hasGetSymbol)
+{
+  Sort n;
+  Sort b = d_solver.getBooleanSort();
+  Sort s0 = d_solver.mkParamSort("s0");
+  Sort s1 = d_solver.mkParamSort("|s1\\|");
+
+  ASSERT_THROW(n.hasSymbol(), CVC5ApiException);
+  ASSERT_FALSE(b.hasSymbol());
+  ASSERT_TRUE(s0.hasSymbol());
+  ASSERT_TRUE(s1.hasSymbol());
+
+  ASSERT_THROW(n.getSymbol(), CVC5ApiException);
+  ASSERT_THROW(b.getSymbol(), CVC5ApiException);
+  ASSERT_EQ(s0.getSymbol(), "s0");
+  ASSERT_EQ(s1.getSymbol(), "|s1\\|");
+}
+
 TEST_F(TestApiBlackSort, isNull)
 {
   Sort x;

diff --git a/test/unit/api/java/SortTest.java b/test/unit/api/java/SortTest.java
index 977ba483e102203f8cfcf661dfd997b96c067e67..511bb65345f321e8be9dae713d1e5e13db9f0b95 100644 (file)
--- a/test/unit/api/java/SortTest.java
+++ b/test/unit/api/java/SortTest.java
@@ -72,6 +72,24 @@ class SortTest
     assertDoesNotThrow(() -> d_solver.getIntegerSort().compareTo(d_solver.getNullSort()));
   }
 
+  @Test void hasGetSymbol() throws CVC5ApiException
+  {
+    Sort n = d_solver.getNullSort();
+    Sort b = d_solver.getBooleanSort();
+    Sort s0 = d_solver.mkParamSort("s0");
+    Sort s1 = d_solver.mkParamSort("|s1\\|");
+
+    assertThrows(CVC5ApiException.class, () -> n.hasSymbol());
+    assertFalse(b.hasSymbol());
+    assertTrue(s0.hasSymbol());
+    assertTrue(s1.hasSymbol());
+
+    assertThrows(CVC5ApiException.class, () -> n.getSymbol());
+    assertThrows(CVC5ApiException.class, () -> b.getSymbol());
+    assertEquals(s0.getSymbol(), "s0");
+    assertEquals(s1.getSymbol(), "|s1\\|");
+  }
+
   @Test void isBoolean()
   {
     assertTrue(d_solver.getBooleanSort().isBoolean());

diff --git a/test/unit/api/python/test_sort.py b/test/unit/api/python/test_sort.py
index 9c945879270adf49a28f9eadb69ebf83e640d9f9..a0a2cbea8693b55594c59466c7c790db03248721 100644 (file)
--- a/test/unit/api/python/test_sort.py
+++ b/test/unit/api/python/test_sort.py
@@ -59,6 +59,26 @@ def test_operators_comparison(solver):
     solver.getIntegerSort() > Sort(solver)
     solver.getIntegerSort() >= Sort(solver)
 
+def test_has_get_symbol(solver):
+    n = Sort(solver)
+    b = solver.getBooleanSort()
+    s0 = solver.mkParamSort("s0")
+    s1 = solver.mkParamSort("|s1\\|")
+
+    with pytest.raises(RuntimeError):
+        n.hasSymbol()
+    assert not b.hasSymbol()
+    assert s0.hasSymbol()
+    assert s1.hasSymbol()
+
+    with pytest.raises(RuntimeError):
+        n.getSymbol()
+    with pytest.raises(RuntimeError):
+        b.getSymbol()
+    assert s0.getSymbol() == "s0"
+    assert s1.getSymbol() == "|s1\\|"
+
+
 def test_is_null(solver):
    x = Sort(solver)
    assert x.isNull()