EnumSort.java

Go to the documentation of this file.

package com.microsoft.z3;

public class EnumSort extends Sort
{
    public FuncDecl[] getConstDecls()
    {
        int n = Native.getDatatypeSortNumConstructors(getContext().nCtx(), getNativeObject());
        FuncDecl[] t = new FuncDecl[n];
        for (int i = 0; i < n; i++)
            t[i] = new FuncDecl(getContext(), Native.getDatatypeSortConstructor(getContext().nCtx(), getNativeObject(), i));
        return t;
    }
    
    public FuncDecl getConstDecl(int inx)
    {
        return new FuncDecl(getContext(), Native.getDatatypeSortConstructor(getContext().nCtx(), getNativeObject(), inx));
    }

    public Expr[] getConsts()
    {        
        FuncDecl[] cds = getConstDecls();
        Expr[] t = new Expr[cds.length];
        for (int i = 0; i < t.length; i++)
            t[i] = getContext().mkApp(cds[i]);
        return t;
    }
    
    public Expr getConst(int inx)
    {        
        return getContext().mkApp(getConstDecl(inx));
    }

    public FuncDecl[] getTesterDecls()
    {
        int n = Native.getDatatypeSortNumConstructors(getContext().nCtx(), getNativeObject());
        FuncDecl[] t = new FuncDecl[n];
        for (int i = 0; i < n; i++)
            t[i] = new FuncDecl(getContext(), Native.getDatatypeSortRecognizer(getContext().nCtx(), getNativeObject(), i));
        return t;
    }
    
    public FuncDecl getTesterDecl(int inx)
    {
        return new FuncDecl(getContext(), Native.getDatatypeSortRecognizer(getContext().nCtx(), getNativeObject(), inx));
    }

    EnumSort(Context ctx, Symbol name, Symbol[] enumNames)
    {
        super(ctx, 0);

        int n = enumNames.length;
        long[] n_constdecls = new long[n];
        long[] n_testers = new long[n];
        setNativeObject(Native.mkEnumerationSort(ctx.nCtx(),
                name.getNativeObject(), (int) n, Symbol.arrayToNative(enumNames),
                n_constdecls, n_testers));        
    }
};