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