Method enumExampleUntyped

examples/java/JavaGenericExample.java:1364–1402

(Context ctx)

    // while you can do this untyped, it's safer to have a helper function -- this will prevent you from
    // mixing up your enum types
    public void enumExampleUntyped(Context ctx) throws TestFailedException
    {
        System.out.println("EnumExample");
        Log.append("EnumExample");

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

        EnumSort<Object> fruit = ctx.mkEnumSort(name, ctx.mkSymbol("apple2"),
                ctx.mkSymbol("banana2"), ctx.mkSymbol("orange2"));

        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<Object>> apple = fruit.getConsts()[0];
        Expr<EnumSort<Object>> banana = fruit.getConsts()[1];
        Expr<EnumSort<Object>> 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<Object>> 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);
    }

    // / Create a list datatype.