build method

@override Z3_ast build(Context c)

Implementation

@override
Z3_ast build(Context c) {
  final runes = value.runes;
  switch (c.config.encoding) {
    case CharEncoding.ascii:
      final buffer = calloc<ffi.Char>(runes.length);
      try {
        for (var i = 0; i < runes.length; i++) {
          if (runes.elementAt(i) > 255) {
            throw ArgumentError.value(
              value,
              'value',
              'String contains non-ASCII characters',
            );
          }
          buffer[i] = runes.elementAt(i);
        }
        final result = c._z3.mk_lstring(value.length, buffer);
        return result;
      } finally {
        malloc.free(buffer);
      }
    case CharEncoding.bmp:
      final buffer = calloc<UnsignedInt>(runes.length);
      try {
        for (var i = 0; i < runes.length; i++) {
          if (runes.elementAt(i) > 65535) {
            throw ArgumentError.value(
              value,
              'value',
              'String contains non-BMP characters',
            );
          }
          buffer[i] = runes.elementAt(i);
        }
        final result = c._z3.mk_u32string(runes.length, buffer);
        return result;
      } finally {
        malloc.free(buffer);
      }
    case CharEncoding.unicode:
      final buffer = calloc<UnsignedInt>(runes.length);
      try {
        for (var i = 0; i < runes.length; i++) {
          buffer[i] = runes.elementAt(i);
        }
        final result = c._z3.mk_u32string(runes.length, buffer);
        return result;
      } finally {
        malloc.free(buffer);
      }
  }
}