Skip to main content

declare_fun

Function declare_fun 

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