Method mkMap

src/api/java/Context.java:1979–1987

Maps f on the argument arrays. Remarks: Each element of args must be of an array sort [domain_i -> range_i]. The function declaration f must have type range_1 .. range_n -> range. v must have sort range. The sort of the result is [domain_i -> range].

(FuncDecl<R2> f, Expr<ArraySort<D, R1>>... args)

     **/
    @SafeVarargs
    public final <D extends Sort, R1 extends Sort, R2 extends Sort> ArrayExpr<D, R2> mkMap(FuncDecl<R2> f, Expr<ArraySort<D, R1>>... args)
    {
        checkContextMatch(f);
        checkContextMatch(args);
        return (ArrayExpr<D, R2>) Expr.create(this, Native.mkMap(nCtx(),
                f.getNativeObject(), AST.arrayLength(args),
                AST.arrayToNative(args)));
    }

    /**
     * Access the array default value.