Public Member Functions | |
int | getArity () throws Z3Exception |
Sort[] | getColumnSorts () throws Z3Exception |
Package Functions | |
RelationSort (Context ctx, long obj) throws Z3Exception |
Relation sorts.
Definition at line 23 of file RelationSort.java.
RelationSort | ( | Context | ctx, |
long | obj | ||
) | throws Z3Exception [inline, package] |
Definition at line 53 of file RelationSort.java.
{ super(ctx, obj); }
int getArity | ( | ) | throws Z3Exception [inline] |
The arity of the relation sort.
Definition at line 28 of file RelationSort.java.
Referenced by RelationSort.getColumnSorts().
{ return Native.getRelationArity(getContext().nCtx(), getNativeObject()); }
Sort [] getColumnSorts | ( | ) | throws Z3Exception [inline] |
The sorts of the columns of the relation sort.
Z3Exception |
Definition at line 37 of file RelationSort.java.
{ if (m_columnSorts != null) return m_columnSorts; int n = getArity(); Sort[] res = new Sort[n]; for (int i = 0; i < n; i++) res[i] = Sort.create(getContext(), Native.getRelationColumn(getContext() .nCtx(), getNativeObject(), i)); return res; }