declareTuple method

TupleInfo declareTuple(Sym name, Map<Sym, Sort> fields)

Declares a tuple with the given name and fields.

Implementation

TupleInfo declareTuple(
  Sym name,
  Map<Sym, Sort> fields,
) {
  final decls = calloc<Z3_func_decl>(fields.length + 1);
  final sortsPtr = calloc<Z3_sort>(fields.length);
  final namesPtr = calloc<Z3_symbol>(fields.length);
  try {
    var i = 0;
    for (final MapEntry(:key, :value) in fields.entries) {
      namesPtr[i] = _createSymbol(key);
      sortsPtr[i] = _createSort(value);
      i++;
    }
    final result = _z3.mk_tuple_sort(
      _createSymbol(name),
      fields.length,
      namesPtr,
      sortsPtr,
      decls.elementAt(i),
      decls,
    );
    _z3.inc_ref(result.cast());
    try {
      final con = decls.elementAt(i).value;
      final proj =
          List.generate(fields.length, (i) => _getFuncDecl(decls[i]));
      return TupleInfo(
        _getSort(result) as DatatypeSort,
        _getFuncDecl(con),
        proj,
      );
    } finally {
      _z3.dec_ref(result.cast());
    }
  } finally {
    malloc.free(decls);
    malloc.free(sortsPtr);
    malloc.free(namesPtr);
  }
}