Method evalExample1

examples/java/JavaExample.java:1837–1873

(Context ctx)

    // / Demonstrate how to use #Eval.

    public void evalExample1(Context ctx)
    {
        System.out.println("EvalExample1");
        Log.append("EvalExample1");

        IntExpr x = ctx.mkIntConst("x");
        IntExpr y = ctx.mkIntConst("y");
        IntExpr two = ctx.mkInt(2);

        Solver solver = ctx.mkSolver();

        /* assert x < y */
        solver.add(ctx.mkLt(x, y));

        /* assert x > 2 */
        solver.add(ctx.mkGt(x, two));

        /* find model for the constraints above */
        Model model = null;
        if (Status.SATISFIABLE == solver.check())
        {
            model = solver.getModel();
            System.out.println(model);
            System.out.println("\nevaluating x+y");
            Expr v = model.evaluate(ctx.mkAdd(x, y), false);
            if (v != null)
            {
                System.out.println("result = " + (v));
            } else
            {
                System.out.println("Failed to evaluate: x+y");
            }
        } else
        {
            System.out.println("BUG, the constraints are not satisfiable.");
        }
    }

    // / Demonstrate how to use #Eval on tuples.