pub unsafe extern "C" fn declare_fun(
cvc5: *mut Solver,
symbol: *const c_char,
size: usize,
sorts: *const Sort,
sort: Sort,
fresh: bool,
) -> TermExpand description
Declare n-ary function symbol.
SMT-LIB:
\verbatim embed:rst:leading-asterisk .. code:: smtlib
(declare-fun <symbol> ( <sort>* ) <sort>)\endverbatim
@param cvc5 The solver instance. @param symbol The name of the function. @param size The number of domain sorts of the function. @param sorts The domain sorts of the function. @param sort The codomain sort of the function. @param fresh If true, then this method always returns a new Term. Otherwise, this method will always return the same Term for each call with the given sorts and symbol where fresh is false. @return The function.