/**
Copyright (c) 2012-2014 Microsoft Corporation
   
Module Name:

    DatatypeSort.java

Abstract:

Author:

    @author Christoph Wintersteiger (cwinter) 2012-03-15

Notes:
    
**/

package com.microsoft.z3;

/**
 * Datatype sorts.
 **/
public class DatatypeSort extends Sort
{
    /**
     * The number of constructors of the datatype sort.
     * @throws Z3Exception on error
     * @return an int
     **/
    public int getNumConstructors()
    {
        return Native.getDatatypeSortNumConstructors(getContext().nCtx(),
                getNativeObject());
    }

    /**
     * The constructors.
     * 
     * @throws Z3Exception
     * @throws Z3Exception on error
     **/
    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;
    }

    /**
     * The recognizers.
     * 
     * @throws Z3Exception
     * @throws Z3Exception on error
     **/
    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;
    }

    /**
     * The constructor accessors.
     * 
     * @throws Z3Exception
     * @throws Z3Exception on error
     **/
    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)));

    }
};
