Skip to main content

cvc5_get_difficulty

Function cvc5_get_difficulty 

Source
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.