mk_lambda method

Z3_ast mk_lambda(Z3_context c, int num_decls, Pointer<Z3_sort> sorts, Pointer<Z3_symbol> decl_names, Z3_ast body,)

\brief Create a lambda expression. It takes an expression \c body that contains bound variables of the same sorts as the sorts listed in the array \c sorts. The bound variables are de-Bruijn indices created using #Z3_mk_bound. The array \c decl_names contains the names that the quantified formula uses for the bound variables. Z3 applies the convention that the last element in the \c decl_names and \c sorts array refers to the variable with index 0, the second to last element of \c decl_names and \c sorts refers to the variable with index 1, etc. The sort of the resulting expression is \c (Array sorts range) where \c range is the sort of \c body. For example, if the lambda binds two variables of sort \c Int and \c Bool, and the \c body has sort \c Real, the sort of the expression is \c (Array Int Bool Real).

\param c logical context \param num_decls number of variables to be bound. \param sorts the sorts of the bound variables. \param decl_names names of the bound variables \param body the body of the lambda expression.

\sa Z3_mk_bound \sa Z3_mk_forall \sa Z3_mk_lambda_const

def_API('Z3_mk_lambda', AST, (_in(CONTEXT), _in(UINT), _in_array(1, SORT), _in_array(1, SYMBOL), _in(AST)))

Implementation

Z3_ast mk_lambda(
  Z3_context c,
  int num_decls,
  ffi.Pointer<Z3_sort> sorts,
  ffi.Pointer<Z3_symbol> decl_names,
  Z3_ast body,
) {
  return _mk_lambda(
    c,
    num_decls,
    sorts,
    decl_names,
    body,
  );
}