Function declare_oracle_fun 

pub unsafe extern "C" fn declare_oracle_fun(
    cvc5: *mut Solver,
    symbol: *const c_char,
    size: usize,
    sorts: *const Sort,
    sort: Sort,
    state: *mut c_void,
    fun: Option<unsafe extern "C" fn(arg1: usize, arg2: *const Term, arg3: *mut c_void) -> Term>,
) -> Term

Declare an oracle function with reference to an implementation.

Oracle functions have a different semantics with respect to ordinary declared functions. In particular, for an input to be satisfiable, its oracle functions are implicitly universally quantified.

This function is used in part for implementing this command:

\verbatim embed:rst:leading-asterisk .. code:: smtlib

(declare-oracle-fun <sym> (<sort>*) <sort> <sym>)

\endverbatim

In particular, the above command is implemented by constructing a function over terms that wraps a call to binary sym via a text interface.

@warning This function is experimental and may change in future versions.

@param cvc5 The solver instance. @param symbol The name of the oracle @param size The number of domain sorts of the oracle function. @param sorts The domain sorts. @param sort The sort of the return value of this function. @param state The state data for the oracle function, may be NULL. @param fun The function that implements the oracle function, taking a an array of term arguments and its size and a void pointer to optionally capture any state data the function may need. @return The oracle function.