Skip to main content

declare_pool

cvc5_sys

Function declare_pool 

Source 
pub unsafe extern "C" fn declare_pool(
    cvc5: *mut Solver,
    symbol: *const c_char,
    sort: Sort,
    size: usize,
    init_value: *const Term,
) -> Term
Expand description

Declare a symbolic pool of terms with the given initial value.

For details on how pools are used to specify instructions for quantifier instantiation, see documentation for the #CVC5_KIND_INST_POOL kind.

SMT-LIB:

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

(declare-pool <symbol> <sort> ( <term>* ))

\endverbatim

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

@param cvc5 The solver instance. @param symbol The name of the pool. @param sort The sort of the elements of the pool. @param size The number of initial values of the pool. @param init_value The initial value of the pool. @return The pool symbol.