DatatypeSort.java

Go to the documentation of this file.

package com.microsoft.z3;

public class DatatypeSort extends Sort
{
    public int getNumConstructors()
    {
        return Native.getDatatypeSortNumConstructors(getContext().nCtx(),
                getNativeObject());
    }

    public FuncDecl[] getConstructors()
    {
        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;
    }

    public FuncDecl[] getRecognizers()
    {
        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;
    }

    public FuncDecl[][] getAccessors()
    {

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

    DatatypeSort(Context ctx, long obj)
    {
        super(ctx, obj);
    }

    DatatypeSort(Context ctx, Symbol name, Constructor[] constructors)
           
    {
        super(ctx, Native.mkDatatype(ctx.nCtx(), name.getNativeObject(),
                constructors.length, arrayToNative(constructors)));

    }
};