Z3 |

Public Member Functions
TupleSort Class Reference
Inheritance diagram for TupleSort:

## Public Member Functions
FuncDecl< TupleSort > | mkDecl ()
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
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

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 }
com.microsoft.z3.FuncDecl<?>
com.microsoft.z3.TupleSort.getNumFields
int getNumFields()
Definition: TupleSort.java:39

## ◆ 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 }