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 }