FiniteDomainSort Class Reference

Inheritance diagram for FiniteDomainSort:

Public Member Functions
long	getSize () throws Z3Exception
Package Functions
	FiniteDomainSort (Context ctx, long obj) throws Z3Exception
	FiniteDomainSort (Context ctx, Symbol name, long size) throws Z3Exception

---

Detailed Description

Finite domain sorts.

Definition at line 23 of file FiniteDomainSort.java.

---

Constructor & Destructor Documentation

FiniteDomainSort	(	Context	ctx,
		long	obj
	)		throws Z3Exception [inline, package]

Definition at line 35 of file FiniteDomainSort.java.

        {
                super(ctx, obj);
        }

FiniteDomainSort	(	Context	ctx,
		Symbol	name,
		long	size
	)		throws Z3Exception [inline, package]

Definition at line 40 of file FiniteDomainSort.java.

        {
                super(ctx, Native.mkFiniteDomainSort(ctx.nCtx(), name.getNativeObject(),
                                size));
        }

---

Member Function Documentation

long getSize

(

)

throws Z3Exception [inline]

The size of the finite domain sort.

Definition at line 28 of file FiniteDomainSort.java.

        {
                Native.LongPtr res = new Native.LongPtr();
                Native.getFiniteDomainSortSize(getContext().nCtx(), getNativeObject(), res);
                return res.value;
        }