Method enumExample

examples/java/JavaExample.java:1536–1579

(Context ctx)

    // / Create an enumeration data type.

    public void enumExample(Context ctx) throws TestFailedException
    {
        System.out.println("EnumExample");
        Log.append("EnumExample");

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

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

        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 apple = fruit.getConsts()[0];
        Expr banana = fruit.getConsts()[1];
        Expr 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, (BoolExpr) ctx.mkApp(fruit.getTesterDecls()[0], apple),
                false);

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

        Expr 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.