Z3
Public Member Functions
TupleSort Class Reference
+ Inheritance diagram for TupleSort:

Public Member Functions

FuncDecl< TupleSortmkDecl ()
 
int getNumFields ()
 
FuncDecl<?>[] getFieldDecls ()
 
- 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
int compareTo (AST other)
 
Z3_ast_kind getASTKind ()
 
boolean isExpr ()
 
boolean isApp ()
 
boolean isVar ()
 
boolean isQuantifier ()
 
boolean isSort ()
 
boolean isFuncDecl ()
 
String getSExpr ()
 

Additional Inherited Members

- Static Public Member Functions inherited from Z3Object
static long[] arrayToNative (Z3Object[] a)
 
static int arrayLength (Z3Object[] a)
 

Detailed Description

Tuple sorts.

Definition at line 23 of file TupleSort.java.

Member Function Documentation

◆ getFieldDecls()

FuncDecl<?> [] getFieldDecls ( )
inline

The field declarations.

Exceptions
Z3Exception

Definition at line 48 of file TupleSort.java.

49  {
50 
51  int n = getNumFields();
52  FuncDecl<?>[] res = new FuncDecl[n];
53  for (int i = 0; i < n; i++)
54  res[i] = new FuncDecl<>(getContext(), Native.getTupleSortFieldDecl(
55  getContext().nCtx(), getNativeObject(), i));
56  return res;
57  }

◆ getNumFields()

int getNumFields ( )
inline

The number of fields in the tuple.

Definition at line 39 of file TupleSort.java.

40  {
41  return Native.getTupleSortNumFields(getContext().nCtx(), getNativeObject());
42  }

Referenced by TupleSort.getFieldDecls().

◆ mkDecl()

FuncDecl<TupleSort> mkDecl ( )
inline

The constructor function of the tuple.

Exceptions
Z3Exception

Definition at line 29 of file TupleSort.java.

30  {
31 
32  return new FuncDecl<>(getContext(), Native.getTupleSortMkDecl(getContext()
33  .nCtx(), getNativeObject()));
34  }