getImpliedEqualities method

List<int>? getImpliedEqualities(
  1. List<Expr> terms
)

Implementation

List<int>? getImpliedEqualities(List<Expr> terms) {
  final termsPtr = calloc<Z3_ast>(terms.length);
  final classIdsPtr = calloc<UnsignedInt>(terms.length);
  try {
    for (var i = 0; i < terms.length; i++) {
      termsPtr[i] = _c._createAST(terms[i]);
    }
    final result = _c._bool(_c._z3.get_implied_equalities(
      _solver,
      terms.length,
      termsPtr,
      classIdsPtr,
    ));
    final classIds = <int>[];
    for (var i = 0; i < terms.length; i++) {
      classIds.add(classIdsPtr[i]);
    }
    if (result == false) {
      return null;
    }
    return classIds;
  } finally {
    malloc.free(termsPtr);
    malloc.free(classIdsPtr);
  }
}