parse method

List<AST> parse(String str, { Map<Sym, Sort> sorts = const {}, Map<Sym, FuncDecl> decls = const {}, })

Parse a SMT-LIB string, returning all of its assertions.

Implementation

List<AST> parse(
  String str, {
  Map<Sym, Sort> sorts = const {},
  Map<Sym, FuncDecl> decls = const {},
}) {
  final sortsPtr = calloc<Z3_symbol>(sorts.length);
  final sortsSortsPtr = calloc<Z3_sort>(sorts.length);
  final declsPtr = calloc<Z3_symbol>(decls.length);
  final declsFuncDeclsPtr = calloc<Z3_func_decl>(decls.length);
  final strPtr = str.toNativeUtf8();
  try {
    var i = 0;
    for (final MapEntry(:key, :value) in sorts.entries) {
      sortsPtr[i] = _createSymbol(key);
      sortsSortsPtr[i] = _createSort(value);
      i++;
    }
    for (final MapEntry(:key, :value) in decls.entries) {
      declsPtr[i] = _createSymbol(key);
      declsFuncDeclsPtr[i] = _createFuncDecl(value);
      i++;
    }
    final vec = _z3.parse_smtlib2_string(
      strPtr.cast(),
      sorts.length,
      sortsPtr,
      sortsSortsPtr,
      decls.length,
      declsPtr,
      declsFuncDeclsPtr,
    );
    return _unpackAstVector(vec);
  } finally {
    malloc.free(sortsPtr);
    malloc.free(sortsSortsPtr);
    malloc.free(declsPtr);
    malloc.free(declsFuncDeclsPtr);
    malloc.free(strPtr);
  }
}