Skip to main content

get_values

cvc5_sys

Function get_values 

Source 
pub unsafe extern "C" fn get_values(
    cvc5: *mut Solver,
    size: usize,
    terms: *const Term,
    rsize: *mut usize,
) -> *const Term
Expand description

Get the values of the given terms in the current model.

SMT-LIB:

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

(get-value ( <term>* ))

\endverbatim

@param cvc5 The solver instance. @param size The number of terms for which the value is queried. @param terms The terms. @param rsize The resulting size of the timeout core. @return The values of the given terms.