Method simplifierExample

examples/java/JavaExample.java:2017–2031

(Context ctx)

    // / Simplifier example.

    public void simplifierExample(Context ctx)
    {
        System.out.println("SimplifierExample");
        Log.append("SimplifierExample");

        IntExpr x = ctx.mkIntConst("x");
        IntExpr y = ctx.mkIntConst("y");
        IntExpr z = ctx.mkIntConst("z");
        @SuppressWarnings("unused")
        IntExpr u = ctx.mkIntConst("u");

        Expr t1 = ctx.mkAdd(x, ctx.mkSub(y, ctx.mkAdd(x, z)));
        Expr t2 = t1.simplify();
        System.out.println((t1) + " -> " + (t2));
    }

    // / Extract unsatisfiable core example