pub unsafe extern "C" fn cvc5_get_difficulty(
cvc5: *mut Cvc5,
size: *mut usize,
inputs: *mut *mut Cvc5Term,
values: *mut *mut Cvc5Term,
)Expand description
Get a difficulty estimate for an asserted formula. This function is intended to be called immediately after any response to a checkSat.
@warning This function is experimental and may change in future versions.
@note The resulting mapping from inputs (which is a subset of the inputs)
to real values is an estimate of how difficult each assertion was to solve.
Unmentioned assertions can be assumed to have zero difficulty.
@param cvc5 The solver instance.
@param size The resulting size of inputs and values.
@param inputs The resulting inputs that are mapped to the resulting values.
@param values The resulting real values.
@note The resulting inputs and values array pointers are only valid
until the next call to this function.