Function z3_sys::Z3_substitute
source · pub unsafe extern "C" fn Z3_substitute(
c: Z3_context,
a: Z3_ast,
num_exprs: c_uint,
from: *const Z3_ast,
to: *const Z3_ast
) -> Z3_ast
Expand description
Substitute every occurrence of from[i]
in a
with to[i]
, for i
smaller than num_exprs
.
The result is the new AST. The arrays from
and to
must have
size num_exprs
.
For every i
smaller than num_exprs
, we must have that sort of
from[i]
must be equal to sort of to[i]
.