Method evalExample1

examples/java/JavaGenericExample.java:1642–1678

(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");
        IntNum 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<IntSort> v = model.evaluate(ctx.mkAdd(x, y), false);
            if (v != null)
            {
                System.out.printf("result = %s%n", v);
            } else
            {
                System.out.println("Failed to evaluate: x+y");
            }
        } else
        {
            System.out.println("BUG, the constraints are satisfiable.");
        }
    }

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