Method proveExample2

examples/java/JavaExample.java:1241–1289

(Context ctx)

    // functions
    // / and arithmetic.</remarks>
    public void proveExample2(Context ctx) throws TestFailedException
    {
        System.out.println("ProveExample2");
        Log.append("ProveExample2");

        /* declare function g */
        Sort I = ctx.getIntSort();

        FuncDecl g = ctx.mkFuncDecl("g", I, I);

        /* create x, y, and z */
        IntExpr x = ctx.mkIntConst("x");
        IntExpr y = ctx.mkIntConst("y");
        IntExpr z = ctx.mkIntConst("z");

        /* create gx, gy, gz */
        Expr gx = ctx.mkApp(g, x);
        Expr gy = ctx.mkApp(g, y);
        Expr gz = ctx.mkApp(g, z);

        /* create zero */
        IntExpr zero = ctx.mkInt(0);

        /* assert not(g(g(x) - g(y)) = g(z)) */
        ArithExpr gx_gy = ctx.mkSub((IntExpr) gx, (IntExpr) gy);
        Expr ggx_gy = ctx.mkApp(g, gx_gy);
        BoolExpr eq = ctx.mkEq(ggx_gy, gz);
        BoolExpr c1 = ctx.mkNot(eq);

        /* assert x + z <= y */
        ArithExpr x_plus_z = ctx.mkAdd(x, z);
        BoolExpr c2 = ctx.mkLe(x_plus_z, y);

        /* assert y <= x */
        BoolExpr c3 = ctx.mkLe(y, x);

        /* prove z < 0 */
        BoolExpr f = ctx.mkLt(z, zero);
        System.out
                .println("prove: not(g(g(x) - g(y)) = g(z)), x + z <= y <= x implies z < 0");
        prove(ctx, f, false, c1, c2, c3);

        /* disprove z < -1 */
        IntExpr minus_one = ctx.mkInt(-1);
        f = ctx.mkLt(z, minus_one);
        System.out
                .println("disprove: not(g(g(x) - g(y)) = g(z)), x + z <= y <= x implies z < -1");
        disprove(ctx, f, false, c1, c2, c3);
    }

    // / Show how push & pop can be used to create "backtracking" points.