diff options
Diffstat (limited to 'src/api/python/cvc5.pxi')
| -rw-r--r-- | src/api/python/cvc5.pxi | 27 |
1 files changed, 21 insertions, 6 deletions
diff --git a/src/api/python/cvc5.pxi b/src/api/python/cvc5.pxi index 9e1aeaca1..3d24b5dbd 100644 --- a/src/api/python/cvc5.pxi +++ b/src/api/python/cvc5.pxi @@ -1130,24 +1130,33 @@ cdef class Solver: term.cterm = self.csolver.mkReal("{}/{}".format(val, den).encode()) return term - def mkRegexpNone(self): - """Create a regular expression empty term. + def mkRegexpAll(self): + """Create a regular expression all (re.all) term. - :return: the empty term + :return: the all term """ cdef Term term = Term(self) - term.cterm = self.csolver.mkRegexpNone() + term.cterm = self.csolver.mkRegexpAll() return term def mkRegexpAllchar(self): - """Create a regular expression sigma term. + """Create a regular expression allchar (re.allchar) term. - :return: the sigma term + :return: the allchar term """ cdef Term term = Term(self) term.cterm = self.csolver.mkRegexpAllchar() return term + def mkRegexpNone(self): + """Create a regular expression none (re.none) term. + + :return: the none term + """ + cdef Term term = Term(self) + term.cterm = self.csolver.mkRegexpNone() + return term + def mkEmptySet(self, Sort s): """Create a constant representing an empty set of the given sort. @@ -2830,6 +2839,12 @@ cdef class Term: op.cop = self.cterm.getOp() return op + def hasSymbol(self): + return self.cterm.hasSymbol() + + def getSymbol(self): + return self.cterm.getSymbol().decode() + def isNull(self): return self.cterm.isNull() |