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 ()
 
- 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 ()
 

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.

Referenced by RelationSort.getColumnSorts().

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

§ 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  }