(Context ctx)
| 1644 | // / Create a binary tree datatype. |
| 1645 | |
| 1646 | public void treeExample(Context ctx) throws TestFailedException |
| 1647 | { |
| 1648 | System.out.println("TreeExample"); |
| 1649 | Log.append("TreeExample"); |
| 1650 | |
| 1651 | Sort cell; |
| 1652 | FuncDecl nil_decl, is_nil_decl, cons_decl, is_cons_decl, car_decl, cdr_decl; |
| 1653 | Expr nil, l1, l2, x, y, u, v; |
| 1654 | BoolExpr fml, fml1; |
| 1655 | String[] head_tail = new String[] { "car", "cdr" }; |
| 1656 | Sort[] sorts = new Sort[] { null, null }; |
| 1657 | int[] sort_refs = new int[] { 0, 0 }; |
| 1658 | Constructor nil_con, cons_con; |
| 1659 | |
| 1660 | nil_con = ctx.mkConstructor("nil", "is_nil", null, null, null); |
| 1661 | cons_con = ctx.mkConstructor("cons", "is_cons", head_tail, sorts, |
| 1662 | sort_refs); |
| 1663 | Constructor[] constructors = new Constructor[] { nil_con, cons_con }; |
| 1664 | |
| 1665 | cell = ctx.mkDatatypeSort("cell", constructors); |
| 1666 | |
| 1667 | nil_decl = nil_con.ConstructorDecl(); |
| 1668 | is_nil_decl = nil_con.getTesterDecl(); |
| 1669 | cons_decl = cons_con.ConstructorDecl(); |
| 1670 | is_cons_decl = cons_con.getTesterDecl(); |
| 1671 | FuncDecl[] cons_accessors = cons_con.getAccessorDecls(); |
| 1672 | car_decl = cons_accessors[0]; |
| 1673 | cdr_decl = cons_accessors[1]; |
| 1674 | |
| 1675 | nil = ctx.mkConst(nil_decl); |
| 1676 | l1 = ctx.mkApp(cons_decl, nil, nil); |
| 1677 | l2 = ctx.mkApp(cons_decl, l1, nil); |
| 1678 | |
| 1679 | /* nil != cons(nil, nil) */ |
| 1680 | prove(ctx, ctx.mkNot(ctx.mkEq(nil, l1)), false); |
| 1681 | |
| 1682 | /* cons(x,u) = cons(x, v) => u = v */ |
| 1683 | u = ctx.mkConst("u", cell); |
| 1684 | v = ctx.mkConst("v", cell); |
| 1685 | x = ctx.mkConst("x", cell); |
| 1686 | y = ctx.mkConst("y", cell); |
| 1687 | l1 = ctx.mkApp(cons_decl, x, u); |
| 1688 | l2 = ctx.mkApp(cons_decl, y, v); |
| 1689 | prove(ctx, ctx.mkImplies(ctx.mkEq(l1, l2), ctx.mkEq(u, v)), false); |
| 1690 | prove(ctx, ctx.mkImplies(ctx.mkEq(l1, l2), ctx.mkEq(x, y)), false); |
| 1691 | |
| 1692 | /* is_nil(u) or is_cons(u) */ |
| 1693 | prove(ctx, |
| 1694 | ctx.mkOr((BoolExpr) ctx.mkApp(is_nil_decl, u), |
| 1695 | (BoolExpr) ctx.mkApp(is_cons_decl, u)), false); |
| 1696 | |
| 1697 | /* occurs check u != cons(x,u) */ |
| 1698 | prove(ctx, ctx.mkNot(ctx.mkEq(u, l1)), false); |
| 1699 | |
| 1700 | /* destructors: is_cons(u) => u = cons(car(u),cdr(u)) */ |
| 1701 | fml1 = ctx.mkEq( |
| 1702 | u, |
| 1703 | ctx.mkApp(cons_decl, ctx.mkApp(car_decl, u), |
no test coverage detected