mk_atmost method

Z3_ast mk_atmost(
  1. Z3_context c,
  2. int num_args,
  3. Pointer<Z3_ast> args,
  4. int k,
)

\brief Pseudo-Boolean relations.

Encode p1 + p2 + ... + pn <= k

def_API('Z3_mk_atmost', AST, (_in(CONTEXT), _in(UINT), _in_array(1,AST), _in(UINT)))

Implementation

Z3_ast mk_atmost(
  Z3_context c,
  int num_args,
  ffi.Pointer<Z3_ast> args,
  int k,
) {
  return _mk_atmost(
    c,
    num_args,
    args,
    k,
  );
}