Skip to main content

cvc5_simplify

cvc5_sys

Function cvc5_simplify 

Source 
pub unsafe extern "C" fn cvc5_simplify(
    cvc5: *mut Cvc5,
    term: Cvc5Term,
    apply_subs: bool,
) -> Cvc5Term
Expand description

Simplify a formula without doing “much” work.

Does not involve the SAT Engine in the simplification, but uses the current definitions, and assertions. It also involves theory normalization.

@warning This function is experimental and may change in future versions.

@param cvc5 The solver instance. @param term The formula to simplify. @param apply_subs True to apply substitutions for solved variables. @return The simplified formula.