From 94c5c54989a7ddbff74c7d7e497e4725c2b36fa7 Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Thu, 16 Dec 2021 10:50:01 -0800 Subject: [PATCH] api: Add Sort::hasSymbol() and Sort::getSymbol(). (#7825) --- src/api/cpp/cvc5.cpp | 23 +++++++++++++++++ src/api/cpp/cvc5.h | 11 +++++++++ src/api/java/io/github/cvc5/api/Sort.java | 21 ++++++++++++++++ src/api/java/jni/sort.cpp | 30 +++++++++++++++++++++++ src/api/python/cvc5.pxd | 2 ++ src/api/python/cvc5.pxi | 18 +++++++++++--- test/unit/api/cpp/sort_black.cpp | 18 ++++++++++++++ test/unit/api/java/SortTest.java | 18 ++++++++++++++ test/unit/api/python/test_sort.py | 20 +++++++++++++++ 9 files changed, 158 insertions(+), 3 deletions(-) diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp index 4202a7fab..a9f7d884a 100644 --- 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 ec7b92088..a4ba3ee90 100644 --- 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 6bd87a9af..d8c162c10 100644 --- 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 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 2c7ee4fd0..ea3a70bd4 100644 --- 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(pointer); + return static_cast(current->hasSymbol()); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast(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(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 2baed575a..8b9a88adc 100644 --- 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 5c75047ef..2bf72e913 100644 --- 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 d0c755cf7..108b24670 100644 --- 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 977ba483e..511bb6534 100644 --- 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 9c9458792..a0a2cbea8 100644 --- 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() -- 2.30.2