Exists.bind constructor

Exists.bind(
  1. Context context,
  2. List<ConstVar> bound,
  3. AST body, {
  4. int weight = 0,
  5. List<Pat> patterns = const [],
  6. List<AST> noPatterns = const [],
  7. Sym? id,
  8. Sym? skolem,
})

Implementation

factory Exists.bind(
  Context context,
  List<ConstVar> bound,
  AST body, {
  int weight = 0,
  List<Pat> patterns = const [],
  List<AST> noPatterns = const [],
  Sym? id,
  Sym? skolem,
}) {
  final boundPtr = calloc<Z3_app>(bound.length);
  final patternsPtr = calloc<Z3_pattern>(patterns.length);
  final noPatternsPtr = calloc<Z3_ast>(noPatterns.length);
  try {
    for (var i = 0; i < bound.length; i++) {
      boundPtr[i] = context._createAST(bound[i]).cast();
    }
    for (var i = 0; i < patterns.length; i++) {
      patternsPtr[i] = context._createPattern(patterns[i]);
    }
    for (var i = 0; i < noPatterns.length; i++) {
      noPatternsPtr[i] = context._createAST(noPatterns[i]);
    }
    final result = context._z3.mk_quantifier_const_ex(
      false,
      weight,
      context._createSymbol(id),
      context._createSymbol(skolem),
      bound.length,
      boundPtr,
      patterns.length,
      patternsPtr,
      noPatterns.length,
      noPatternsPtr,
      context._createAST(body),
    );
    return context._getAST(result) as Exists;
  } finally {
    malloc.free(boundPtr);
    malloc.free(patternsPtr);
    malloc.free(noPatternsPtr);
  }
}