declareDatatypes method

Map<Sym, DatatypeInfo> declareDatatypes(Map<Sym, List<Constructor>> datatypes)

Declare mutually recursive datatypes given a map from their name to their constructors.

Implementation

Map<Sym, DatatypeInfo> declareDatatypes(
  Map<Sym, List<Constructor>> datatypes,
) {
  final sortsPtr = calloc<Z3_sort>(datatypes.length);
  final namesPtr = calloc<Z3_symbol>(datatypes.length);
  final constructorsPtr = calloc<Z3_constructor_list>(datatypes.length);
  final allConstructors = <Z3_constructor>[];
  try {
    var i = 0;
    for (final MapEntry(:key, :value) in datatypes.entries) {
      namesPtr[i] = _createSymbol(key);
      final constructors =
          value.map((e) => e.buildConstructor(this)).toList();
      allConstructors.addAll(constructors);
      constructorsPtr[i] = _constructorList(constructors);
      i++;
    }

    _z3.mk_datatypes(
      datatypes.length,
      namesPtr,
      sortsPtr,
      constructorsPtr,
    );

    final result = <Sym, DatatypeInfo>{};
    for (var i = 0; i < datatypes.length; i++) {
      final sort = _getSort(sortsPtr[i]) as DatatypeSort;
      result[sort.name] = getDatatypeInfo(sort);
    }
    return result;
  } finally {
    for (var i = 0; i < datatypes.length; i++) {
      if (constructorsPtr[i] != nullptr) {
        _z3.del_constructor_list(constructorsPtr[i]);
      }
    }
    allConstructors.forEach(_z3.del_constructor);
    malloc.free(sortsPtr);
    malloc.free(namesPtr);
    malloc.free(constructorsPtr);
  }
}