Method mkPattern

src/api/java/Context.java:723–732

Create a quantifier pattern.

(Expr<?>... terms)

     * Create a quantifier pattern.
     **/
    @SafeVarargs
    public final Pattern mkPattern(Expr<?>... terms)
    {
        if (terms.length == 0)
            throw new Z3Exception("Cannot create a pattern from zero terms");

        long[] termsNative = AST.arrayToNative(terms);
        return new Pattern(this, Native.mkPattern(nCtx(), terms.length,
                termsNative));
    }

    /**
     * Creates a new Constant of sort {@code range} and named