[−][src]Function z3_sys::Z3_mk_distinct
pub unsafe extern "C" fn Z3_mk_distinct(
c: Z3_context,
num_args: c_uint,
args: *const Z3_ast
) -> Z3_ast
Create an AST node representing distinct(args[0], ..., args[num_args-1])
.
The distinct
construct is used for declaring the arguments pairwise distinct.
That is, Forall 0 <= i < j < num_args. not args[i] = args[j]
.
All arguments must have the same sort.
NOTE: The number of arguments of a distinct construct must be greater than one.