pbLe method

Expr pbLe(
  1. Map<Expr, int> args,
  2. int k
)

Create the pseudo-boolean relation p1 + p2 + ... + pn <= k.

Implementation

Expr pbLe(Map<Expr, int> args, int k) {
  final argsPtr = calloc<Z3_ast>(args.length);
  final coeffsPtr = calloc<Int>(args.length);
  try {
    var i = 0;
    for (final MapEntry(:key, :value) in args.entries) {
      argsPtr[i] = _createAST(key);
      coeffsPtr[i] = value;
      i++;
    }
    final result = _z3.mk_pble(args.length, argsPtr, coeffsPtr, k);
    return _getExpr(result);
  } finally {
    malloc.free(argsPtr);
    malloc.free(coeffsPtr);
  }
}