build method

@override Z3_ast build(Context c)

Implementation

@override
Z3_ast build(Context c) {
  final patternsPtr = calloc<Z3_pattern>(patterns.length);
  final noPatternsPtr = calloc<Z3_ast>(noPatterns.length);
  final namesPtr = calloc<Z3_symbol>(args.length);
  final sortsPtr = calloc<Z3_sort>(args.length);
  try {
    for (var i = 0; i < patterns.length; i++) {
      patternsPtr[i] = c._createPattern(patterns[i]);
    }
    for (var i = 0; i < noPatterns.length; i++) {
      noPatternsPtr[i] = c._createAST(noPatterns[i]);
    }
    var i = 0;
    for (final MapEntry(:key, :value) in args.entries) {
      namesPtr[i] = c._createSymbol(key);
      sortsPtr[i] = c._createSort(value);
      i++;
    }
    final result = c._z3.mk_quantifier_ex(
      true,
      weight,
      c._createSymbol(id),
      c._createSymbol(skolem),
      patterns.length,
      patternsPtr,
      noPatterns.length,
      noPatternsPtr,
      args.length,
      sortsPtr,
      namesPtr,
      c._createAST(body),
    );
    return result;
  } finally {
    malloc.free(patternsPtr);
    malloc.free(noPatternsPtr);
    malloc.free(namesPtr);
    malloc.free(sortsPtr);
  }
}