Skip to main content

synth_fun

Function synth_fun 

Source
pub unsafe extern "C" fn synth_fun(
    cvc5: *mut Solver,
    symbol: *const c_char,
    size: usize,
    bound_vars: *const Term,
    sort: Sort,
) -> Term
Expand 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.