Function Z3_func_interp_add_entry

pub unsafe extern "C" fn Z3_func_interp_add_entry(
    c: Z3_context,
    fi: Z3_func_interp,
    args: Z3_ast_vector,
    value: Z3_ast,
)

add a function entry to a function interpretation.

• c: logical context
• fi: a function interpretation to be updated.
• args: list of arguments. They should be constant values (such as integers) and be of the same types as the domain of the function.
• 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.