Method evalExample2

examples/java/JavaGenericExample.java:1682–1725

(Context ctx)

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

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

        IntSort 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<IntSort> first = (FuncDecl<IntSort>) tuple.getFieldDecls()[0]; // declarations are for
                                                   // projections
        FuncDecl<IntSort> second = (FuncDecl<IntSort>) tuple.getFieldDecls()[1];
        Expr<TupleSort> tup1 = ctx.mkConst("t1", tuple);
        Expr<TupleSort> 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.printf("evaluating tup1 %s%n", model.evaluate(tup1, false));
            System.out.printf("evaluating tup2 %s%n", model.evaluate(tup2, false));
            System.out.printf("evaluating second(tup2) %s%n", 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.