declareEnum method

EnumInfo declareEnum(Sym name, List<Sym> elements)

Implementation

EnumInfo declareEnum(
  Sym name,
  List<Sym> elements,
) {
  final constsPtr = calloc<Z3_func_decl>(elements.length);
  final testersPtr = calloc<Z3_func_decl>(elements.length);
  final elementsPtr = calloc<Z3_symbol>(elements.length);
  try {
    for (var i = 0; i < elements.length; i++) {
      elementsPtr[i] = _createSymbol(elements[i]);
    }
    final result = _z3.mk_enumeration_sort(
      _createSymbol(name),
      elements.length,
      elementsPtr,
      constsPtr,
      testersPtr,
    );
    _z3.inc_ref(result.cast());
    // Annoying but we need to increment the reference to these beforehand
    // because _getAST makes api calls that will probably free them.
    final consts = List.generate(elements.length, (i) => constsPtr[i]);
    final testers = List.generate(elements.length, (i) => testersPtr[i]);
    for (var i = 0; i < elements.length; i++) {
      _z3.inc_ref(constsPtr[i].cast());
      _z3.inc_ref(testersPtr[i].cast());
    }
    try {
      return EnumInfo(
        _getSort(result) as DatatypeSort,
        {
          for (final e in consts)
            _getSymbol(_z3.get_decl_name(e)): ConstVar.func(_getFuncDecl(e))
        },
        testers.map(_getFuncDecl).toList(),
      );
    } finally {
      _z3.dec_ref(result.cast());
      for (var i = 0; i < elements.length; i++) {
        _z3.dec_ref(constsPtr[i].cast());
        _z3.dec_ref(testersPtr[i].cast());
      }
    }
  } finally {
    malloc.free(constsPtr);
    malloc.free(testersPtr);
    malloc.free(elementsPtr);
  }
}