Z3 |

Public Member Functions
ArraySort< D extends Sort, R extends Sort > Class Template Reference
Inheritance diagram for ArraySort< D extends Sort, R extends Sort >:

## Public Member Functions
D | getDomain ()
R | getRange ()
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

Array sorts.

Definition at line 24 of file ArraySort.java.

## Member Function Documentation

## ◆ getDomain()

D getDomain | ( |  | ) |
| inline

The domain of the array sort.

Exceptions

  Z3Exception |
  Z3Exception | on error

Returns
  a sort

Definition at line 32 of file ArraySort.java.

33 {
34 return (D) Sort.create(getContext(),
35 Native.getArraySortDomain(getContext().nCtx(), getNativeObject()));
36 }

## ◆ getRange()

R getRange | ( |  | ) |
| inline

The range of the array sort.

Exceptions

  Z3Exception |
  Z3Exception | on error

Returns
  a sort

Definition at line 44 of file ArraySort.java.

45 {
46 return (R) Sort.create(getContext(),
47 Native.getArraySortRange(getContext().nCtx(), getNativeObject()));
48 }