Method evalExample2

examples/java/JavaExample.java:1877–1922

(Context ctx)

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

    public void evalExample2(Context ctx)
    {
        System.out.println("EvalExample2");
        Log.append("EvalExample2");

        Sort int_type = ctx.getIntSort();
        TupleSort tuple = ctx.mkTupleSort(ctx.mkSymbol("mk_tuple"), // name of
                                                                    // tuple
                                                                    // constructor
                new Symbol[] { ctx.mkSymbol("first"), ctx.mkSymbol("second") }, // names
                                                                                // of
                                                                                // projection
                                                                                // operators
                new Sort[] { int_type, int_type } // types of projection
                                                  // operators
                );
        FuncDecl first = tuple.getFieldDecls()[0]; // declarations are for
                                                   // projections
        FuncDecl second = tuple.getFieldDecls()[1];
        Expr tup1 = ctx.mkConst("t1", tuple);
        Expr tup2 = ctx.mkConst("t2", tuple);

        Solver solver = ctx.mkSolver();

        /* assert tup1 != tup2 */
        solver.add(ctx.mkNot(ctx.mkEq(tup1, tup2)));
        /* assert first tup1 = first tup2 */
        solver.add(ctx.mkEq(ctx.mkApp(first, tup1), ctx.mkApp(first, tup2)));

        /* find model for the constraints above */
        Model model = null;
        if (Status.SATISFIABLE == solver.check())
        {
            model = solver.getModel();
            System.out.println(model);
            System.out.println("evaluating tup1 "
                    + (model.evaluate(tup1, false)));
            System.out.println("evaluating tup2 "
                    + (model.evaluate(tup2, false)));
            System.out.println("evaluating second(tup2) "
                    + (model.evaluate(ctx.mkApp(second, tup2), false)));
        } else
        {
            System.out.println("BUG, the constraints are satisfiable.");
        }
    }

    // / Demonstrate how to use <code>Push</code>and <code>Pop</code>to
    // / control the size of models.