buildConstructor method

Z3_constructor buildConstructor(Context c)

Implementation

Z3_constructor buildConstructor(Context c) {
  final fieldNamesPtr = calloc<Z3_symbol>(fields.length);
  final sortsPtr = calloc<Z3_sort>(fields.length);
  final sortRefsPtr = calloc<UnsignedInt>(fields.length);
  try {
    var i = 0;
    for (final MapEntry(:key, :value) in fields.entries) {
      fieldNamesPtr[i] = c._createSymbol(key);
      if (value is IndexRefSort) {
        sortsPtr[i] = nullptr;
        sortRefsPtr[i] = value.index;
      } else {
        sortsPtr[i] = c._createSort(value);
        sortRefsPtr[i] = 0;
      }
      i++;
    }
    final result = c._z3.mk_constructor(
      c._createSymbol(name),
      c._createSymbol(recognizer),
      fields.length,
      fieldNamesPtr,
      sortsPtr,
      sortRefsPtr,
    );
    return result;
  } finally {
    malloc.free(fieldNamesPtr);
    malloc.free(sortsPtr);
    malloc.free(sortRefsPtr);
  }
}