get_relation_column method

Z3_sort get_relation_column(
  1. Z3_context c,
  2. Z3_sort s,
  3. int col
)

\brief Return sort at i'th column of relation sort.

\pre Z3_get_sort_kind(c, s) == Z3_RELATION_SORT \pre col < Z3_get_relation_arity(c, s)

\sa Z3_get_relation_arity

def_API('Z3_get_relation_column', SORT, (_in(CONTEXT), _in(SORT), _in(UINT)))

Implementation

Z3_sort get_relation_column(
  Z3_context c,
  Z3_sort s,
  int col,
) {
  return _get_relation_column(
    c,
    s,
    col,
  );
}