Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines
Public Member Functions | Package Functions
ArraySort Class Reference
+ Inheritance diagram for ArraySort:

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

Detailed Description

Array sorts.

Definition at line 23 of file ArraySort.java.


Constructor & Destructor Documentation

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()));
        }

Member Function Documentation

Sort getDomain ( ) throws Z3Exception [inline]

The domain of the array sort.

Exceptions:
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.

Exceptions:
Z3Exception

Definition at line 39 of file ArraySort.java.

        {
                return Sort.create(getContext(),
                                Native.getArraySortRange(getContext().nCtx(), getNativeObject()));
        }
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines