Function z3_sys::Z3_model_get_const_interp [−][src]
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