Function Z3_get_relation_column

Source
pub unsafe extern "C" fn Z3_get_relation_column(
    c: Z3_context,
    s: Z3_sort,
    col: c_uint,
) -> Z3_sort
Expand description

Return sort at i’th column of relation sort.

§Preconditions:

  • Z3_get_sort_kind(c, s) == SortKind::Relation
  • col < Z3_get_relation_arity(c, s)

§See also: