Method treeExample

examples/java/JavaGenericExample.java:1461–1517

(Context ctx)

    // / Create a binary tree datatype.

    @SuppressWarnings("unchecked")
    public <Tree> void treeExample(Context ctx) throws TestFailedException
    {
        System.out.println("TreeExample");
        Log.append("TreeExample");

        String[] head_tail = new String[] { "car", "cdr" };
        Sort[] sorts = new Sort[] { null, null };
        int[] sort_refs = new int[] { 0, 0 };
        Constructor<Tree> nil_con, cons_con;

        nil_con = ctx.mkConstructor("nil", "is_nil", null, null, null);
        cons_con = ctx.mkConstructor("cons", "is_cons", head_tail, sorts,
                sort_refs);
        Constructor<Tree>[] constructors = new Constructor[] { nil_con, cons_con };

        DatatypeSort<Tree> cell = ctx.mkDatatypeSort("cell", constructors);

        FuncDecl<DatatypeSort<Tree>> nil_decl = nil_con.ConstructorDecl();
        FuncDecl<BoolSort> is_nil_decl = nil_con.getTesterDecl();
        FuncDecl<DatatypeSort<Tree>> cons_decl = cons_con.ConstructorDecl();
        FuncDecl<BoolSort> is_cons_decl = cons_con.getTesterDecl();
        FuncDecl<?>[] cons_accessors = cons_con.getAccessorDecls();
        FuncDecl<?> car_decl = cons_accessors[0];
        FuncDecl<?> cdr_decl = cons_accessors[1];

        Expr<DatatypeSort<Tree>> nil = ctx.mkConst(nil_decl);
        Expr<DatatypeSort<Tree>> l1 = ctx.mkApp(cons_decl, nil, nil);
        Expr<DatatypeSort<Tree>> l2 = ctx.mkApp(cons_decl, l1, nil);

        /* nil != cons(nil, nil) */
        prove(ctx, ctx.mkNot(ctx.mkEq(nil, l1)), false);

        /* cons(x,u) = cons(x, v) => u = v */
        Expr<DatatypeSort<Tree>> u = ctx.mkConst("u", cell);
        Expr<DatatypeSort<Tree>> v = ctx.mkConst("v", cell);
        Expr<DatatypeSort<Tree>> x = ctx.mkConst("x", cell);
        Expr<DatatypeSort<Tree>> y = ctx.mkConst("y", cell);
        l1 = ctx.mkApp(cons_decl, x, u);
        l2 = ctx.mkApp(cons_decl, y, v);
        prove(ctx, ctx.mkImplies(ctx.mkEq(l1, l2), ctx.mkEq(u, v)), false);
        prove(ctx, ctx.mkImplies(ctx.mkEq(l1, l2), ctx.mkEq(x, y)), false);

        /* is_nil(u) or is_cons(u) */
        prove(ctx, ctx.mkOr(ctx.mkApp(is_nil_decl, u), ctx.mkApp(is_cons_decl, u)), false);

        /* occurs check u != cons(x,u) */
        prove(ctx, ctx.mkNot(ctx.mkEq(u, l1)), false);

        /* destructors: is_cons(u) => u = cons(car(u),cdr(u)) */
        BoolExpr fml1 = ctx.mkEq(u, ctx.mkApp(cons_decl, ctx.mkApp(car_decl, u), ctx.mkApp(cdr_decl, u)));
        BoolExpr fml = ctx.mkImplies(ctx.mkApp(is_cons_decl, u), fml1);
        System.out.printf("Formula %s%n", fml);
        prove(ctx, fml, false);

        disprove(ctx, fml1, false);
    }