diff options
Diffstat (limited to 'src/api/python/cvc5.pxi')
| -rw-r--r-- | src/api/python/cvc5.pxi | 33 |
1 files changed, 10 insertions, 23 deletions
diff --git a/src/api/python/cvc5.pxi b/src/api/python/cvc5.pxi index 3367bf47b..6f50b8401 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. |