getExprApp method

App? getExprApp(
  1. Expr app
)

Get the App representing an expression, this gives you access to the underlying FuncDecl and parameters.

Implementation

App? getExprApp(Expr app) {
  final ast = _createAST(app);
  final kind = _z3.get_ast_kind(ast);
  if (kind == Z3_ast_kind.APP_AST || kind == Z3_ast_kind.NUMERAL_AST) {
    final Z3_app app = ast.cast();
    final decl = _z3.get_app_decl(app);
    return App._(
      _getFuncDecl(decl),
      _getAppArgs(app),
      this,
      ast.cast(),
    );
  } else {
    return null;
  }
}