Method tupleExample

examples/java/JavaExample.java:1361–1388

(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");

        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
        @SuppressWarnings("unused")
        FuncDecl second = tuple.getFieldDecls()[1];
        Expr x = ctx.mkConst("x", int_type);
        Expr y = ctx.mkConst("y", int_type);
        Expr n1 = tuple.mkDecl().apply(x, y);
        Expr n2 = first.apply(n1);
        BoolExpr n3 = ctx.mkEq(x, n2);
        System.out.println("Tuple example: " + n3);
        prove(ctx, n3, false);
    }

    // / Simple bit-vector example.