substitute_vars method

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

\brief Substitute the variables in \c a with the expressions in \c to. For every \c i smaller than \c num_exprs, the variable with de-Bruijn index \c i is replaced with term \ccode{toi}. Note that a variable is created using the function \ref Z3_mk_bound.

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

Implementation

Z3_ast substitute_vars(
  Z3_context c,
  Z3_ast a,
  int num_exprs,
  ffi.Pointer<Z3_ast> to,
) {
  return _substitute_vars(
    c,
    a,
    num_exprs,
    to,
  );
}