Function z3_sys::Z3_func_interp_add_entry [−][src]
pub unsafe extern "C" fn Z3_func_interp_add_entry(
c: Z3_context,
fi: Z3_func_interp,
args: Z3_ast_vector,
value: Z3_ast
)
Expand description
add a function entry to a function interpretation.
c
: logical contextfi
: 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.