substituteFuncs<A extends Expr> method

A substituteFuncs<A extends Expr>(
  1. Expr expr,
  2. Map<FuncDecl, Expr> substitutions
)

Substitute the arguments to FuncDecls in expr with the expressions in to.

Implementation

A substituteFuncs<A extends Expr>(
  Expr expr,
  Map<FuncDecl, Expr> substitutions,
) {
  final fromPtr = calloc<Z3_func_decl>(substitutions.length);
  final toPtr = calloc<Z3_ast>(substitutions.length);
  try {
    for (var i = 0; i < substitutions.length; i++) {
      final entry = substitutions.entries.elementAt(i);
      fromPtr[i] = _createFuncDecl(entry.key);
      toPtr[i] = _createAST(entry.value);
    }
    final result = _z3.substitute_funs(
      _createAST(expr),
      substitutions.length,
      fromPtr,
      toPtr,
    );
    return _getExpr(result) as A;
  } finally {
    malloc.free(fromPtr);
    malloc.free(toPtr);
  }
}