Fix getKind for Python bindings (#4496)

I noticed recently that getKind for Op and Term was not correct in the python bindings. This PR would add maps to keep track of the Kind objects and the Python names (which are different from the C++ Kind names). Then a Python `kind` only needs the integer representation of a `Kind` to be constructed. Now, in `getKind` it can just pass the integer representation when constructing a `kind`.

diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index 810f4b925eab9ef4c9f5c13eae039128938aa40a..35154828f87d00100eb1a80791e210eb169e69b8 100644 (file)
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -82,6 +82,12 @@ jobs:
         python3 -m pip install \
           Cython==0.29 --install-option="--no-cython-compile"
 
+    - name: Install Pytest
+      if: matrix.python-bindings
+      run: |
+        python3 -m pip install pytest
+        python3 -m pytest --version
+
     - name: Restore Dependencies
       id: restore-deps
       uses: actions/cache@v1
@@ -160,6 +166,12 @@ jobs:
        export PYTHONPATH="$PYTHONPATH:$(dirname $(find build/install/ -name "pycvc4" -type d))"
        python3 -c "import pycvc4"
 
+    - name: Run Pytest
+      if: matrix.python-bindings
+      run: |
+       export PYTHONPATH="$PYTHONPATH:$(dirname $(find build/install/ -name "pycvc4" -type d))"
+       python3 -m pytest ./test/unit/api/python
+
       # Examples are built for non-symfpu builds
     - name: Check Examples
       if: matrix.check-examples && runner.os == 'Linux'

diff --git a/src/api/python/cvc4.pxd b/src/api/python/cvc4.pxd
index 624b3c365f01abf92d1543af062c04418a0d7346..eb4254560aadcf99f950e37a5a6647b9a9812af7 100644 (file)
--- a/src/api/python/cvc4.pxd
+++ b/src/api/python/cvc4.pxd
@@ -250,6 +250,7 @@ cdef extern from "api/cvc4cpp.h" namespace "CVC4::api":
         bint hasOp() except +
         Op getOp() except +
         bint isNull() except +
+        bint isConst() except +
         Term getConstArrayBase() except +
         Term notTerm() except +
         Term andTerm(const Term& t) except +

diff --git a/src/api/python/cvc4.pxi b/src/api/python/cvc4.pxi
index b7593f6f1366b168b91fbe37c7dd10214b9479b9..5abbfb1136a4e9210bde216cb57ccfd0326770b5 100644 (file)
--- a/src/api/python/cvc4.pxi
+++ b/src/api/python/cvc4.pxi
@@ -1100,6 +1100,9 @@ cdef class Term:
     def isNull(self):
         return self.cterm.isNull()
 
+    def isConst(self):
+        return self.cterm.isConst()
+
     def getConstArrayBase(self):
         cdef Term term = Term()
         term.cterm = self.cterm.getConstArrayBase()

diff --git a/src/api/python/genkinds.py b/src/api/python/genkinds.py
index 4fe7347e6e6a1b012e22c4837b7b201179034d81..a12c9735c7543b7f550d8d62a29ce8fa03f4910c 100755 (executable)
--- a/src/api/python/genkinds.py
+++ b/src/api/python/genkinds.py
@@ -69,11 +69,21 @@ from cvc4kinds cimport *
 import sys
 from types import ModuleType
 
+from libcpp.string cimport string
+from libcpp.unordered_map cimport unordered_map
+
+# these maps are used for creating a kind
+# it is needed for dynamically making a kind
+# e.g. for getKind()
+cdef unordered_map[int, Kind] int2kind
+cdef unordered_map[int, string] int2name
+
 cdef class kind:
     cdef Kind k
     cdef str name
-    def __cinit__(self, str name):
-        self.name = name
+    def __cinit__(self, int kindint):
+        self.k = int2kind[kindint]
+        self.name = int2name[kindint].decode()
 
     def __eq__(self, kind other):
         return (<int> self.k) == (<int> other.k)
@@ -100,8 +110,9 @@ kinds.__file__ = kinds.__name__ + ".py"
 
 KINDS_ATTR_TEMPLATE = \
 r"""
-cdef kind {name} = kind("{name}")
-{name}.k = {kind}
+int2kind[<int> {kind}] = {kind}
+int2name[<int> {kind}] = "{name}".encode()
+cdef kind {name} = kind(<int> {kind})
 setattr(kinds, "{name}", {name})
 """
 

diff --git a/test/unit/api/python/test_term.py b/test/unit/api/python/test_term.py
new file mode 100644 (file)
index 0000000..43e5414
--- /dev/null
+++ b/test/unit/api/python/test_term.py
@@ -0,0 +1,88 @@
+import pytest
+
+import pycvc4
+from pycvc4 import kinds
+
+
+def test_get_kind():
+    solver = pycvc4.Solver()
+    intsort = solver.getIntegerSort()
+    x = solver.mkConst(intsort, 'x')
+    y = solver.mkConst(intsort, 'y')
+    xpy = solver.mkTerm(kinds.Plus, x, y)
+    assert xpy.getKind() == kinds.Plus
+
+    funsort = solver.mkFunctionSort(intsort, intsort)
+    f = solver.mkConst(funsort, 'f')
+    assert f.getKind() == kinds.Constant
+
+    fx = solver.mkTerm(kinds.ApplyUf, f, x)
+    assert fx.getKind() == kinds.ApplyUf
+
+
+def test_eq():
+    solver = pycvc4.Solver()
+    usort = solver.mkUninterpretedSort('u')
+    x = solver.mkConst(usort, 'x')
+    y = solver.mkConst(usort, 'y')
+    z = x
+
+    assert x == x
+    assert x == z
+    assert not (x != x)
+    assert x != y
+    assert y != z
+
+
+def test_get_sort():
+    solver = pycvc4.Solver()
+    intsort = solver.getIntegerSort()
+    bvsort8 = solver.mkBitVectorSort(8)
+
+    x = solver.mkConst(intsort, 'x')
+    y = solver.mkConst(intsort, 'y')
+
+    a = solver.mkConst(bvsort8, 'a')
+    b = solver.mkConst(bvsort8, 'b')
+
+    assert x.getSort() == intsort
+    assert solver.mkTerm(kinds.Plus, x, y).getSort() == intsort
+
+    assert a.getSort() == bvsort8
+    assert solver.mkTerm(kinds.BVConcat, a, b).getSort() == solver.mkBitVectorSort(16)
+
+def test_get_op():
+    solver = pycvc4.Solver()
+    intsort = solver.getIntegerSort()
+    funsort = solver.mkFunctionSort(intsort, intsort)
+
+    x = solver.mkConst(intsort, 'x')
+    f = solver.mkConst(funsort, 'f')
+
+    fx = solver.mkTerm(kinds.ApplyUf, f, x)
+
+    assert not x.hasOp()
+
+    try:
+        op = x.getOp()
+        assert False
+    except:
+        assert True
+
+    assert fx.hasOp()
+    assert fx.getOp().getKind() == kinds.ApplyUf
+    # equivalent check
+    assert fx.getOp() == solver.mkOp(kinds.ApplyUf)
+
+
+def test_is_const():
+    solver = pycvc4.Solver()
+    intsort = solver.getIntegerSort()
+    one = solver.mkReal(1)
+    x = solver.mkConst(intsort, 'x')
+    xpone = solver.mkTerm(kinds.Plus, x, one)
+    onepone = solver.mkTerm(kinds.Plus, one, one)
+    assert not x.isConst()
+    assert one.isConst()
+    assert not xpone.isConst()
+    assert not onepone.isConst()