Method proveExample2

examples/java/JavaGenericExample.java:1030–1076

(Context ctx)

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

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

        FuncDecl<IntSort> 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<IntSort> gx = ctx.mkApp(g, x);
        Expr<IntSort> gy = ctx.mkApp(g, y);
        Expr<IntSort> gz = ctx.mkApp(g, z);

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

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

        /* assert x + z <= y */
        ArithExpr<IntSort> 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 */
        IntNum 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.