diff options
Diffstat (limited to 'src/api')
-rw-r--r-- | src/api/python/cvc4.pxd | 1 | ||||
-rw-r--r-- | src/api/python/cvc4.pxi | 3 | ||||
-rwxr-xr-x | src/api/python/genkinds.py | 19 |
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}) """ |