Method quantifierExample4

examples/java/JavaGenericExample.java:684–719

(Context ctx)

    // cref="inj_axiom"/>

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

        /*
         * 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 */
        IntSort I = ctx.getIntSort();
        FuncDecl<IntSort> f = ctx.mkFuncDecl("f", new Sort[] { I, I }, I);

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

        /* create x, y, v, w, fxy, fwv */
        IntExpr x = ctx.mkIntConst("x");
        IntExpr y = ctx.mkIntConst("y");
        IntExpr v = ctx.mkIntConst("v");
        IntExpr w = ctx.mkIntConst("w");
        Expr<IntSort> fxy = ctx.mkApp(f, x, y);
        Expr<IntSort> 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);
    }

    // / Some basic tests.