Method getConsts

src/api/java/EnumSort.java:53–60

The constants in the enumeration. @throws Z3Exception on error @return an Expr[]

()

     * @return an Expr[]
     **/
    public Expr<EnumSort<R>>[] 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 (Expr<EnumSort<R>>[]) t;
    }
    
    /**
     * Retrieves the inx'th constant in the enumeration.