Method mkSelect

src/api/java/Context.java:1868–1876

Array read. Remarks: The argument a is the array and i is the index of the array that gets read. The node a must have an array sort [domain -> range], and i must have the sort domain. The sort of the result is range. @see #mkArraySort(Sort[]

(Expr<ArraySort<D, R>> a, Expr<D> i)

     * @see #mkStore(Expr<ArraySort<D, R>> a, Expr<D> i, Expr<R> v)
     **/
    public final <D extends Sort, R extends Sort> Expr<R> mkSelect(Expr<ArraySort<D, R>> a, Expr<D> i)
    {
        checkContextMatch(a);
        checkContextMatch(i);
        return (Expr<R>) Expr.create(
                this,
                Native.mkSelect(nCtx(), a.getNativeObject(),
                        i.getNativeObject()));
    }

    /**
     * Array read.