Public Member Functions | |
Sort | getDomain () throws Z3Exception |
Sort | getRange () throws Z3Exception |
Package Functions | |
ArraySort (Context ctx, long obj) throws Z3Exception | |
ArraySort (Context ctx, Sort domain, Sort range) throws Z3Exception |
Array sorts.
Definition at line 23 of file ArraySort.java.
ArraySort | ( | Context | ctx, |
long | obj | ||
) | throws Z3Exception [inline, package] |
Definition at line 45 of file ArraySort.java.
{ super(ctx, obj); }
ArraySort | ( | Context | ctx, |
Sort | domain, | ||
Sort | range | ||
) | throws Z3Exception [inline, package] |
Definition at line 50 of file ArraySort.java.
{ super(ctx, Native.mkArraySort(ctx.nCtx(), domain.getNativeObject(), range.getNativeObject())); }
Sort getDomain | ( | ) | throws Z3Exception [inline] |
The domain of the array sort.
Z3Exception |
Definition at line 29 of file ArraySort.java.
{ return Sort.create(getContext(), Native.getArraySortDomain(getContext().nCtx(), getNativeObject())); }
Sort getRange | ( | ) | throws Z3Exception [inline] |
The range of the array sort.
Z3Exception |
Definition at line 39 of file ArraySort.java.
{ return Sort.create(getContext(), Native.getArraySortRange(getContext().nCtx(), getNativeObject())); }