Function z3_sys::Z3_mk_lambda [−][src]
pub unsafe extern "C" fn Z3_mk_lambda(
c: Z3_context,
num_decls: c_uint,
sorts: *const Z3_sort,
decl_names: *const Z3_symbol,
body: Z3_ast
) -> Z3_ast
Expand description
Create a lambda expression.
It takes an expression body
that contains bound variables of
the same sorts as the sorts listed in the array sorts
. The
bound variables are de-Bruijn indices created using Z3_mk_bound
.
The array decl_names
contains the names that the quantified
formula uses for the bound variables. Z3 applies the convention
that the last element in the decl_names
and sorts
array
refers to the variable with index 0
, the second to last element
of decl_names
and sorts
refers to the variable with index 1
, etc.
The sort of the resulting expression is (Array sorts range)
where
range
is the sort of body
. For example, if the lambda binds two
variables of sort Int
and Bool
, and the body
has sort Real
,
the sort of the expression is (Array Int Bool Real)
.
c
: logical contextnum_decls
: number of variables to be bound.sorts
: the sorts of the bound variables.decl_names
: names of the bound variablesbody
: the body of the lambda expression.