diff options
Diffstat (limited to 'src/api/python/cvc5.pxi')
| -rw-r--r-- | src/api/python/cvc5.pxi | 45 |
1 files changed, 16 insertions, 29 deletions
diff --git a/src/api/python/cvc5.pxi b/src/api/python/cvc5.pxi index 3367bf47b..05138e9bc 100644 --- a/src/api/python/cvc5.pxi +++ b/src/api/python/cvc5.pxi @@ -1811,14 +1811,8 @@ cdef class Solver: sort.csort = self.csolver.declareSort(symbol.encode(), arity) return sort - def defineFun(self, sym_or_fun, bound_vars, sort_or_term, t=None, glbl=False): - """ - Define n-ary function. - Supports two uses: - - - ``Term defineFun(str symbol, List[Term] bound_vars, Sort sort, Term term, bool glbl)`` - - ``Term defineFun(Term fun, List[Term] bound_vars, Term term, bool glbl)`` - + def defineFun(self, str symbol, list bound_vars, Sort sort, Term term, glbl=False): + """Define n-ary function. SMT-LIB: @@ -1830,27 +1824,20 @@ cdef class Solver: :param bound_vars: the parameters to this function :param sort: the sort of the return value of this function :param term: the function body - :param global: determines whether this definition is global (i.e. persists when popping the context) + :param glbl: determines whether this definition is global (i.e. persists when popping the context) :return: the function """ - cdef Term term = Term(self) + cdef Term fun = Term(self) cdef vector[c_Term] v for bv in bound_vars: v.push_back((<Term?> bv).cterm) - if t is not None: - term.cterm = self.csolver.defineFun((<str?> sym_or_fun).encode(), - <const vector[c_Term] &> v, - (<Sort?> sort_or_term).csort, - (<Term?> t).cterm, - <bint> glbl) - else: - term.cterm = self.csolver.defineFun((<Term?> sym_or_fun).cterm, - <const vector[c_Term]&> v, - (<Term?> sort_or_term).cterm, - <bint> glbl) - - return term + fun.cterm = self.csolver.defineFun(symbol.encode(), + <const vector[c_Term] &> v, + sort.csort, + term.cterm, + <bint> glbl) + return fun def defineFunRec(self, sym_or_fun, bound_vars, sort_or_term, t=None, glbl=False): """Define recursive functions. @@ -2060,25 +2047,25 @@ cdef class Solver: """ return self.csolver.isModelCoreSymbol(v.cterm) - def getSeparationHeap(self): + def getValueSepHeap(self): """When using separation logic, obtain the term for the heap. :return: The term for the heap """ cdef Term term = Term(self) - term.cterm = self.csolver.getSeparationHeap() + term.cterm = self.csolver.getValueSepHeap() return term - def getSeparationNilTerm(self): + def getValueSepNil(self): """When using separation logic, obtain the term for nil. :return: The term for nil """ cdef Term term = Term(self) - term.cterm = self.csolver.getSeparationNilTerm() + term.cterm = self.csolver.getValueSepNil() return term - def declareSeparationHeap(self, Sort locType, Sort dataType): + def declareSepHeap(self, Sort locType, Sort dataType): """ When using separation logic, this sets the location sort and the datatype sort to the given ones. This method should be invoked exactly @@ -2087,7 +2074,7 @@ cdef class Solver: :param locSort: The location sort of the heap :param dataSort: The data sort of the heap """ - self.csolver.declareSeparationHeap(locType.csort, dataType.csort) + self.csolver.declareSepHeap(locType.csort, dataType.csort) def declarePool(self, str symbol, Sort sort, initValue): """Declare a symbolic pool of terms with the given initial value. |