Method of

src/api/java/Quantifier.java:175–207

Create a quantified expression. @param ctx Context to create the quantifier on. @param isForall Quantifier type. @param sorts Sorts of bound variables. @param names Names of bound variables @param body Body of quantifier @param weight Weight used to indicate priority for quantifier instantiation @p

(
            Context ctx, boolean isForall, Sort[] sorts, Symbol[] names,
            Expr<BoolSort> body, int weight, Pattern[] patterns, Expr<?>[] noPatterns,
            Symbol quantifierID, Symbol skolemID)

     * @param skolemID Nullable skolemID
     */
    public static Quantifier of(
            Context ctx, boolean isForall, Sort[] sorts, Symbol[] names,
            Expr<BoolSort> body, int weight, Pattern[] patterns, Expr<?>[] noPatterns,
            Symbol quantifierID, Symbol skolemID) {
        ctx.checkContextMatch(patterns);
        ctx.checkContextMatch(noPatterns);
        ctx.checkContextMatch(sorts);
        ctx.checkContextMatch(names);
        ctx.checkContextMatch(body);

        if (sorts.length != names.length) {
            throw new Z3Exception(
                    "Number of sorts does not match number of names");
        }

        long nativeObj;
        if (noPatterns == null && quantifierID == null && skolemID == null) {
            nativeObj = Native.mkQuantifier(ctx.nCtx(), (isForall), weight, AST.arrayLength(patterns), AST
                    .arrayToNative(patterns), AST.arrayLength(sorts), AST
                    .arrayToNative(sorts), Symbol.arrayToNative(names), body
                    .getNativeObject());
        } else {
            nativeObj = Native.mkQuantifierEx(ctx.nCtx(),
                    (isForall), weight, AST.getNativeObject(quantifierID),
                    AST.getNativeObject(skolemID),
                    AST.arrayLength(patterns), AST.arrayToNative(patterns),
                    AST.arrayLength(noPatterns), AST.arrayToNative(noPatterns),
                    AST.arrayLength(sorts), AST.arrayToNative(sorts),
                    Symbol.arrayToNative(names),
                    body.getNativeObject());
        }
        return new Quantifier(ctx, nativeObj);
    }


    /**