Skip to main content

get_value

Function get_value 

Source
pub unsafe extern "C" fn get_value(
    cvc5: *mut Solver,
    term: Term,
) -> Term
Expand description

Get the value of the given term in the current model.

SMT-LIB:

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

(get-value ( <term> ))

\endverbatim

@param cvc5 The solver instance. @param term The term for which the value is queried. @return The value of the given term.