substitute method

Z3_ast substitute(
  1. Z3_context c,
  2. Z3_ast a,
  3. int num_exprs,
  4. Pointer<Z3_ast> from,
  5. Pointer<Z3_ast> to,
)

\brief Substitute every occurrence of \ccode{fromi} in \c a with \ccode{toi}, for \c i smaller than \c num_exprs. The result is the new AST. The arrays \c from and \c to must have size \c num_exprs. For every \c i smaller than \c num_exprs, we must have that sort of \ccode{fromi} must be equal to sort of \ccode{toi}.

def_API('Z3_substitute', AST, (_in(CONTEXT), _in(AST), _in(UINT), _in_array(2, AST), _in_array(2, AST)))

Implementation

Z3_ast substitute(
  Z3_context c,
  Z3_ast a,
  int num_exprs,
  ffi.Pointer<Z3_ast> from,
  ffi.Pointer<Z3_ast> to,
) {
  return _substitute(
    c,
    a,
    num_exprs,
    from,
    to,
  );
}