From: yoni206 <yoni206@users.noreply.github.com>
Date: Tue, 1 Jun 2021 09:40:54 +0000 (-0700)
Subject: FP value support in python API (#6644)
X-Git-Tag: cvc5-1.0.0~1670
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=e7dccb880f08e14004501c827cd1c199a936cb64;p=cvc5.git

FP value support in python API (#6644)

This PR adds new is* functions from the cpp API to the python API.
In particular, it adds getFloatingPointValue() function from the cpp API.
A test (translated from term_black.cpp) is added.

getFloatingPointValue() returns a tuple, and so this requires importing an instance of tuples into cython.
---

diff --git a/src/api/python/cvc5.pxd b/src/api/python/cvc5.pxd
index ef65c9070..87a646666 100644
--- a/src/api/python/cvc5.pxd
+++ b/src/api/python/cvc5.pxd
@@ -27,6 +27,15 @@ cdef extern from "<string>" namespace "std":
         const wchar_t* data() except +
         size_t size() except +
 
+cdef extern from "<tuple>" namespace "std" nogil:
+    cdef cppclass tuple[T, U, S]:
+        pass
+
+cdef extern from "<tuple>" namespace "std":
+    uint32_t get0 "std::get<0>"(tuple[uint32_t,uint32_t,Term]) except +
+    uint32_t get1 "std::get<1>"(tuple[uint32_t,uint32_t,Term]) except +
+    Term get2 "std::get<2>"(tuple[uint32_t,uint32_t,Term]) except +
+
 cdef extern from "api/cpp/cvc5.h" namespace "cvc5":
     cdef cppclass Options:
         pass
@@ -387,6 +396,14 @@ cdef extern from "api/cpp/cvc5.h" namespace "cvc5::api":
         string getRealValue() except +
         bint isBitVectorValue() except +
         string getBitVectorValue(uint32_t base) except +
+        bint isFloatingPointPosZero() except +
+        bint isFloatingPointNegZero() except +
+        bint isFloatingPointPosInf() except +
+        bint isFloatingPointNegInf() except +
+        bint isFloatingPointNaN() except +
+        bint isFloatingPointValue() except +
+
+        tuple[uint32_t, uint32_t, Term] getFloatingPointValue() except +
         vector[Term] getSequenceValue() except +
 
     cdef cppclass TermHashFunction:
diff --git a/src/api/python/cvc5.pxi b/src/api/python/cvc5.pxi
index 7731f4e71..cd9e91e51 100644
--- a/src/api/python/cvc5.pxi
+++ b/src/api/python/cvc5.pxi
@@ -28,7 +28,8 @@ from cvc5 cimport ROUND_NEAREST_TIES_TO_AWAY
 from cvc5 cimport Term as c_Term
 from cvc5 cimport hash as c_hash
 from cvc5 cimport wstring as c_wstring
-
+from cvc5 cimport tuple as c_tuple
+from cvc5 cimport get0, get1, get2
 from cvc5kinds cimport Kind as c_Kind
 
 cdef extern from "Python.h":
@@ -1661,6 +1662,30 @@ cdef class Term:
 
     def isIntegerValue(self):
         return self.cterm.isIntegerValue()
+    
+    def isFloatingPointPosZero(self):
+        return self.cterm.isFloatingPointPosZero()
+    
+    def isFloatingPointNegZero(self):
+        return self.cterm.isFloatingPointNegZero()
+    
+    def isFloatingPointPosInf(self):
+        return self.cterm.isFloatingPointPosInf()
+    
+    def isFloatingPointNegInf(self):
+        return self.cterm.isFloatingPointNegInf()
+    
+    def isFloatingPointNaN(self):
+        return self.cterm.isFloatingPointNaN()
+    
+    def isFloatingPointValue(self):
+        return self.cterm.isFloatingPointValue()
+
+    def getFloatingPointValue(self):
+        cdef c_tuple[uint32_t, uint32_t, c_Term] t = self.cterm.getFloatingPointValue()
+        cdef Term term = Term(self.solver)
+        term.cterm = get2(t)
+        return (get0(t), get1(t), term)
 
     def getIntegerValue(self):
         return int(self.cterm.getIntegerValue().decode())
diff --git a/test/python/unit/api/test_term.py b/test/python/unit/api/test_term.py
index 2b6fd8fd6..5603655c6 100644
--- a/test/python/unit/api/test_term.py
+++ b/test/python/unit/api/test_term.py
@@ -930,6 +930,25 @@ def test_term_children(solver):
         tnull[0]
 
 
+def test_get_floating_point(solver):
+    bvval = solver.mkBitVector("0000110000000011")
+    fp = solver.mkFloatingPoint(5, 11, bvval)
+
+    assert fp.isFloatingPointValue()
+    assert not fp.isFloatingPointPosZero()
+    assert not fp.isFloatingPointNegZero()
+    assert not fp.isFloatingPointPosInf()
+    assert not fp.isFloatingPointNegInf()
+    assert not fp.isFloatingPointNaN()
+    assert (5, 11, bvval) == fp.getFloatingPointValue()
+
+    assert solver.mkPosZero(5, 11).isFloatingPointPosZero()
+    assert solver.mkNegZero(5, 11).isFloatingPointNegZero()
+    assert solver.mkPosInf(5, 11).isFloatingPointPosInf()
+    assert solver.mkNegInf(5, 11).isFloatingPointNegInf()
+    assert solver.mkNaN(5, 11).isFloatingPointNaN()
+
+
 def test_is_integer(solver):
     int1 = solver.mkInteger("-18446744073709551616")
     int2 = solver.mkInteger("-18446744073709551615")
@@ -1018,11 +1037,11 @@ def test_get_real(solver):
     assert 0 == real1.getRealValue()
     assert 0 == real2.getRealValue()
     assert -17 == real3.getRealValue()
-    assert -3/5 == real4.getRealValue()
-    assert 127/10 == real5.getRealValue()
-    assert 1/4294967297 == real6.getRealValue()
+    assert -3 / 5 == real4.getRealValue()
+    assert 127 / 10 == real5.getRealValue()
+    assert 1 / 4294967297 == real6.getRealValue()
     assert 4294967297 == real7.getRealValue()
-    assert 1/18446744073709551617 == real8.getRealValue()
+    assert 1 / 18446744073709551617 == real8.getRealValue()
     assert float(18446744073709551617) == real9.getRealValue()