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 ()
D	getDomain (int idx)
R	getRange ()
int	getArity ()
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)
int	getDepth ()
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

Array sorts.

Definition at line 24 of file ArraySort.java.

Member Function Documentation

getArity()

int getArity ( )

inline

The number of dimensions of the array sort.

Exceptions

Z3Exception

on error

Returns

an int

Definition at line 67 of file ArraySort.java.

    {
        return Native.getArrayArity(getContext().nCtx(), getNativeObject());
    }

getDomain() [1/2]

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.

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

getDomain() [2/2]

D getDomain ( int  idx )

inline

The domain of a multi-dimensional array sort.

Exceptions

Z3Exception
Z3Exception	on error

Returns

a sort

Definition at line 44 of file ArraySort.java.

    {
        return (D) Sort.create(getContext(),
                               Native.getArraySortDomainN(getContext().nCtx(), getNativeObject(), idx));
    }

getRange()

R getRange ( )

inline

The range of the array sort.

Exceptions

Z3Exception
Z3Exception	on error

Returns

a sort

Definition at line 56 of file ArraySort.java.

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