Method enumExampleTyped

examples/java/JavaGenericExample.java:1321–1360

(Context ctx)

    // / Create an enumeration data type.

    public <T extends Sort> void enumExampleTyped(Context ctx) throws TestFailedException
    {
        System.out.println("EnumExample");
        Log.append("EnumExample");

        Symbol name = ctx.mkSymbol("fruit");

        EnumSort<T> fruit = ctx.mkEnumSort(name, ctx.mkSymbol("apple"),
                ctx.mkSymbol("banana"), ctx.mkSymbol("orange"));

        // helper function for consistent typing: https://docs.oracle.com/javase/tutorial/java/generics/capture.html
        System.out.println((fruit.getConsts()[0]));
        System.out.println((fruit.getConsts()[1]));
        System.out.println((fruit.getConsts()[2]));

        System.out.println((fruit.getTesterDecls()[0]));
        System.out.println((fruit.getTesterDecls()[1]));
        System.out.println((fruit.getTesterDecls()[2]));

        Expr<EnumSort<T>> apple = fruit.getConsts()[0];
        Expr<EnumSort<T>> banana = fruit.getConsts()[1];
        Expr<EnumSort<T>> orange = fruit.getConsts()[2];

        /* Apples are different from oranges */
        prove(ctx, ctx.mkNot(ctx.mkEq(apple, orange)), false);

        /* Apples pass the apple test */
        prove(ctx, ctx.mkApp(fruit.getTesterDecls()[0], apple),
                false);

        /* Oranges fail the apple test */
        disprove(ctx, ctx.mkApp(fruit.getTesterDecls()[0], orange), false);
        prove(ctx, ctx.mkNot(ctx.mkApp(fruit.getTesterDecls()[0], orange)), false);

        Expr<EnumSort<T>> fruity = ctx.mkConst("fruity", fruit);

        /* If something is fruity, then it is an apple, banana, or orange */

        prove(ctx, ctx.mkOr(ctx.mkEq(fruity, apple), ctx.mkEq(fruity, banana), ctx.mkEq(fruity, orange)), false);
    }

    // while you can do this untyped, it's safer to have a helper function -- this will prevent you from
    // mixing up your enum types