Skip to main content

simplify

Function simplify 

Source
pub unsafe extern "C" fn simplify(
    cvc5: *mut Solver,
    term: Term,
    apply_subs: bool,
) -> Term
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.