pub unsafe extern "C" fn synth_fun(
cvc5: *mut Solver,
symbol: *const c_char,
size: usize,
bound_vars: *const Term,
sort: Sort,
) -> TermExpand description
Synthesize n-ary function.
SyGuS v2:
\verbatim embed:rst:leading-asterisk .. code:: smtlib
(synth-fun <symbol> ( <boundVars>* ) <sort>)\endverbatim
@param cvc5 The solver instance. @param symbol The name of the function. @param size The number of parameters. @param bound_vars The parameters to this function. @param sort The sort of the return value of this function. @return The function.