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

3 files changed, 19 insertions, 4 deletions

diff --git a/src/api/python/cvc4.pxd b/src/api/python/cvc4.pxd
index 624b3c365..eb4254560 100644
--- 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 b7593f6f1..5abbfb113 100644
--- 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 4fe7347e6..a12c9735c 100755
--- 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})
 """