mk_pbeq method

Z3_ast mk_pbeq(
  1. Z3_context c,
  2. int num_args,
  3. Pointer<Z3_ast> args,
  4. Pointer<Int> coeffs,
  5. int k,
)

\brief Pseudo-Boolean relations.

Encode k1p1 + k2p2 + ... + kn*pn = k

def_API('Z3_mk_pbeq', AST, (_in(CONTEXT), _in(UINT), _in_array(1,AST), _in_array(1,INT), _in(INT)))

Implementation

Z3_ast mk_pbeq(
  Z3_context c,
  int num_args,
  ffi.Pointer<Z3_ast> args,
  ffi.Pointer<ffi.Int> coeffs,
  int k,
) {
  return _mk_pbeq(
    c,
    num_args,
    args,
    coeffs,
    k,
  );
}