diff options
| author | makaimann <makaim@stanford.edu> | 2020-06-04 18:21:37 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-06-04 18:21:37 -0700 |
| commit | a2fc412f22552ae0e8f9c36650d1de2d362638dd (patch) | |
| tree | 5f66f0f8128a826e6099845191ccbe5efdd0f3c3 /src/api/python | |
| parent | 67678d6c8a28e71483d8171311725e9e1a86775c (diff) | |
Add a method for retrieving base of a constant array through API (#4494)
Diffstat (limited to 'src/api/python')
| -rw-r--r-- | src/api/python/cvc4.pxd | 1 | ||||
| -rw-r--r-- | src/api/python/cvc4.pxi | 5 |
2 files changed, 6 insertions, 0 deletions
diff --git a/src/api/python/cvc4.pxd b/src/api/python/cvc4.pxd index 1e0b9893b..cc998306d 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 + + Term getConstArrayBase() except + Term notTerm() except + Term andTerm(const Term& t) except + Term orTerm(const Term& t) except + diff --git a/src/api/python/cvc4.pxi b/src/api/python/cvc4.pxi index 827c53ef4..9dd9c1cde 100644 --- a/src/api/python/cvc4.pxi +++ b/src/api/python/cvc4.pxi @@ -1096,6 +1096,11 @@ cdef class Term: def isNull(self): return self.cterm.isNull() + def getConstArrayBase(self): + cdef Term term = Term() + term.cterm = self.cterm.getConstArrayBase() + return term + def notTerm(self): cdef Term term = Term() term.cterm = self.cterm.notTerm() |