Method quantifierExample2

examples/java/JavaGenericExample.java:587–637

(Context ctx)

    }

    void quantifierExample2(Context ctx)
    {

        System.out.println("QuantifierExample2");
        Log.append("QuantifierExample2");

        Quantifier q1, q2;
        FuncDecl<IntSort> f = ctx.mkFuncDecl("f", ctx.getIntSort(), ctx.getIntSort());
        FuncDecl<IntSort> g = ctx.mkFuncDecl("g", ctx.getIntSort(), ctx.getIntSort());

        // Quantifier with Exprs as the bound variables.
        {
            Expr<IntSort> x = ctx.mkConst("x", ctx.getIntSort());
            Expr<IntSort> y = ctx.mkConst("y", ctx.getIntSort());
            Expr<IntSort> f_x = ctx.mkApp(f, x);
            Expr<IntSort> f_y = ctx.mkApp(f, y);
            Expr<IntSort> g_y = ctx.mkApp(g, y);
            @SuppressWarnings("unused")
            Pattern[] pats = new Pattern[] { ctx.mkPattern(f_x, g_y) };
            Expr[] no_pats = new Expr[] { f_y };
            Expr[] bound = new Expr[] { x, y };
            BoolExpr body = ctx.mkAnd(ctx.mkEq(f_x, f_y), ctx.mkEq(f_y, g_y));

            q1 = ctx.mkForall(bound, body, 1, null, no_pats, ctx.mkSymbol("q"),
                    ctx.mkSymbol("sk"));

            System.out.println(q1);
        }

        // Quantifier with de-Bruijn indices.
        {
            Expr<IntSort> x = ctx.mkBound(1, ctx.getIntSort());
            Expr<IntSort> y = ctx.mkBound(0, ctx.getIntSort());
            Expr<IntSort> f_x = ctx.mkApp(f, x);
            Expr<IntSort> f_y = ctx.mkApp(f, y);
            Expr<IntSort> g_y = ctx.mkApp(g, y);
            @SuppressWarnings("unused")
            Pattern[] pats = new Pattern[] { ctx.mkPattern(f_x, g_y) };
            Expr[] no_pats = new Expr[] { f_y };
            Symbol[] names = new Symbol[] { ctx.mkSymbol("x"),
                    ctx.mkSymbol("y") };
            Sort[] sorts = new Sort[] { ctx.getIntSort(), ctx.getIntSort() };
            BoolExpr body = ctx.mkAnd(ctx.mkEq(f_x, f_y), ctx.mkEq(f_y, g_y));

            q2 = ctx.mkForall(sorts, names, body, 1, null, // pats,
                    no_pats, ctx.mkSymbol("q"), ctx.mkSymbol("sk"));
            System.out.println(q2);
        }

        System.out.println(q1.equals(q2));
    }

    // / Prove that <tt>f(x, y) = f(w, v) implies y = v</tt> when
    // / <code>f</code> is injective in the second argument. <seealso