solver_congruence_root method

Z3_ast solver_congruence_root(Z3_context c, Z3_solver s, Z3_ast a)

\brief retrieve the congruence closure root of an expression. The root is retrieved relative to the state where the solver was in when it completed. If it completed during a set of case splits, the congruence roots are relative to these case splits. That is, the congruences are not consequences but they are true under the current state.

def_API('Z3_solver_congruence_root', AST, (_in(CONTEXT), _in(SOLVER), _in(AST)))

Implementation

Z3_ast solver_congruence_root(
  Z3_context c,
  Z3_solver s,
  Z3_ast a,
) {
  return _solver_congruence_root(
    c,
    s,
    a,
  );
}