Method quantifierExample3

examples/java/JavaExample.java:691–726

(Context ctx)

    // cref="inj_axiom"/>

    public void quantifierExample3(Context ctx) throws TestFailedException
    {
        System.out.println("QuantifierExample3");
        Log.append("QuantifierExample3");

        /*
         * If quantified formulas are asserted in a logical context, then the
         * model produced by Z3 should be viewed as a potential model.
         */

        /* declare function f */
        Sort I = ctx.getIntSort();
        FuncDecl f = ctx.mkFuncDecl("f", new Sort[] { I, I }, I);

        /* f is injective in the second argument. */
        BoolExpr inj = injAxiom(ctx, f, 1);

        /* create x, y, v, w, fxy, fwv */
        Expr x = ctx.mkIntConst("x");
        Expr y = ctx.mkIntConst("y");
        Expr v = ctx.mkIntConst("v");
        Expr w = ctx.mkIntConst("w");
        Expr fxy = ctx.mkApp(f, x, y);
        Expr fwv = ctx.mkApp(f, w, v);

        /* f(x, y) = f(w, v) */
        BoolExpr p1 = ctx.mkEq(fxy, fwv);

        /* prove f(x, y) = f(w, v) implies y = v */
        BoolExpr p2 = ctx.mkEq(y, v);
        prove(ctx, p2, false, inj, p1);

        /* disprove f(x, y) = f(w, v) implies x = w */
        BoolExpr p3 = ctx.mkEq(x, w);
        disprove(ctx, p3, false, inj, p1);
    }

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