func_interp_add_entry method

void func_interp_add_entry(Z3_context c, Z3_func_interp fi, Z3_ast_vector args, Z3_ast value,)

\brief add a function entry to a function interpretation.

\param c logical context \param fi a function interpretation to be updated. \param args list of arguments. They should be constant values (such as integers) and be of the same types as the domain of the function. \param value value of the function when the parameters match args.

It is assumed that entries added to a function cover disjoint arguments. If an two entries are added with the same arguments, only the second insertion survives and the first inserted entry is removed.

def_API('Z3_func_interp_add_entry', VOID, (_in(CONTEXT), _in(FUNC_INTERP), _in(AST_VECTOR), _in(AST)))

Implementation

void func_interp_add_entry(
  Z3_context c,
  Z3_func_interp fi,
  Z3_ast_vector args,
  Z3_ast value,
) {
  return _func_interp_add_entry(
    c,
    fi,
    args,
    value,
  );
}