From 1f5ccbacb0a578724a004e91934aa472783884c2 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 17 Dec 2021 12:22:13 -0600 Subject: [PATCH] Get getRealOrIntegerValueSign to the API (#7832) --- src/api/cpp/cvc5.cpp | 11 +++++++++++ src/api/cpp/cvc5.h | 7 +++++++ src/api/java/io/github/cvc5/api/Term.java | 13 +++++++++++++ src/api/java/jni/term.cpp | 16 ++++++++++++++++ src/api/python/cvc5.pxd | 1 + src/api/python/cvc5.pxi | 10 ++++++++++ test/unit/api/cpp/term_black.cpp | 3 +++ test/unit/api/java/TermTest.java | 3 +++ test/unit/api/python/test_term.py | 4 ++++ 9 files changed, 68 insertions(+) diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp index 71ce432fe..e9998c72b 100644 --- a/src/api/cpp/cvc5.cpp +++ b/src/api/cpp/cvc5.cpp @@ -2871,6 +2871,17 @@ bool isUInt64(const Node& node) } } // namespace detail +int32_t Term::getRealOrIntegerValueSign() const +{ + CVC5_API_TRY_CATCH_BEGIN; + CVC5_API_CHECK_NOT_NULL; + //////// all checks before this line + const Rational& r = detail::getRational(*d_node); + return static_cast(r.sgn()); + //////// + CVC5_API_TRY_CATCH_END; +} + bool Term::isInt32Value() const { CVC5_API_TRY_CATCH_BEGIN; diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h index 3904a553c..e29729c06 100644 --- a/src/api/cpp/cvc5.h +++ b/src/api/cpp/cvc5.h @@ -1340,6 +1340,13 @@ class CVC5_EXPORT Term */ const_iterator end() const; + /** + * Get integer or real value sign. Must be called on integer or real values, + * or otherwise an exception is thrown. + * @return 0 if this term is zero, -1 if this term is a negative real or + * integer value, 1 if this term is a positive real or integer value. + */ + int32_t getRealOrIntegerValueSign() const; /** * @return true if the term is an integer value that fits within int32_t. */ diff --git a/src/api/java/io/github/cvc5/api/Term.java b/src/api/java/io/github/cvc5/api/Term.java index db780f9bd..f6897d59b 100644 --- a/src/api/java/io/github/cvc5/api/Term.java +++ b/src/api/java/io/github/cvc5/api/Term.java @@ -334,6 +334,19 @@ public class Term extends AbstractPointer implements Comparable, Iterable< */ protected native String toString(long pointer); + /** + * Get integer or real value sign. Must be called on integer or real values, + * or otherwise an exception is thrown. + * @return 0 if this term is zero, -1 if this term is a negative real or + * integer value, 1 if this term is a positive real or integer value. + */ + public int getRealOrIntegerValueSign() + { + return getRealOrIntegerValueSign(pointer); + } + + private native int getRealOrIntegerValueSign(long pointer); + /** * @return true if the term is an integer value. */ diff --git a/src/api/java/jni/term.cpp b/src/api/java/jni/term.cpp index 702a5064d..1e8669873 100644 --- a/src/api/java/jni/term.cpp +++ b/src/api/java/jni/term.cpp @@ -457,6 +457,22 @@ JNIEXPORT jstring JNICALL Java_io_github_cvc5_api_Term_toString(JNIEnv* env, CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, nullptr); } +/* + * Class: io_github_cvc5_api_Term + * Method: getRealOrIntegerValueSign + * Signature: (J)Z + */ +JNIEXPORT jint JNICALL +Java_io_github_cvc5_api_Term_getRealOrIntegerValueSign(JNIEnv* env, + jobject, + jlong pointer) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Term* current = reinterpret_cast(pointer); + return static_cast(current->getRealOrIntegerValueSign()); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast(0)); +} + /* * Class: io_github_cvc5_api_Term * Method: isIntegerValue diff --git a/src/api/python/cvc5.pxd b/src/api/python/cvc5.pxd index e283fb7b6..5a33628a6 100644 --- a/src/api/python/cvc5.pxd +++ b/src/api/python/cvc5.pxd @@ -421,6 +421,7 @@ cdef extern from "api/cpp/cvc5.h" namespace "cvc5::api": bint getBooleanValue() except + bint isStringValue() except + wstring getStringValue() except + + int32_t getRealOrIntegerValueSign() except + bint isIntegerValue() except + string getIntegerValue() except + bint isRealValue() except + diff --git a/src/api/python/cvc5.pxi b/src/api/python/cvc5.pxi index 88d69c26a..d3f58ce62 100644 --- a/src/api/python/cvc5.pxi +++ b/src/api/python/cvc5.pxi @@ -3043,6 +3043,16 @@ cdef class Term: cdef c_wstring s = self.cterm.getStringValue() return PyUnicode_FromWideChar(s.data(), s.size()) + def getRealOrIntegerValueSign(self): + """ + Get integer or real value sign. Must be called on integer or real values, + or otherwise an exception is thrown. + + :return: 0 if this term is zero, -1 if this term is a negative real or + integer value, 1 if this term is a positive real or integer value. + """ + return self.cterm.getRealOrIntegerValueSign() + def isIntegerValue(self): """:return: True iff this term is an integer value.""" return self.cterm.isIntegerValue() diff --git a/test/unit/api/cpp/term_black.cpp b/test/unit/api/cpp/term_black.cpp index c76182e47..bb57612b2 100644 --- a/test/unit/api/cpp/term_black.cpp +++ b/test/unit/api/cpp/term_black.cpp @@ -708,6 +708,7 @@ TEST_F(TestApiBlackTerm, getInteger) && !int1.isInt64Value() && !int1.isUInt64Value() && int1.isIntegerValue()); ASSERT_EQ(int1.getIntegerValue(), "-18446744073709551616"); + ASSERT_TRUE(int1.getRealOrIntegerValueSign() == -1); ASSERT_TRUE(!int2.isInt32Value() && !int2.isUInt32Value() && !int2.isInt64Value() && !int2.isUInt64Value() && int2.isIntegerValue()); @@ -735,6 +736,7 @@ TEST_F(TestApiBlackTerm, getInteger) ASSERT_EQ(int6.getInt64Value(), 0); ASSERT_EQ(int6.getUInt64Value(), 0); ASSERT_EQ(int6.getIntegerValue(), "0"); + ASSERT_TRUE(int6.getRealOrIntegerValueSign() == 0); ASSERT_TRUE(int7.isInt32Value() && int7.isUInt32Value() && int7.isInt64Value() && int7.isUInt64Value() && int7.isIntegerValue()); ASSERT_EQ(int7.getInt32Value(), 10); @@ -742,6 +744,7 @@ TEST_F(TestApiBlackTerm, getInteger) ASSERT_EQ(int7.getInt64Value(), 10); ASSERT_EQ(int7.getUInt64Value(), 10); ASSERT_EQ(int7.getIntegerValue(), "10"); + ASSERT_TRUE(int7.getRealOrIntegerValueSign() == 1); ASSERT_TRUE(!int8.isInt32Value() && int8.isUInt32Value() && int8.isInt64Value() && int8.isUInt64Value() && int8.isIntegerValue()); diff --git a/test/unit/api/java/TermTest.java b/test/unit/api/java/TermTest.java index b7f111428..ad84bb18d 100644 --- a/test/unit/api/java/TermTest.java +++ b/test/unit/api/java/TermTest.java @@ -713,6 +713,7 @@ class TermTest assertTrue(int1.isIntegerValue()); assertEquals(int1.getIntegerValue().toString(), "-18446744073709551616"); + assertEquals(int1.getRealOrIntegerValueSign(), -1); assertTrue(int2.isIntegerValue()); assertEquals(int2.getIntegerValue().toString(), "-18446744073709551615"); assertTrue(int3.isIntegerValue()); @@ -729,10 +730,12 @@ class TermTest assertEquals(int6.getIntegerValue().intValue(), 0); assertEquals(int6.getIntegerValue().intValue(), 0); assertEquals(int6.getIntegerValue().toString(), "0"); + assertEquals(int6.getRealOrIntegerValueSign(), 0); assertTrue(int7.isIntegerValue()); assertEquals(int7.getIntegerValue().intValue(), 10); assertEquals(int7.getIntegerValue().intValue(), 10); assertEquals(int7.getIntegerValue().toString(), "10"); + assertEquals(int7.getRealOrIntegerValueSign(), 1); assertTrue(int8.isIntegerValue()); assertEquals(int8.getIntegerValue().longValue(), 4294967295L); assertEquals(int8.getIntegerValue().toString(), "4294967295"); diff --git a/test/unit/api/python/test_term.py b/test/unit/api/python/test_term.py index 27702bd23..cc15a3181 100644 --- a/test/unit/api/python/test_term.py +++ b/test/unit/api/python/test_term.py @@ -1132,6 +1132,10 @@ def test_is_integer(solver): assert int9.getIntegerValue() == 4294967296 assert int10.getIntegerValue() == 18446744073709551615 assert int11.getIntegerValue() == 18446744073709551616 + + assert int1.getRealOrIntegerValueSign() == -1 + assert int6.getRealOrIntegerValueSign() == 0 + assert int7.getRealOrIntegerValueSign() == 1 def test_get_string(solver): -- 2.30.2