Method isFiniteDomain

src/api/java/Expr.java:2075–2081

Indicates whether the term is of an array sort. @throws Z3Exception on error @return a boolean

()

     * @return a boolean
     **/
    public boolean isFiniteDomain()
    {
        return (Native.isApp(getContext().nCtx(), getNativeObject()) && Native
                .getSortKind(getContext().nCtx(),
                        Native.getSort(getContext().nCtx(), getNativeObject())) == Z3_sort_kind.Z3_FINITE_DOMAIN_SORT
                .toInt());
    }

    /**
     * Indicates whether the term is a less than predicate over a finite domain.