benchmark_to_smtlib_string method

Z3_string benchmark_to_smtlib_string(Z3_context c, Z3_string name, Z3_string logic, Z3_string status, Z3_string attributes, int num_assumptions, Pointer<Z3_ast> assumptions, Z3_ast formula,)

\brief Convert the given benchmark into SMT-LIB formatted string.

\warning The result buffer is statically allocated by Z3. It will be automatically deallocated when #Z3_del_context is invoked. So, the buffer is invalidated in the next call to \c Z3_benchmark_to_smtlib_string.

\param c - context. \param name - name of benchmark. The argument is optional. \param logic - the benchmark logic. \param status - the status string (sat, unsat, or unknown) \param attributes - other attributes, such as source, difficulty or category. \param num_assumptions - number of assumptions. \param assumptions - auxiliary assumptions. \param formula - formula to be checked for consistency in conjunction with assumptions.

def_API('Z3_benchmark_to_smtlib_string', STRING, (_in(CONTEXT), _in(STRING), _in(STRING), _in(STRING), _in(STRING), _in(UINT), _in_array(5, AST), _in(AST)))

Implementation

Z3_string benchmark_to_smtlib_string(
  Z3_context c,
  Z3_string name,
  Z3_string logic,
  Z3_string status,
  Z3_string attributes,
  int num_assumptions,
  ffi.Pointer<Z3_ast> assumptions,
  Z3_ast formula,
) {
  return _benchmark_to_smtlib_string(
    c,
    name,
    logic,
    status,
    attributes,
    num_assumptions,
    assumptions,
    formula,
  );
}