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