declareList method

ListInfo declareList(Sym name, Sort element)

Declares a list with the given name and element type.

Implementation

ListInfo declareList(
  Sym name,
  Sort element,
) {
  final decls = calloc<Z3_func_decl>(6);
  try {
    final result = _z3.mk_list_sort(
      _createSymbol(name),
      _createSort(element),
      decls.elementAt(0),
      decls.elementAt(1),
      decls.elementAt(2),
      decls.elementAt(3),
      decls.elementAt(4),
      decls.elementAt(5),
    );
    final nil = decls[0];
    final isNil = decls[1];
    final cons = decls[2];
    final isCons = decls[3];
    final head = decls[4];
    final tail = decls[5];
    _z3.inc_ref(result.cast());
    _z3.inc_ref(nil.cast());
    _z3.inc_ref(isNil.cast());
    _z3.inc_ref(cons.cast());
    _z3.inc_ref(isCons.cast());
    _z3.inc_ref(head.cast());
    _z3.inc_ref(tail.cast());
    try {
      return ListInfo(
        _getSort(result) as DatatypeSort,
        ConstVar.func(_getFuncDecl(nil)),
        _getFuncDecl(isNil),
        _getFuncDecl(cons),
        _getFuncDecl(isCons),
        _getFuncDecl(head),
        _getFuncDecl(tail),
      );
    } finally {
      _z3.dec_ref(result.cast());
      _z3.dec_ref(nil.cast());
      _z3.dec_ref(isNil.cast());
      _z3.dec_ref(cons.cast());
      _z3.dec_ref(isCons.cast());
      _z3.dec_ref(head.cast());
      _z3.dec_ref(tail.cast());
    }
  } finally {
    malloc.free(decls);
  }
}