get_implied_equalities method

int get_implied_equalities(Z3_context c, Z3_solver s, int num_terms, Pointer<Z3_ast> terms, Pointer<UnsignedInt> class_ids,)

\brief 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 \c Z3_L_FALSE if the current assertions are not satisfiable.

def_API('Z3_get_implied_equalities', LBOOL, (_in(CONTEXT), _in(SOLVER), _in(UINT), _in_array(2, AST), _out_array(2, UINT)))

Implementation

int get_implied_equalities(
  Z3_context c,
  Z3_solver s,
  int num_terms,
  ffi.Pointer<Z3_ast> terms,
  ffi.Pointer<ffi.UnsignedInt> class_ids,
) {
  return _get_implied_equalities(
    c,
    s,
    num_terms,
    terms,
    class_ids,
  );
}