Function z3_sys::Z3_benchmark_to_smtlib_string [−][src]
pub unsafe extern "C" fn Z3_benchmark_to_smtlib_string(
c: Z3_context,
name: Z3_string,
logic: Z3_string,
status: Z3_string,
attributes: Z3_string,
num_assumptions: c_uint,
assumptions: *const Z3_ast,
formula: Z3_ast
) -> Z3_string
Expand description
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
Z3_benchmark_to_smtlib_string
.
c
: - context.name
: - name of benchmark. The argument is optional.logic
: - the benchmark logic.status
: - the status string (sat, unsat, or unknown)attributes
: - other attributes, such as source, difficulty or category.num_assumptions
: - number of assumptions.assumptions
: - auxiliary assumptions.formula
: - formula to be checked for consistency in conjunction with assumptions.