Skip to content
This repository has been archived by the owner on May 7, 2021. It is now read-only.
/ CVC4-archived Public archive

Commit

Permalink
Fix getKind for Python bindings (#4496)
Browse files Browse the repository at this point in the history
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`.
  • Loading branch information
makaimann authored Jun 10, 2020
1 parent 2a51894 commit 05c0998
Show file tree
Hide file tree
Showing 5 changed files with 119 additions and 4 deletions.
12 changes: 12 additions & 0 deletions .github/workflows/ci.yml
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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'
Expand Down
1 change: 1 addition & 0 deletions src/api/python/cvc4.pxd
Original file line number Diff line number Diff line change
Expand Up @@ -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 +
Expand Down
3 changes: 3 additions & 0 deletions src/api/python/cvc4.pxi
Original file line number Diff line number Diff line change
Expand Up @@ -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()
Expand Down
19 changes: 15 additions & 4 deletions src/api/python/genkinds.py
Original file line number Diff line number Diff line change
Expand Up @@ -69,11 +69,21 @@
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)
Expand All @@ -100,8 +110,9 @@ def as_int(self):

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})
"""

Expand Down
88 changes: 88 additions & 0 deletions test/unit/api/python/test_term.py
Original file line number Diff line number Diff line change
@@ -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()

0 comments on commit 05c0998

Please sign in to comment.