Z3 |

Public Member Functions
RelationSort Class Reference
Inheritance diagram for RelationSort:

## Public Member Functions
int | getArity ()
Sort[] | getColumnSorts ()
Public Member Functions inherited from Sort
boolean | equals (Object o)
int | hashCode ()
int | getId ()
Z3_sort_kind | getSortKind ()
Symbol | getName ()
String | toString ()
Sort | translate (Context ctx)
Public Member Functions inherited from AST
boolean | equals (Object o)
int | compareTo (AST other)
int | hashCode ()
int | getId ()
AST | translate (Context ctx)
Z3_ast_kind | getASTKind ()
boolean | isExpr ()
boolean | isApp ()
boolean | isVar ()
boolean | isQuantifier ()
boolean | isSort ()
boolean | isFuncDecl ()
String | toString ()
String | getSExpr ()

## Additional Inherited Members
Static Public Member Functions inherited from Z3Object
static long[] | arrayToNative (Z3Object[] a)
static int | arrayLength (Z3Object[] a)

## Detailed Description

Relation sorts.

Definition at line 23 of file RelationSort.java.

## Member Function Documentation

## ◆ getArity()

int getArity | ( |  | ) |
| inline

The arity of the relation sort.

Definition at line 28 of file RelationSort.java.

29 {
30 return Native.getRelationArity(getContext().nCtx(), getNativeObject());
31 }

Referenced by RelationSort.getColumnSorts().

## ◆ getColumnSorts()

Sort[] getColumnSorts | ( |  | ) |
| inline

The sorts of the columns of the relation sort.

Exceptions

  Z3Exception |

Definition at line 37 of file RelationSort.java.

38 {
39
40 if (m_columnSorts != null)
41 return m_columnSorts;
42
43 int n = getArity();
44 Sort[] res = new Sort[n];
45 for (int i = 0; i < n; i++)
46 res[i] = Sort.create(getContext(), Native.getRelationColumn(getContext()
47 .nCtx(), getNativeObject(), i));
48 return res;
49 }
com.microsoft.z3.RelationSort.getArity
int getArity()
Definition: RelationSort.java:28