Method findSmallModelExample

examples/java/JavaExample.java:2000–2013

(Context ctx)

    // / Reduced-size model generation example.

    public void findSmallModelExample(Context ctx)
    {
        System.out.println("FindSmallModelExample");
        Log.append("FindSmallModelExample");

        BitVecExpr x = ctx.mkBVConst("x", 32);
        BitVecExpr y = ctx.mkBVConst("y", 32);
        BitVecExpr z = ctx.mkBVConst("z", 32);

        Solver solver = ctx.mkSolver();

        solver.add(ctx.mkBVULE(x, ctx.mkBVAdd(y, z)));
        checkSmall(ctx, solver, x, y, z);
    }

    // / Simplifier example.