DatatypeSort Class Reference

Inheritance diagram for DatatypeSort:

Public Member Functions
int	getNumConstructors () throws Z3Exception
FuncDecl[]	getConstructors () throws Z3Exception
FuncDecl[]	getRecognizers () throws Z3Exception
FuncDecl[][]	getAccessors () throws Z3Exception
Package Functions
	DatatypeSort (Context ctx, long obj) throws Z3Exception
	DatatypeSort (Context ctx, Symbol name, Constructor[] constructors) throws Z3Exception

---

Detailed Description

Datatype sorts.

Definition at line 23 of file DatatypeSort.java.

---

Constructor & Destructor Documentation

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

Definition at line 90 of file DatatypeSort.java.

        {
                super(ctx, obj);
        }

DatatypeSort	(	Context	ctx,
		Symbol	name,
		Constructor[]	constructors
	)		throws Z3Exception [inline, package]

Definition at line 95 of file DatatypeSort.java.

        {
                super(ctx, Native.mkDatatype(ctx.nCtx(), name.getNativeObject(),
                                (int) constructors.length, arrayToNative(constructors)));

        }

---

Member Function Documentation

FuncDecl [][] getAccessors

(

)

throws Z3Exception [inline]

The constructor accessors.

Exceptions:

Z3Exception

Definition at line 69 of file DatatypeSort.java.

        {

                int n = getNumConstructors();
                FuncDecl[][] res = new FuncDecl[n][];
                for (int i = 0; i < n; i++)
                {
                        FuncDecl fd = new FuncDecl(getContext(),
                                        Native.getDatatypeSortConstructor(getContext().nCtx(),
                                                        getNativeObject(), i));
                        int ds = fd.getDomainSize();
                        FuncDecl[] tmp = new FuncDecl[ds];
                        for (int j = 0; j < ds; j++)
                                tmp[j] = new FuncDecl(getContext(),
                                                Native.getDatatypeSortConstructorAccessor(getContext()
                                                                .nCtx(), getNativeObject(), i, j));
                        res[i] = tmp;
                }
                return res;
        }

FuncDecl [] getConstructors

(

)

throws Z3Exception [inline]

The constructors.

Exceptions:

Z3Exception

Definition at line 39 of file DatatypeSort.java.

        {
                int n = getNumConstructors();
                FuncDecl[] res = new FuncDecl[n];
                for (int i = 0; i < n; i++)
                        res[i] = new FuncDecl(getContext(), Native.getDatatypeSortConstructor(
                                        getContext().nCtx(), getNativeObject(), i));
                return res;
        }

int getNumConstructors

(

)

throws Z3Exception [inline]

The number of constructors of the datatype sort.

Definition at line 28 of file DatatypeSort.java.

Referenced by DatatypeSort.getAccessors(), DatatypeSort.getConstructors(), and DatatypeSort.getRecognizers().

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

FuncDecl [] getRecognizers

(

)

throws Z3Exception [inline]

The recognizers.

Exceptions:

Z3Exception

Definition at line 54 of file DatatypeSort.java.

        {
                int n = getNumConstructors();
                FuncDecl[] res = new FuncDecl[n];
                for (int i = 0; i < n; i++)
                        res[i] = new FuncDecl(getContext(), Native.getDatatypeSortRecognizer(
                                        getContext().nCtx(), getNativeObject(), i));
                return res;
        }