Method findModelExample1

examples/java/JavaExample.java:1139–1151

(Context ctx)

    // / Find a model for <code>x xor y</code>.

    public void findModelExample1(Context ctx) throws TestFailedException
    {
        System.out.println("FindModelExample1");
        Log.append("FindModelExample1");

        BoolExpr x = ctx.mkBoolConst("x");
        BoolExpr y = ctx.mkBoolConst("y");
        BoolExpr x_xor_y = ctx.mkXor(x, y);

        Model model = check(ctx, x_xor_y, Status.SATISFIABLE);
        System.out.println("x = " + model.evaluate(x, false) + ", y = "
                + model.evaluate(y, false));
    }

    // / Find a model for <tt>x < y + 1, x > 2</tt>.
    // / Then, assert <tt>not(x = y)</tt>, and find another model.