pub unsafe extern "C" fn Z3_get_implied_equalities(
    c: Z3_context,
    s: Z3_solver,
    num_terms: c_uint,
    terms: *const Z3_ast,
    class_ids: *mut c_uint
) -> Z3_lbool
Expand description

Retrieve congruence class representatives for terms.

The function can be used for relying on Z3 to identify equal terms under the current set of assumptions. The array of terms and array of class identifiers should have the same length. The class identifiers are numerals that are assigned to the same value for their corresponding terms if the current context forces the terms to be equal. You cannot deduce that terms corresponding to different numerals must be all different, (especially when using non-convex theories). All implied equalities are returned by this call. This means that two terms map to the same class identifier if and only if the current context implies that they are equal.

A side-effect of the function is a satisfiability check on the assertions on the solver that is passed in. The function return Z3_L_FALSE if the current assertions are not satisfiable.