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`.

1 files changed, 88 insertions, 0 deletions

diff --git a/test/unit/api/python/test_term.py b/test/unit/api/python/test_term.py
new file mode 100644
index 000000000..43e541412
--- /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()