model_get_const_interp method

Z3_ast model_get_const_interp(
  1. Z3_context c,
  2. Z3_model m,
  3. Z3_func_decl a
)

\brief Return the interpretation (i.e., assignment) of constant \c a in the model \c m. Return \c NULL, if the model does not assign an interpretation for \c a. That should be interpreted as: the value of \c a does not matter.

\pre Z3_get_arity(c, a) == 0

def_API('Z3_model_get_const_interp', AST, (_in(CONTEXT), _in(MODEL), _in(FUNC_DECL)))

Implementation

Z3_ast model_get_const_interp(
  Z3_context c,
  Z3_model m,
  Z3_func_decl a,
) {
  return _model_get_const_interp(
    c,
    m,
    a,
  );
}