Method proveExample1

examples/java/JavaGenericExample.java:984–1021

(Context ctx)

    // / <remarks>This function demonstrates how to create uninterpreted
    // / types and functions.</remarks>
    public void proveExample1(Context ctx) throws TestFailedException
    {
        System.out.println("ProveExample1");
        Log.append("ProveExample1");

        /* create uninterpreted type. */
        UninterpretedSort U = ctx.mkUninterpretedSort(ctx.mkSymbol("U"));

        /* declare function g */
        FuncDecl<UninterpretedSort> g = ctx.mkFuncDecl("g", U, U);

        /* create x and y */
        Expr<UninterpretedSort> x = ctx.mkConst("x", U);
        Expr<UninterpretedSort> y = ctx.mkConst("y", U);
        /* create g(x), g(y) */
        Expr<UninterpretedSort> gx = g.apply(x);
        Expr<UninterpretedSort> gy = g.apply(y);

        /* assert x = y */
        BoolExpr eq = ctx.mkEq(x, y);

        /* prove g(x) = g(y) */
        BoolExpr f = ctx.mkEq(gx, gy);
        System.out.println("prove: x = y implies g(x) = g(y)");
        prove(ctx, ctx.mkImplies(eq, f), false);

        /* create g(g(x)) */
        Expr<UninterpretedSort> ggx = g.apply(gx);

        /* disprove g(g(x)) = g(y) */
        f = ctx.mkEq(ggx, gy);
        System.out.println("disprove: x = y implies g(g(x)) = g(y)");
        disprove(ctx, ctx.mkImplies(eq, f), false);

        /* Print the model using the custom model printer */
        Model m = check(ctx, ctx.mkNot(f), Status.SATISFIABLE);
        System.out.println(m);
    }

    // / Prove <tt>not(g(g(x) - g(y)) = g(z)), x + z <= y <= x implies z < 0
    // </tt>.