build method

@override Z3_ast build(Context c)

Implementation

@override
Z3_ast build(Context c) {
  final argsPtr = calloc<Z3_ast>(args.length);
  try {
    for (var i = 0; i < args.length; i++) {
      argsPtr[i] = c._createAST(args[i]);
    }
    final Z3_ast result;
    switch (kind) {
      case NaryOpKind.distinct:
        result = c._z3.mk_distinct(args.length, argsPtr);
      case NaryOpKind.and:
        result = c._z3.mk_and(args.length, argsPtr);
      case NaryOpKind.or:
        result = c._z3.mk_or(args.length, argsPtr);
      case NaryOpKind.add:
        result = c._z3.mk_add(args.length, argsPtr);
      case NaryOpKind.mul:
        result = c._z3.mk_mul(args.length, argsPtr);
      case NaryOpKind.sub:
        result = c._z3.mk_sub(args.length, argsPtr);
      case NaryOpKind.setUnion:
        result = c._z3.mk_set_union(args.length, argsPtr);
      case NaryOpKind.setIntersect:
        result = c._z3.mk_set_intersect(args.length, argsPtr);
      case NaryOpKind.seqConcat:
        result = c._z3.mk_seq_concat(args.length, argsPtr);
      case NaryOpKind.reUnion:
        result = c._z3.mk_re_union(args.length, argsPtr);
      case NaryOpKind.reConcat:
        result = c._z3.mk_re_concat(args.length, argsPtr);
      case NaryOpKind.reIntersect:
        result = c._z3.mk_re_intersect(args.length, argsPtr);
    }
    return result;
  } finally {
    malloc.free(argsPtr);
  }
}