Function z3_sys::Z3_model_get_const_interp

source · 
pub unsafe extern "C" fn Z3_model_get_const_interp(
    c: Z3_context,
    m: Z3_model,
    a: Z3_func_decl
) -> Z3_ast
Expand description

Return the interpretation (i.e., assignment) of constant a in the model m.

Return NULL, if the model does not assign an interpretation for a. That should be interpreted as: the value of a does not matter.

Preconditions:

  • Z3_get_arity(c, a) == 0