Method tupleExample

examples/java/JavaGenericExample.java:1147–1176

(Context ctx)

    // / <remarks>Check that the projection of a tuple
    // / returns the corresponding element.</remarks>
    public void tupleExample(Context ctx) throws TestFailedException
    {
        System.out.println("TupleExample");
        Log.append("TupleExample");

        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
                );
        // have to cast here because it is not possible to type a member of an array of mixed generics
        @SuppressWarnings("unchecked")
        FuncDecl<IntSort> first = (FuncDecl<IntSort>) tuple.getFieldDecls()[0]; // declarations are for
                                                   // projections
        @SuppressWarnings("unused")
        FuncDecl<?> second = tuple.getFieldDecls()[1];
        Expr<IntSort> x = ctx.mkConst("x", int_type);
        Expr<IntSort> y = ctx.mkConst("y", int_type);
        Expr<TupleSort> n1 = tuple.mkDecl().apply(x, y);
        Expr<IntSort> n2 = first.apply(n1);
        BoolExpr n3 = ctx.mkEq(x, n2);
        System.out.printf("Tuple example: %s%n", n3);
        prove(ctx, n3, false);
    }

    // / Simple bit-vector example.