substitute_funs method

Z3_ast substitute_funs(
  1. Z3_context c,
  2. Z3_ast a,
  3. int num_funs,
  4. Pointer<Z3_func_decl> from,
  5. Pointer<Z3_ast> to,
)

\brief Substitute functions in \c from with new expressions in \c to.

The expressions in \c to can have free variables. The free variable in \c to at index 0 refers to the first argument of \c from, the free variable at index 1 corresponds to the second argument.

def_API('Z3_substitute_funs', AST, (_in(CONTEXT), _in(AST), _in(UINT), _in_array(2, FUNC_DECL), _in_array(2, AST)))

Implementation

Z3_ast substitute_funs(
  Z3_context c,
  Z3_ast a,
  int num_funs,
  ffi.Pointer<Z3_func_decl> from,
  ffi.Pointer<Z3_ast> to,
) {
  return _substitute_funs(
    c,
    a,
    num_funs,
    from,
    to,
  );
}