Get getRealOrIntegerValueSign to the API (#7832)

diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp
index 71ce432fe729731cf1a4f91a929560faadb42ad8..e9998c72be55932d6f75c807e123588396620bff 100644 (file)
--- 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<int32_t>(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 3904a553ca379353dcb39932aa456d2831d46870..e29729c069fc4b8b96d57206eb9d0746d544a157 100644 (file)
--- 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 db780f9bdd8efa8f2d5de8948059a9e6f6605088..f6897d59bca3c25b96ad0c1eaea5b9d83762f31c 100644 (file)
--- 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<Term>, 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 702a5064d408895f55b9c01349871eabe070c621..1e8669873eb1938db1b75411df1acbee4cc2ccb3 100644 (file)
--- 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<Term*>(pointer);
+  return static_cast<jint>(current->getRealOrIntegerValueSign());
+  CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast<jint>(0));
+}
+
 /*
  * Class:     io_github_cvc5_api_Term
  * Method:    isIntegerValue

diff --git a/src/api/python/cvc5.pxd b/src/api/python/cvc5.pxd
index e283fb7b65fa7a6161747ce6994932b252ba1fcd..5a33628a6eedbcc193af802706b902a3f2a7e2ce 100644 (file)
--- 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 88d69c26adc2349b55fb3e955a702da21879a976..d3f58ce620bcab7f2f8adb5be0a7b21ab02d44e5 100644 (file)
--- 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 c76182e479e597eb4a18941f277096aecded71d5..bb57612b221f758b6e7c0a9e5d5c75716097066d 100644 (file)
--- 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 b7f11142807c20f61bb48572579020866c963364..ad84bb18d56c41a4ab781cbd71d775597653096f 100644 (file)
--- 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 27702bd23378170c44c63c2f0c9e6f85d931b5ee..cc15a3181a38d1a68a220ee1ca7d9cb6363b4b2e 100644 (file)
--- 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):