Function get_model 

pub unsafe extern "C" fn get_model(
    cvc5: *mut Solver,
    nsorts: usize,
    sorts: *const Sort,
    nconsts: usize,
    consts: *const Term,
) -> *const c_char

Get the model

SMT-LIB:

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

(get-model)

Requires to enable option :ref:produce-models <lbl-option-produce-models>. \endverbatim

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

@param cvc5 The solver instance. @param nsorts The number of uninterpreted sorts that should be printed in the model. @param sorts The list of uninterpreted sorts. @param nconsts The size of the list of free constants that should be printed in the model. @param consts The list of free constants that should be printed in the model. A subset of these may be printed based on isModelCoreSymbol(). @return A string representing the model. @note The returned char* pointer is only valid until the next call to this function.