mk_transitive_closure method

Z3_func_decl mk_transitive_closure(
  1. Z3_context c,
  2. Z3_func_decl f
)

\brief create transitive closure of binary relation.

\pre f is a binary relation, such that the two arguments have the same sorts.

The resulting relation f+ represents the transitive closure of f.

def_API('Z3_mk_transitive_closure', FUNC_DECL ,(_in(CONTEXT), _in(FUNC_DECL)))

Implementation

Z3_func_decl mk_transitive_closure(
  Z3_context c,
  Z3_func_decl f,
) {
  return _mk_transitive_closure(
    c,
    f,
  );
}