diff options
Diffstat (limited to 'src/api/python/cvc5.pxi')
-rw-r--r-- | src/api/python/cvc5.pxi | 84 |
1 files changed, 70 insertions, 14 deletions
diff --git a/src/api/python/cvc5.pxi b/src/api/python/cvc5.pxi index 25ded76bb..8599a1cd1 100644 --- a/src/api/python/cvc5.pxi +++ b/src/api/python/cvc5.pxi @@ -658,6 +658,19 @@ cdef class Solver: term.cterm = self.csolver.mkTerm((<Op?> op).cop, v) return term + def mkTuple(self, sorts, terms): + cdef vector[c_Sort] csorts + cdef vector[c_Term] cterms + + for s in sorts: + csorts.push_back((<Sort?> s).csort) + for s in terms: + cterms.push_back((<Term?> s).cterm) + cdef Term result = Term(self) + result.cterm = self.csolver.mkTuple(csorts, cterms) + return result + + def mkOp(self, kind k, arg0=None, arg1 = None): ''' Supports the following uses: @@ -1609,19 +1622,6 @@ cdef class Term: def isNull(self): return self.cterm.isNull() - def getConstArrayBase(self): - cdef Term term = Term(self.solver) - term.cterm = self.cterm.getConstArrayBase() - return term - - def getSequenceValue(self): - elems = [] - for e in self.cterm.getSequenceValue(): - term = Term(self.solver) - term.cterm = e - elems.append(term) - return elems - def notTerm(self): cdef Term term = Term(self.solver) term.cterm = self.cterm.notTerm() @@ -1657,6 +1657,14 @@ cdef class Term: term.cterm = self.cterm.iteTerm(then_t.cterm, else_t.cterm) return term + def isConstArray(self): + return self.cterm.isConstArray() + + def getConstArrayBase(self): + cdef Term term = Term(self.solver) + term.cterm = self.cterm.getConstArrayBase() + return term + def isBooleanValue(self): return self.cterm.isBooleanValue() @@ -1673,7 +1681,12 @@ cdef class Term: def isIntegerValue(self): return self.cterm.isIntegerValue() - + def isAbstractValue(self): + return self.cterm.isAbstractValue() + + def getAbstractValue(self): + return self.cterm.getAbstractValue().decode() + def isFloatingPointPosZero(self): return self.cterm.isFloatingPointPosZero() @@ -1698,6 +1711,49 @@ cdef class Term: term.cterm = get2(t) return (get0(t), get1(t), term) + def isSetValue(self): + return self.cterm.isSetValue() + + def getSetValue(self): + elems = set() + for e in self.cterm.getSetValue(): + term = Term(self.solver) + term.cterm = e + elems.add(term) + return elems + + def isSequenceValue(self): + return self.cterm.isSequenceValue() + + def getSequenceValue(self): + elems = [] + for e in self.cterm.getSequenceValue(): + term = Term(self.solver) + term.cterm = e + elems.append(term) + return elems + + def isUninterpretedValue(self): + return self.cterm.isUninterpretedValue() + + def getUninterpretedValue(self): + cdef pair[c_Sort, int32_t] p = self.cterm.getUninterpretedValue() + cdef Sort sort = Sort(self.solver) + sort.csort = p.first + i = p.second + return (sort, i) + + def isTupleValue(self): + return self.cterm.isTupleValue() + + def getTupleValue(self): + elems = [] + for e in self.cterm.getTupleValue(): + term = Term(self.solver) + term.cterm = e + elems.append(term) + return elems + def getIntegerValue(self): return int(self.cterm.getIntegerValue().decode()) |