Skip to main content

declare_sort

cvc5_sys

Function declare_sort 

Source 
pub unsafe extern "C" fn declare_sort(
    cvc5: *mut Solver,
    symbol: *const c_char,
    arity: u32,
    fresh: bool,
) -> Sort
Expand description

Declare uninterpreted sort.

SMT-LIB:

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

(declare-sort <symbol> <numeral>)

\endverbatim

@note This corresponds to cvc5_mk_uninterpreted_sort() if arity = 0, and to cvc5_mk_uninterpreted_sort_constructor_sort() if arity > 0.

@param cvc5 The solver instance. @param symbol The name of the sort. @param arity The arity of the sort. @param fresh If true, then this method always returns a new Sort. @return The sort.