1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310 311 312 313 314 315 316 317 318 319 320 321 322 323 324 325 326 327 328 329 330 331 332 333 334 335 336 337 338 339 340 341 342 343 344 345 346 347 348 349 350 351 352 353 354 355 356 357 358 359 360 361 362 363 364 365 366 367 368 369 370 371 372 373 374 375 376 377 378 379 380 381 382 383 384 385 386 387 388 389 390 391 392 393 394 395 396 397 398 399 400 401 402 403 404 405 406 407 408 409 410 411 412 413 414 415 416 417 418 419 420 421 422 423 424 425 426 427 428 429 430 431 432 433 434 435 436 437 438 439 440 441 442 443 444 445 446 447 448 449 450 451 452 453 454 455 456 457 458 459 460 461 462 463 464 465 466 467 468 469 470 471 472 473 474 475 476 477 478 479 480 481 482 483 484 485 486 487 488 489 490 491 492 493 494 495 496 497 498 499 500 501 502 503 504 505 506 507 508 509 510 511 512 513 514 515 516 517 518 519 520 521 522 523 524 525 526 527 528 529 530 531 532 533 534 535 536 537 538 539 540 541 542 543 544 545 546 547 548 549 550 551 552 553 554 555 556 557 558 559 560 561 562 563 564 565 566 567 568 569 570 571 572 573 574 575 576 577 578 579 580 581 582 583 584 585 586 587 588 589 590 591 592 593 594 595 596 597 598 599 600 601 602 603 604 605 606 607 608 609 610 611 612 613 614 615 616 617 618 619 620 621 622 623 624 625 626 627 628 629 630 631 632 633 634 635 636 637 638 639 640 641 642 643 644 645 646 647 648 649 650 651 652 653 654 655 656 657 658 659 660 661 662 663 664 665 666 667 668 669 670 671 672 673 674 675 676 677 678 679 680 681 682 683 684 685 686 687 688 689 690 691 692 693 694 695 696 697 698 699 700 701 702 703 704 705 706 707 708 709 710 711 712 713 714 715 716 717 718 719 720 721 722 723 724 725 726 727 728 729 730 731 732 733 734 735 736 737 738 739 740 741 742 743 744 745 746 747 748 749 750 751 752 753 754 755 756 757 758 759 760 761 762 763 764 765 766 767 768 769 770 771 772 773 774 775 776 777 778 779 780 781 782 783 784 785 786 787 788 789 790 791 792 793 794 795 796 797 798 799 800 801 802 803 804 805 806 807 808 809 810 811 812 813 814 815 816 817 818 819 820 821 822 823 824 825 826 827 828 829 830 831 832 833 834 835 836 837 838 839 840 841 842 843 844 845 846 847 848 849 850 851 852 853 854 855 856 857 858 859 860 861 862 863 864 865 866 867 868 869 870 871 872 873 874 875 876 877 878 879 880 881 882 883 884 885 886 887 888 889 890 891 892 893 894 895 896 897 898 899 900 901 902 903 904 905 906 907 908 909 910 911 912 913 914 915 916 917 918 919 920 921 922 923 924 925 926 927 928 929 930 931 932 933 934 935 936 937 938 939 940 941 942 943 944 945 946 947 948 949 950 951 952 953 954 955 956 957 958 959 960 961 962 963 964 965 966 967 968 969 970 971 972 973 974 975 976 977 978 979 980 981 982 983 984 985 986 987 988 989 990 991 992 993 994 995 996 997 998 999 1000 1001 1002 1003 1004 1005 1006 1007 1008 1009 1010 1011 1012 1013 1014 1015 1016 1017 1018 1019 1020 1021 1022 1023 1024 1025 1026 1027 1028 1029 1030 1031 1032 1033 1034 1035 1036 1037 1038 1039 1040 1041 1042 1043 1044 1045 1046 1047 1048 1049 1050 1051 1052 1053 1054 1055 1056 1057 1058 1059 1060 1061 1062 1063 1064 1065 1066 1067 1068 1069 1070 1071 1072 1073 1074 1075 1076 1077 1078 1079 1080 1081 1082 1083 1084 1085 1086 1087 1088 1089 1090 1091 1092 1093 1094 1095 1096 1097 1098 1099 1100 1101 1102 1103 1104 1105 1106 1107 1108 1109 1110 1111 1112 1113 1114 1115 1116 1117 1118 1119 1120 1121 1122 1123 1124 1125 1126 1127 1128 1129 1130 1131 1132 1133 1134 1135 1136 1137 1138 1139 1140 1141 1142 1143 1144 1145 1146 1147 1148 1149 1150 1151 1152 1153 1154 1155 1156 1157 1158 1159 1160 1161 1162 1163 1164 1165 1166 1167 1168 1169 1170 1171 1172 1173 1174 1175 1176 1177 1178 1179 1180 1181 1182 1183 1184 1185 1186 1187 1188 1189 1190 1191 1192 1193 1194 1195 1196 1197 1198 1199 1200 1201 1202 1203 1204 1205 1206 1207 1208 1209 1210 1211 1212 1213 1214 1215 1216 1217 1218 1219 1220 1221 1222 1223 1224 1225 1226 1227 1228 1229 1230 1231 1232 1233 1234 1235 1236 1237 1238 1239 1240 1241 1242 1243 1244 1245 1246 1247 1248 1249 1250 1251 1252 1253 1254 1255 1256 1257 1258 1259 1260 1261 1262 1263 1264 1265 1266 1267 1268 1269 1270 1271 1272 1273 1274 1275 1276 1277 1278 1279 1280 1281 1282 1283 1284 1285 1286 1287 1288 1289 1290 1291 1292 1293 1294 1295 1296 1297 1298 1299 1300 1301 1302 1303 1304 1305 1306 1307 1308 1309 1310 1311 1312 1313 1314 1315 1316 1317 1318 1319 1320 1321 1322 1323 1324 1325 1326 1327 1328 1329 1330 1331 1332 1333 1334 1335 1336 1337 1338 1339 1340 1341 1342 1343 1344 1345 1346 1347 1348 1349 1350 1351 1352 1353 1354 1355 1356 1357 1358 1359 1360 1361 1362 1363 1364 1365 1366 1367 1368 1369 1370 1371 1372 1373 1374 1375 1376 1377 1378 1379 1380 1381 1382 1383 1384 1385 1386 1387 1388 1389 1390 1391 1392 1393 1394 1395 1396 1397 1398 1399 1400 1401 1402 1403 1404 1405 1406 1407 1408 1409 1410 1411 1412 1413 1414 1415 1416 1417 1418 1419 1420 1421 1422 1423 1424 1425 1426 1427 1428 1429 1430 1431 1432 1433 1434 1435 1436 1437 1438 1439 1440 1441 1442 1443 1444 1445 1446 1447 1448 1449 1450 1451 1452 1453 1454 1455 1456 1457 1458 1459 1460 1461 1462 1463 1464 1465 1466 1467 1468 1469 1470 1471 1472 1473 1474 1475 1476 1477 1478 1479 1480 1481 1482 1483 1484 1485 1486 1487 1488 1489 1490 1491 1492 1493 1494 1495 1496 1497 1498 1499 1500 1501 1502 1503 1504 1505 1506 1507 1508 1509 1510 1511 1512 1513 1514 1515 1516 1517 1518 1519 1520 1521 1522 1523 1524 1525 1526 1527 1528 1529 1530 1531 1532 1533 1534 1535 1536 1537 1538 1539 1540 1541 1542 1543 1544 1545 1546 1547 1548 1549 1550 1551 1552 1553 1554 1555 1556 1557 1558 1559 1560 1561 1562 1563 1564 1565 1566 1567 1568 1569 1570 1571 1572 1573 1574 1575 1576 1577 1578 1579 1580 1581 1582 1583 1584 1585 1586 1587 1588 1589 1590 1591 1592 1593 1594 1595 1596 1597 1598 1599 1600 1601 1602 1603 1604 1605 1606 1607 1608 1609 1610 1611 1612 1613 1614 1615 1616 1617 1618 1619 1620 1621 1622 1623 1624 1625 1626 1627 1628 1629 1630 1631 1632 1633 1634 1635 1636 1637 1638 1639 1640 1641 1642 1643 1644 1645 1646 1647 1648 1649 1650 1651 1652 1653 1654 1655 1656 1657 1658 1659 1660 1661 1662 1663 1664 1665 1666 1667 1668 1669 1670 1671 1672 1673 1674 1675 1676 1677 1678 1679 1680 1681 1682 1683 1684 1685 1686 1687 1688 1689 1690 1691 1692 1693 1694 1695 1696 1697 1698 1699 1700 1701 1702 1703 1704 1705 1706 1707 1708 1709 1710 1711 1712 1713 1714 1715 1716 1717 1718 1719 1720 1721 1722 1723 1724 1725 1726 1727 1728 1729 1730 1731 1732 1733 1734 1735 1736 1737 1738 1739 1740 1741 1742 1743 1744 1745 1746 1747 1748 1749 1750 1751 1752 1753 1754 1755 1756 1757 1758 1759 1760 1761 1762 1763 1764 1765 1766 1767 1768 1769 1770 1771 1772 1773 1774 1775 1776 1777 1778 1779 1780 1781 1782 1783 1784 1785 1786 1787 1788 1789 1790 1791 1792 1793 1794 1795 1796 1797 1798 1799 1800 1801 1802 1803 1804 1805 1806 1807 1808 1809 1810 1811 1812 1813 1814 1815 1816 1817 1818 1819 1820 1821 1822 1823 1824 1825 1826 1827 1828 1829 1830 1831 1832 1833 1834 1835 1836 1837 1838 1839 1840 1841 1842 1843 1844 1845 1846 1847 1848 1849 1850 1851 1852 1853 1854 1855 1856 1857 1858 1859 1860 1861 1862 1863 1864 1865 1866 1867 1868 1869 1870 1871 1872 1873 1874 1875 1876 1877 1878 1879 1880 1881 1882 1883 1884 1885 1886 1887 1888 1889 1890 1891 1892 1893 1894 1895 1896 1897 1898 1899 1900 1901 1902 1903 1904 1905 1906 1907 1908 1909 1910 1911 1912 1913 1914 1915 1916 1917 1918 1919 1920 1921 1922 1923 1924 1925 1926 1927 1928 1929 1930 1931 1932 1933 1934 1935 1936 1937 1938 1939 1940 1941 1942 1943 1944 1945 1946 1947 1948 1949 1950 1951 1952 1953 1954 1955 1956 1957 1958 1959 1960 1961 1962 1963 1964 1965 1966 1967 1968 1969 1970 1971 1972 1973 1974 1975 1976 1977 1978 1979 1980 1981 1982 1983 1984 1985 1986 1987 1988 1989 1990 1991 1992 1993 1994 1995 1996 1997 1998 1999 2000 2001 2002 2003 2004 2005 2006 2007 2008 2009 2010 2011 2012 2013 2014 2015 2016 2017 2018 2019 2020 2021 2022 2023 2024 2025 2026 2027 2028 2029 2030 2031 2032 2033 2034 2035 2036 2037 2038 2039 2040 2041 2042 2043 2044 2045 2046 2047 2048 2049 2050 2051 2052 2053 2054 2055 2056 2057 2058 2059 2060 2061 2062 2063 2064 2065 2066 2067 2068 2069 2070 2071 2072 2073 2074 2075 2076 2077 2078 2079 2080 2081 2082 2083 2084 2085 2086 2087 2088 2089 2090 2091 2092 2093 2094 2095 2096 2097 2098 2099 2100 2101 2102 2103 2104 2105 2106 2107 2108 2109 2110 2111 2112 2113 2114 2115 2116 2117 2118 2119 2120 2121 2122 2123 2124 2125 2126 2127 2128 2129 2130 2131 2132 2133 2134 2135 2136 2137 2138 2139 2140 2141 2142 2143 2144 2145 2146 2147 2148 2149 2150 2151 2152 2153 2154 2155 2156 2157 2158 2159 2160 2161 2162 2163 2164 2165 2166 2167 2168 2169 2170 2171 2172 2173 2174 2175 2176 2177 2178 2179 2180 2181 2182 2183 2184 2185 2186 2187 2188 2189 2190 2191 2192 2193 2194 2195 2196 2197 2198 2199 2200 2201 2202 2203 2204 2205 2206 2207 2208 2209 2210 2211 2212 2213 2214 2215 2216 2217 2218 2219 2220 2221 2222 2223 2224 2225 2226 2227 2228 2229 2230 2231 2232 2233 2234 2235 2236 2237 2238 2239 2240 2241 2242 2243 2244 2245 2246 2247 2248 2249 2250 2251 2252 2253 2254 2255 2256 2257 2258 2259 2260 2261 2262 2263 2264 2265 2266 2267 2268 2269 2270 2271 2272 2273 2274 2275 2276 2277 2278 2279 2280 2281 2282 2283 2284 2285 2286 2287 2288 2289 2290 2291 2292 2293 2294 2295 2296 2297 2298 2299 2300 2301 2302 2303 2304 2305 2306 2307 2308 2309 2310 2311 2312 2313 2314 2315 2316 2317 2318 2319 2320 2321 2322 2323 2324 2325 2326 2327 2328 2329 2330 2331 2332 2333 2334 2335 2336 2337 2338 2339 2340 2341 2342 2343 2344 2345 2346 2347 2348 2349 2350 2351 2352 2353 2354 2355 2356 2357 2358 2359 2360 2361 2362 2363 2364 2365 2366 2367 2368 2369 2370 2371 2372 2373 2374 2375 2376 2377 2378 2379 2380 2381 2382 2383 2384 2385 2386 2387 2388 2389 2390 2391 2392 2393 2394 2395 2396 2397 2398 2399 2400 2401 2402 2403 2404 2405 2406 2407 2408 2409 2410 2411 2412 2413 2414 2415 2416 2417 2418 2419 2420 2421 2422 2423 2424 2425 2426 2427 2428 2429 2430 2431 2432 2433 2434 2435 2436 2437 2438 2439 2440 2441 2442 2443 2444 2445 2446 2447 2448 2449 2450 2451 2452 2453 2454 2455 2456 2457 2458 2459 2460 2461 2462 2463 2464 2465 2466 2467 2468 2469 2470 2471 2472 2473 2474 2475 2476 2477 2478 2479 2480 2481 2482 2483 2484 2485 2486 2487 2488 2489 2490 2491 2492 2493 2494 2495 2496 2497 2498 2499 2500 2501 2502 2503 2504 2505 2506 2507 2508 2509 2510 2511 2512 2513 2514 2515 2516 2517 2518 2519 2520 2521 2522 2523 2524 2525 2526 2527 2528 2529 2530 2531 2532 2533 2534 2535 2536 2537 2538 2539 2540 2541 2542 2543 2544 2545 2546 2547 2548 2549 2550 2551 2552 2553 2554 2555 2556 2557 2558 2559 2560 2561 2562 2563 2564 2565 2566 2567 2568 2569 2570 2571 2572 2573 2574 2575 2576 2577 2578 2579 2580 2581 2582 2583 2584 2585 2586 2587 2588 2589 2590 2591 2592 2593 2594 2595 2596 2597 2598 2599 2600 2601 2602 2603 2604 2605 2606 2607 2608 2609 2610 2611 2612 2613 2614 2615 2616 2617 2618 2619 2620 2621 2622 2623 2624 2625 2626 2627 2628 2629 2630 2631 2632 2633 2634 2635 2636 2637 2638 2639 2640 2641 2642 2643 2644 2645 2646 2647 2648 2649 2650 2651 2652 2653 2654 2655 2656 2657 2658 2659 2660 2661 2662 2663 2664 2665 2666 2667 2668 2669 2670 2671 2672 2673 2674 2675 2676 2677 2678 2679 2680 2681 2682 2683 2684 2685 2686 2687 2688 2689 2690 2691 2692 2693 2694 2695 2696 2697 2698 2699 2700 2701 2702 2703 2704 2705 2706 2707 2708 2709 2710 2711 2712 2713 2714 2715 2716 2717 2718 2719 2720 2721 2722 2723 2724 2725 2726 2727 2728 2729 2730 2731 2732 2733 2734 2735 2736 2737 2738 2739 2740 2741 2742 2743 2744 2745 2746 2747 2748 2749 2750 2751 2752 2753 2754 2755 2756 2757 2758 2759 2760 2761 2762 2763 2764 2765 2766 2767 2768 2769 2770 2771 2772 2773 2774 2775 2776 2777 2778 2779 2780 2781 2782 2783 2784 2785 2786 2787 2788 2789 2790 2791 2792 2793 2794 2795 2796 2797 2798 2799 2800 2801 2802 2803 2804 2805 2806 2807 2808 2809 2810 2811 2812 2813 2814 2815 2816 2817 2818 2819 2820 2821 2822 2823 2824 2825 2826 2827 2828 2829 2830 2831 2832 2833 2834 2835 2836 2837 2838 2839 2840 2841 2842 2843 2844 2845 2846 2847 2848 2849 2850 2851 2852 2853 2854 2855 2856 2857 2858 2859 2860 2861 2862 2863 2864 2865 2866 2867 2868 2869 2870 2871 2872 2873 2874 2875 2876 2877 2878 2879 2880 2881 2882 2883 2884 2885 2886 2887 2888 2889 2890 2891 2892 2893 2894 2895 2896 2897 2898 2899 2900 2901 2902 2903 2904 2905 2906 2907 2908 2909 2910 2911 2912 2913 2914 2915 2916 2917 2918 2919 2920 2921 2922 2923 2924 2925 2926 2927 2928 2929 2930 2931 2932 2933 2934 2935 2936 2937 2938 2939 2940 2941 2942 2943 2944 2945 2946 2947 2948 2949 2950 2951 2952 2953 2954 2955 2956 2957 2958 2959 2960 2961 2962 2963 2964 2965 2966 2967 2968 2969 2970 2971 2972 2973 2974 2975 2976 2977 2978 2979 2980 2981 2982 2983 2984 2985 2986 2987 2988 2989 2990 2991 2992 2993 2994 2995 2996 2997 2998 2999 3000 3001 3002 3003 3004 3005 3006 3007 3008 3009 3010 3011 3012 3013 3014 3015 3016 3017 3018 3019 3020 3021 3022 3023 3024 3025 3026 3027 3028 3029 3030 3031 3032 3033 3034 3035 3036 3037 3038 3039 3040 3041 3042 3043 3044 3045 3046 3047 3048 3049 3050 3051 3052 3053 3054 3055 3056 3057 3058 3059 3060 3061 3062 3063 3064 3065 3066 3067 3068 3069 3070 3071 3072 3073 3074 3075 3076 3077 3078 3079 3080 3081 3082 3083 3084 3085 3086 3087 3088 3089 3090 3091 3092 3093 3094 3095 3096 3097 3098 3099 3100 3101 3102 3103 3104 3105 3106 3107 3108 3109 3110 3111 3112 3113 3114 3115 3116 3117 3118 3119 3120 3121 3122 3123 3124 3125 3126 3127 3128 3129 3130 3131 3132 3133 3134 3135 3136 3137 3138 3139 3140 3141 3142 3143 3144 3145 3146 3147 3148 3149 3150 3151 3152 3153 3154 3155 3156 3157 3158 3159 3160 3161 3162 3163 3164 3165 3166 3167 3168 3169 3170 3171 3172 3173 3174 3175 3176 3177 3178 3179 3180 3181 3182 3183 3184 3185 3186 3187 3188 3189 3190 3191 3192 3193 3194 3195 3196 3197 3198 3199 3200 3201 3202 3203 3204 3205 3206 3207 3208 3209 3210 3211 3212 3213 3214 3215 3216 3217 3218 3219 3220 3221 3222 3223 3224 3225 3226 3227 3228 3229 3230 3231 3232 3233 3234 3235 3236 3237 3238 3239 3240 3241 3242 3243 3244 3245 3246 3247 3248 3249 3250 3251 3252 3253 3254 3255 3256 3257 3258 3259 3260 3261 3262 3263 3264 3265 3266 3267 3268 3269 3270 3271 3272 3273 3274 3275 3276 3277 3278 3279 3280 3281 3282 3283 3284 3285 3286 3287 3288 3289 3290 3291 3292 3293 3294 3295 3296 3297 3298 3299 3300 3301 3302 3303 3304 3305 3306 3307 3308 3309 3310 3311 3312 3313 3314 3315 3316 3317 3318 3319 3320 3321 3322 3323 3324 3325 3326 3327 3328 3329 3330 3331 3332 3333 3334 3335 3336 3337 3338 3339 3340 3341 3342 3343 3344 3345 3346 3347 3348 3349 3350 3351 3352 3353 3354 3355 3356 3357 3358 3359 3360 3361 3362 3363 3364 3365 3366 3367 3368 3369 3370 3371 3372 3373 3374 3375 3376 3377 3378 3379 3380 3381 3382 3383 3384 3385 3386 3387 3388 3389 3390 3391 3392 3393 3394 3395 3396 3397 3398 3399 3400 3401 3402 3403 3404 3405 3406 3407 3408 3409 3410 3411 3412 3413 3414 3415 3416 3417 3418 3419 3420 3421 3422 3423 3424 3425 3426 3427 3428 3429 3430 3431 3432 3433 3434 3435 3436 3437 3438 3439 3440 3441 3442 3443 3444 3445 3446 3447 3448 3449 3450 3451 3452 3453 3454 3455 3456 3457 3458 3459 3460 3461 3462 3463 3464 3465 3466 3467 3468 3469 3470 3471 3472 3473 3474 3475 3476 3477 3478 3479 3480 3481 3482 3483 3484 3485 3486 3487 3488 3489 3490 3491 3492 3493 3494 3495 3496 3497 3498 3499 3500 3501 3502 3503 3504 3505 3506 3507 3508 3509 3510 3511 3512 3513 3514 3515 3516 3517 3518 3519 3520 3521 3522 3523 3524 3525 3526 3527 3528 3529 3530 3531 3532 3533 3534 3535 3536 3537 3538 3539 3540 3541 3542 3543 3544 3545 3546 3547 3548 3549 3550 3551 3552 3553 3554 3555 3556 3557 3558 3559 3560 3561 3562 3563 3564 3565 3566 3567 3568 3569 3570 3571 3572 3573 3574 3575 3576 3577 3578 3579 3580 3581 3582 3583 3584 3585 3586 3587 3588 3589 3590 3591 3592 3593 3594 3595 3596 3597 3598 3599 3600 3601 3602 3603 3604 3605 3606 3607 3608 3609 3610 3611 3612 3613 3614 3615 3616 3617 3618 3619 3620 3621 3622 3623 3624 3625 3626 3627 3628 3629 3630 3631 3632 3633 3634 3635 3636 3637 3638 3639 3640 3641 3642 3643 3644 3645 3646 3647 3648 3649 3650 3651 3652 3653 3654 3655 3656 3657 3658 3659 3660 3661 3662 3663 3664 3665 3666 3667 3668 3669 3670 3671 3672 3673 3674 3675 3676 3677 3678 3679 3680 3681 3682 3683 3684 3685 3686 3687 3688 3689 3690 3691 3692 3693 3694 3695 3696 3697 3698 3699 3700 3701 3702 3703 3704 3705 3706 3707 3708 3709 3710 3711 3712 3713 3714 3715 3716 3717 3718 3719 3720 3721 3722 3723 3724 3725 3726 3727 3728 3729 3730 3731 3732 3733 3734 3735 3736 3737 3738 3739 3740 3741 3742 3743 3744 3745 3746 3747 3748 3749 3750 3751 3752 3753 3754 3755 3756 3757 3758 3759 3760 3761 3762 3763 3764 3765 3766 3767 3768 3769 3770 3771 3772 3773 3774 3775 3776 3777 3778 3779 3780 3781 3782 3783 3784 3785 3786 3787 3788 3789 3790 3791 3792 3793 3794 3795 3796 3797 3798 3799 3800 3801 3802 3803 3804 3805 3806 3807 3808 3809 3810 3811 3812 3813 3814 3815 3816 3817 3818 3819 3820 3821 3822 3823 3824 3825 3826 3827 3828 3829 3830 3831 3832 3833 3834 3835 3836 3837 3838 3839 3840 3841 3842 3843 3844 3845 3846 3847 3848 3849 3850 3851 3852 3853 3854 3855 3856 3857 3858 3859 3860 3861 3862 3863 3864 3865 3866 3867 3868 3869 3870 3871 3872 3873 3874 3875 3876 3877 3878 3879 3880 3881 3882 3883 3884 3885 3886 3887 3888 3889 3890 3891 3892 3893 3894 3895 3896 3897 3898 3899 3900 3901 3902 3903 3904 3905 3906 3907 3908 3909 3910 3911 3912 3913 3914 3915 3916 3917 3918 3919 3920 3921 3922 3923 3924 3925 3926 3927 3928 3929 3930 3931 3932 3933 3934 3935 3936 3937 3938 3939 3940 3941 3942 3943 3944 3945 3946 3947 3948 3949 3950 3951 3952 3953 3954 3955 3956 3957 3958 3959 3960 3961 3962 3963 3964 3965 3966 3967 3968 3969 3970 3971 3972 3973 3974 3975 3976 3977 3978 3979 3980 3981 3982 3983 3984 3985 3986 3987 3988 3989 3990 3991 3992 3993 3994 3995 3996 3997 3998 3999 4000 4001 4002 4003 4004 4005 4006 4007 4008 4009 4010 4011 4012 4013 4014 4015 4016 4017 4018 4019 4020 4021 4022 4023 4024 4025 4026

; ACL2 Version 3.1  A Computational Logic for Applicative Common Lisp
; Copyright (C) 2006 University of Texas at Austin
; This version of ACL2 is a descendent of ACL2 Version 1.9, Copyright
; (C) 1997 Computational Logic, Inc. See the documentation topic NOTE20.
; This program is free software; you can redistribute it and/or modify
; it under the terms of the GNU General Public License as published by
; the Free Software Foundation; either version 2 of the License, or
; (at your option) any later version.
; This program is distributed in the hope that it will be useful,
; but WITHOUT ANY WARRANTY; without even the implied warranty of
; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
; GNU General Public License for more details.
; You should have received a copy of the GNU General Public License
; along with this program; if not, write to the Free Software
; Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139, USA.
; Written by: Matt Kaufmann and J Strother Moore
; email: Kaufmann@cs.utexas.edu and Moore@cs.utexas.edu
; Department of Computer Sciences
; University of Texas at Austin
; Austin, TX 787121188 U.S.A.
# Table of contents.
0. PRELIMINARY MACROS
I. INTRODUCTION AND DATA TYPES
II. OPALIST
III. HASH OPERATIONS
IV. HASH OPERATIONS: QUOTEPS
V. BDD RULES AND ONEWAY UNIFIER
VI. SOME INTERFACE UTILITIES
VII. MAIN ALGORITHM
VIII. TOPLEVEL (INTERFACE) ROUTINES
IX. COMPILING THIS FILE AND OTHER HELPFUL TIPS
#
; Mxidbound is currently 438619, perhaps too low. We could perhaps fix this
; by changing how we deal with close to 16 args in ophashindex1, and by
; changing 131 in ifhashindex.
(inpackage "ACL2")
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;;; 0. PRELIMINARY MACROS ;;;;;;;;;;;;;;;;;;;;;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(defmacro mvf (x &rest rest)
; We often wish to pass back a multiple value such that the first value is a
; fixnum. Efficiency is apparently improved in GCL when that fixnum is not
; "boxed," but instead is treated as a raw C integer. Currently ACL2 provides
; mechanisms for this, but they require that an appropriate THE expression
; surround such a value when it is the first value passed back by MV. (Note
; that there seems to be no way to keep GCL from boxing fixnums in other than
; the first argument position of MV.)
`(mv (thefixnum ,x) ,@rest))
(defmacro logandf (&rest args)
(xxxjoinfixnum 'logand args 1))
(defmacro logxorf (&rest args)
(xxxjoinfixnum 'logxor args 0))
(defmacro logiorf (&rest args)
(xxxjoinfixnum 'logior args 0))
(defmacro ashf (x y)
(list 'thefixnum
(list 'ash (list 'thefixnum x) (list 'thefixnum y))))
(defmacro mxidbound ()
; This bound on mxid must be such that our calls of +f and *f involving mxid
; produce fixnums. At this writing the most severe such test is in
; ophashindex1; see the comment there.
(1 (floor (fixnumbound) 153)))
(defmacro 1+mxid (x)
; DILEMMA: Do we let this macro box (1+ x) or not, and if so, when? Here are
; some thoughts on the issue.
; Use this macro to increment mxid,in order to guarantee that mxid remains a
; fixnum. X is known to be a nonnegative fixnum; this macro checks that we
; keep it a fixnum by adding 1 to it. It actually checks even more, namely,
; that
`(thefixnum
(let ((x ,x))
(declare (type (signedbyte 29) x))
; Should we really include the declaration above? The main reason seems to be
; in order for the incrementing operation below to run fast, but in fact we
; have done several experiments and it seems that the current version of this
; code is optimal for performance. That's a bit surprising, since each mxid
; gets consed into a list anyhow (a cst), and hence is boxed in GCL (which is
; the only list we are talking about here). So, there wouldn't appear to be
; any particular advantage in wrapping thefixnum around this form. At any
; rate, the performance issues here seem to be quite minor.
; A typical use of this macro is of the form
#
(let ((newmxid (1+mxid mxid)))
(declare (type (signedbyte 29) newmxid))
(let ((newcst (makeleafcst
newmxid
term
nil)))
(mvf newmxid
...)))
#
; Note that makeleafcst will box newmxid  after all, it is consing
; newmxid into a list. The present approach delays this boxing until that
; time, so that we don't have to unbox newmxid in the mvf form above. The
; unboxed newmxid may actually never benefit from being unboxed, and in fact
; we may want to rework our entire bdd code so that mxids are always boxed.
(cond ((< x ,(mxidbound))
(1+f x))
(t (ifix
; This use of ifix looks goofy, but the reason is that we want the compiler
; to behave properly, and we have proclaimed (at least in GCL) that this
; function returns a fixnum.
(erhardval 0 'bdd
"Maximum id for bdds exceeded. Current maximum id is ~x0."
x)))))))
(defmacro bdderror (mxid fmtstring fmtalist badcst ttree)
; Perhaps it would be more "natural" to define this macro to return
; `(mvf ,mxid ,(cons fmtstring ,fmtalist) ,badcst <nilcallstack> ,ttree)
; since then we can view the result as
; `(mvf ,mxid ,<msg> ,badcst ,callstack ,ttree)
; However, we would like to have a very fast test for whether the tuple
; returned designates an error. The present approach allows us to test with
; stringp on the second value returned. We take advantage of that in the
; definition of mvlet?.
; Note that the order of the first two values should not be changed: we
; declare mxid to be a fixnum at some point, and we we want the second
; position to be tested by stringp to see if we have an "error" situation.
; Keep this in sync with mvlet?.
`(mvf ,mxid ,fmtstring (cons ,fmtalist ,badcst)
; The following nil is really an initial value of the bddcallstack that is
; ultimately to be placed in a bddnote. At the time of this writing, mvlet?
; is the only place where we update this stack.
nil
,ttree))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;;; I. INTRODUCTION AND DATA TYPES ;;;;;;;;;;;;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; In this work we represent terms in what we call the cheap syntax. Such a
; "term" is called a "csterm". Bryant would call it a "node."
; We are interested in normalized IF expressions corresponding to ACL2 terms.
; If x is not itself an IF term, then (IF x y z) is represented by
; `(k ,x ,boolp ,y . ,z)
; where k is a natural number that is uniquely associated with <x,y,z> and
; boolp is t if the term is known to be Boolean. The association between k and
; <x,y,z> is arranged via a "hash table" discussed below. The objective is
; that two canonicalized IF expressions are equal (and therefore represent the
; same term) iff their unique identifiers (cars) are =.
; We also represent "leaf" ACL2 terms, which are generally IFfree, as csts of
; a slightly different sort; see below. (Note that these may have IFs in them
; because certain function symbols are "blocked"  see bddconstructors.)
; The list of "leaf" csts arising from variables in the input term, which we
; typically call leafcstlist, is passed around unchanged by various of our
; functions. We rely on the opht to find csts for other leaves, and to avoid
; reconsing up leaf csts.
; The shapes of csts are as follows. Note that two csts are equal iff their
; cars are =.
; Nonleaf:
; (uniqueid tst boolp tbr . fbr) ; informally, represents (if tst tbr fbr)
; Leaf:
; (uniqueid term boolp)
; where term is of one of the following forms:
; variable
; quotep
; application of function symbol other than IF to a list of csts
; WARNING: The definition of leafp below relies on the fact that leaf csts are
; exactly those whose final cdr is nil. Do not succomb to the temptation to
; add a new field as the final cdr without taking this into account.
; Note: It is tempting to replace the "term" in the last case by an ACL2 term,
; rather than an application of a function symbol to a list of csts. However,
; the list of csts has presumably already been consed up, so we save the
; reconsing, awaiting the final decoding to build the actual ACL2 term if
; necessary.
; Macros for accessing canonicalized IFs:
(defmacro uniqueid (x) `(thefixnum (car ,x)))
(defmacro tst (x) `(cadr ,x)) ;a cst, not a number; but beware since tst=trm
;and trm is a sort of term
; Note: We found that 95% of the time on one test was being spent inside
; cstboolp, when we used to keep this information directly in leaf nodes only.
(defmacro cstboolp (x) `(caddr ,x))
(defmacro tbr (x) `(cadddr ,x))
(defmacro fbr (x) `(cddddr ,x))
(defmacro leafp (x)
`(null (cdddr ,x)))
(defmacro trm (x) `(cadr ,x))
(defun bddconstructors (wrld)
(declare (xargs :guard
(and (worldp wrld)
(alistp (tablealist 'acl2defaultstable wrld)))))
(let ((pair (assoceq :bddconstructors (tablealist
'acl2defaultstable wrld))))
(if pair
(cdr pair)
'(cons))))
(defun makeleafcst (uniqueid trm boolp)
; We write the definition this way, rather than simply as something like (list*
; uniqueid trm boolp ), in order to avoid repeatedly consing up '(t . nil) and
; '(nil . nil).
(if boolp
(list* uniqueid trm '(t))
(list* uniqueid trm '(nil))))
(defun evgfnsymb (x)
; This function takes the view that every explicit value can be constructed
; from 0. It returns nil on 0, but, in principle, returns an appropriate
; function symbol otherwise. At this point we choose not to support this idea
; in full, but instead we view cons as the only constructor. We leave the full
; code in place as a comment, in case we choose to support this idea in the
; future.
#
(cond ((consp x) 'cons)
((symbolp x) 'interninpackageofsymbol)
((integerp x)
(cond ((< x 0) 'unary)
((< 0 x) 'binary+)
(t nil)))
((rationalp x)
(if (equal (numerator x) 1)
'unary/
'binary*))
((complexrationalp x)
'complex)
((stringp x) 'coerce)
((characterp x) 'charcode)
(t (er hard 'fnsymb "Unexpected object, ~x0."
x)))
#
(cond ((consp x) 'cons)
(t nil)))
(defun bddconstructortrmp (trm bddconstructors)
(and (consp trm)
(if (fquotep trm)
(membereq (evgfnsymb (cadr trm)) bddconstructors)
(membereq (car trm) bddconstructors))))
(defun evgtype (x)
; This function takes the view that every explicit value can be constructed
; from 0. It returns nil on 0, but, in principle, returns an appropriate
; function symbol otherwise. See also evgfnsymb.
(cond ((consp x) 'consp)
((symbolp x) 'symbol)
((integerp x) 'integer)
((rationalp x) 'rational)
((complexrationalp x) 'complexrational)
((stringp x) 'string)
((characterp x) 'character)
(t (er hard 'fnsymb "Unexpected object, ~x0."
x))))
(defun makeifcst (uniqueid tst tbr fbr bddconstructors)
; The second value returned is always a new cst. The first value is nonnil
; when there is an "error", in which case that value is of the form (fmtstring
; . alist).
(let* ((boolp (and (cstboolp tbr)
(cstboolp fbr)))
(newcst (list* uniqueid tst boolp tbr fbr)))
(cond
((or (and (leafp tbr)
(bddconstructortrmp (trm tbr) bddconstructors))
(and (leafp fbr)
(bddconstructortrmp (trm fbr) bddconstructors)))
(mv (msg "Attempted to create IF node during BDD processing with ~@0, ~
which would produce a nonBDD term (as defined in :DOC ~
bddalgorithm). See :DOC showbdd."
(let ((truefn (trm tbr))
(falsefn (trm fbr)))
(cond
((and (leafp tbr)
(bddconstructortrmp (trm tbr) bddconstructors))
(cond
((and (leafp fbr)
(bddconstructortrmp (trm fbr) bddconstructors))
(msg "true branch with ~#0~[function symbol ~x1~/explicit ~
value of type ~x2~] and false branch with ~
~#3~[function symbol ~x4~/explicit value of type ~
~x5~]"
(if (eq (car truefn) 'quote) 1 0)
(car truefn)
(and (eq (car truefn) 'quote)
(evgtype (cadr truefn)))
(if (eq (car falsefn) 'quote) 1 0)
(car falsefn)
(and (eq (car falsefn) 'quote)
(evgtype (cadr falsefn)))))
(t (msg "true branch with ~#0~[function symbol ~x1~/explicit ~
value of type ~x2~]"
(if (eq (car truefn) 'quote) 1 0)
(car truefn)
(and (eq (car truefn) 'quote)
(evgtype (cadr truefn)))))))
(t (msg "false branch with ~#0~[function symbol ~x1~/explicit ~
value of type ~x2~]"
(if (eq (car falsefn) 'quote) 1 0)
(car falsefn)
(and (eq (car falsefn) 'quote)
(evgtype (cadr falsefn))))))))
newcst))
(t (mv nil newcst)))))
; We will always represent nil and t as described above. To make this work, we
; must set the initial mxid to 2, so the next unique id generated is 3.
; It is nearly inconsequential which of t or nil has the smaller id, but we
; find it handy to give t the smaller id, as noted in a comment in the
; definition of combineopcstscomm.
(defconst *cstt* (makeleafcst 1 *t* t))
(defconst *cstnil* (makeleafcst 2 *nil* t))
(defmacro cst= (cst1 cst2)
`(= (uniqueid ,cst1)
(uniqueid ,cst2)))
(defmacro csttp (cst)
`(= (uniqueid ,cst) 1))
(defmacro cstnilp (cst)
`(= (uniqueid ,cst) 2))
(defmacro cstvarp (cst)
`(< 2 (uniqueid ,cst)))
(defun cstnonnilp (cst)
(and (leafp cst)
(if (quotep (trm cst))
(not (cstnilp cst))
(and (nvariablep (trm cst))
; Consider other types here besides cons, e.g., that of numbers. We may want
; to pass in a list of functions that have been checked to have typesets that
; are disjoint from *tsnil* and variablefree. We would use a membereq test
; below against such a list. This list of function symbols could be determined
; easily from the list of all function symbols in opalist.
(eq (ffnsymb (trm cst)) 'cons)))))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;;; II. OPALIST ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; The goal of this section is to define functions opalist and opalistinfo.
; See those definitions below for more details. Briefly, these functions
; respectively build and do lookup in a socalled opalist, which is a list of
; entries that describe function symbols occurring in the term for which we
; want to build a bdd.
(defun boolmask1 (formals vars rune)
; Formals is the list of formals of a function symbol, and vars is a list of
; variables contained in formals such that every call of that function returns
; either t or nil, assuming that each var in vars is of boolean type. This
; function returns a list in oneone correspondence with formals (but see
; below), replacing a formal by t if it belongs to vars (thus indicating that
; this position's actual might be returned) and nil if not. Rune is a
; typeprescription record, used simply for the final cdr of the list returned
; (after all the t's and nil's have been listed as indicated above).
(cond
((endp formals) rune)
((membereq (car formals) vars)
(cons t (boolmask1 (cdr formals) vars rune)))
(t (cons nil (boolmask1 (cdr formals) vars rune)))))
(defun booleantermvar (x)
; X is a term. If x is of the form (booleanp v) or something "clearly"
; equivalent to it, return v. Otherwise return nil.
(and (not (variablep x))
(not (fquotep x))
(cond
((and (eq (ffnsymb x) 'booleanp)
(variablep (fargn x 1)))
(fargn x 1))
((eq (ffnsymb x) 'if)
; Check for translated version of (or (equal v t) (equal v nil)) or
; (or (equal v nil) (equal v t)).
(let ((test (fargn x 1))
(tbr (fargn x 2))
(fbr (fargn x 3)))
(and (not (variablep test))
(not (fquotep test))
(eq (ffnsymb test) 'equal)
(let ((v (fargn test 1)))
(and (variablep v)
(let ((b (fargn test 2)))
(and (or (equal b *t*) (equal b *nil*))
(let ((c (if (equal b *t*) *nil* *t*)))
(if (and (equal test tbr)
(equal fbr (fconsterm* 'equal v c)))
v
nil)))))))))
(t nil))))
(defun booleanhypsvars (hyps)
; If hyps consists of terms of the form (booleanp v), or perhaps the
; equivalent, then we return a list indices of such v.
(if (endp hyps)
nil
(let ((rst (booleanhypsvars (cdr hyps))))
(if (eq rst t)
t
(let ((v (booleantermvar (car hyps))))
(if v
(cons v rst)
t))))))
(defun firstbooleantypeprescription (typeprescriptionlist ens formals)
; This function finds the most recent enabled typeprescription rule from the
; given list whose :basicts is boolean and :hyps are all of the form (booleanp
; v) or a "clearly" equivalent form, where the :term is of the form (fn ... v
; ...). It returns two values. The first is the :rune of the rule, which is
; nonnil if and only if such a rule is found. If the first value is nonnil,
; then the second value is a "mask" as described in the comment in boolmask.
(cond
((endp typeprescriptionlist)
(mv nil nil))
((and (enablednumep
(access typeprescription (car typeprescriptionlist) :nume)
ens)
(tssubsetp
(access typeprescription (car typeprescriptionlist) :basicts)
*tsboolean*))
(let* ((tp (car typeprescriptionlist))
(hyps (access typeprescription tp :hyps))
(vars (access typeprescription tp :vars)))
(if hyps
(let ((morevars (booleanhypsvars hyps)))
(if (or (eq morevars t)
(not (subsetpeq morevars formals)))
(firstbooleantypeprescription (cdr typeprescriptionlist)
ens
formals)
(mv (access typeprescription tp :rune)
(unioneq vars morevars))))
(mv (access typeprescription tp :rune)
vars))))
(t (firstbooleantypeprescription
(cdr typeprescriptionlist) ens formals))))
(defun recognizerrune (fn recognizeralist wrld ens)
(cond
((endp recognizeralist) nil)
((and (eq fn (access recognizertuple (car recognizeralist) :fn))
(enabledrunep (access recognizertuple (car recognizeralist) :rune)
ens
wrld))
(access recognizertuple (car recognizeralist) :rune))
(t (recognizerrune fn (cdr recognizeralist) wrld ens))))
(defun boolmask (fn recognizeralist wrld ens)
; Returns a "mask" that is a suitable argument to boolflg. Thus, this
; function returns either nil or else a mask of the form
; (list* b1 b2 ... bn rune)
; where rune is a type prescription rune and each bi is either t or nil. The
; function boolflg will check that a given call of fn is boolean, returning
; rune if it can confirm this fact. A bi must be marked t if the conclusion
; that the call of fn is boolean requires a check that the formal corresponding
; to bi is boolean.
; We give special treatment not only to compound recognizers, but also to
; Booleanvalued primitives, since these will not generally have builtin
; typeprescription rules.
(cond
((or (eq fn 'equal) (eq fn '<))
(list* nil nil *fakerunefortypeset*))
((eq fn 'not)
; `Not' is so basic that we could probably skip this case, but we might as well
; handle it appropriately.
(list* nil *fakerunefortypeset*))
(t
(let ((rune (recognizerrune fn recognizeralist wrld ens))
(formals (formals fn wrld)))
(if rune
(boolmask1 formals nil rune)
(mvlet (rune vars)
; We only consider the most recent type prescription with Boolean base type.
; Some day we might consider somehow combining all such type prescription
; rules.
(firstbooleantypeprescription
(getprop fn 'typeprescriptions nil 'currentacl2world wrld)
ens
formals)
(and rune
(boolmask1 formals vars rune))))))))
(defun commutativep1 (fn lemmas ens)
; Fn is assumed to have arity 2 in the current ACL2 world.
(cond
((endp lemmas) nil)
(t (if (and (membereq (access rewriterule (car lemmas) :subclass)
'(backchain abbreviation))
(equal (access rewriterule (car lemmas) :equiv) 'equal)
(enablednumep (access rewriterule (car lemmas) :nume) ens)
(null (access rewriterule (car lemmas) :hyps))
(let ((lhs (access rewriterule (car lemmas) :lhs))
(rhs (access rewriterule (car lemmas) :rhs)))
(and (or (eq (ffnsymb lhs) fn)
(er hard 'commutativep1
"We had thought we had a rewrite rule with :lhs ~
being a call of ~x0, but the :lhs is ~x1."
fn lhs))
(nvariablep rhs)
(not (fquotep rhs))
(eq (ffnsymb rhs) fn)
(variablep (fargn lhs 1))
(variablep (fargn lhs 2))
(not (eq (fargn lhs 1) (fargn lhs 2)))
(equal (fargn lhs 1) (fargn rhs 2))
(equal (fargn lhs 2) (fargn rhs 1)))))
(access rewriterule (car lemmas) :rune)
(commutativep1 fn (cdr lemmas) ens)))))
(defun findequivalencerune (fn rules)
(cond
((endp rules)
nil)
((eq (access congruencerule (car rules) :equiv) fn)
(let ((rune (access congruencerule (car rules) :rune)))
(if (eq (car rune) :equivalence)
rune
(findequivalencerune fn (cdr rules)))))
(t (findequivalencerune fn (cdr rules)))))
(defun equivalencerune1 (fn congruences)
; For example, if fn is 'iff then congruences may contain:
; (EQUAL ((126 IFF :EQUIVALENCE IFFISANEQUIVALENCE))
; ((126 IFF :EQUIVALENCE IFFISANEQUIVALENCE)))
; But the two singleton lists above can contain other members too. See the
; Essay on Equivalence, Refinements, and Congruencebased Rewriting.
; See addequivalencerule.
(cond
((endp congruences)
(er hard 'equivalencerune
"Failed to find an equivalence rune for function symbol ~x0."
fn))
(t (let ((x (car congruences)))
(casematch x
(('equal rules1 rules2)
(let ((rune (findequivalencerune fn rules1)))
(if (and rune
(equal rune (findequivalencerune fn rules2)))
rune
(equivalencerune1 fn (cdr congruences)))))
(& (equivalencerune1 fn (cdr congruences))))))))
(defun equivalencerune (fn wrld)
(declare (xargs :guard (equivalencerelationp fn wrld)))
(cond
((eq fn 'equal)
(fnrunenume 'equal nil nil wrld))
(t (equivalencerune1 fn
(getprop fn 'congruences
'(:error "See equivalencerune.")
'currentacl2world wrld)))))
(defun commutativep (fn ens wrld)
; Note that if the value is nonnil, it is a rune justifying the commutativity
; of the given function.
(and (= (arity fn wrld) 2)
(if (equivalencerelationp fn wrld)
(equivalencerune fn wrld)
(commutativep1 fn
(getprop fn 'lemmas nil 'currentacl2world wrld)
ens))))
; To memoize the various merging operations we will hash on the opcodes.
; Increasing each by a factor of 3 was intended to make it spread out a little
; more, but (at least this has been true at one time) it doesn't have much of
; an effect.
(defun opalist (fns acc i ens wrld)
; Build a list of entries (op opcode commp enabledexecutablecounterpartp
; mask). The next index to use is i. Call this as in (opalist (remove1eq
; 'if (allfnnames term)) nil 6 (ens state) (w state)). Keep this in sync with
; opalistinfo.
; Note that if commp is nonnil, it is a rune justifying the commutativity of
; the given function. Similarly, if enabledexecutablecounterpartp is nonnil
; then it is an :executablecounterpart rune.
(cond
((endp fns) acc)
((> i (mxidbound))
(er hard 'bdd
"We are very surprised to see that, apparently, your problem for bdd ~
processing involves ~x0 function symbols! We cannot handle this many ~
function symbols."
(/ i 3)))
(t (opalist (cdr fns)
(cons (list* (car fns)
i
(commutativep (car fns) ens wrld)
(and (not (getprop (car fns) 'constrainedp nil
'currentacl2world wrld))
(enabledxfnp (car fns) ens wrld)
(fnrunenume (car fns) nil t wrld))
(boolmask (car fns)
(globalval 'recognizeralist wrld)
wrld
ens))
acc)
(+ 3 i)
ens
wrld))))
(defun opalistinfo (fn opalist)
; Returns (mv opcode commp enabledexecp mask). Keep this in sync with
; opalist.
(cond
((endp opalist)
(mv (er hard 'opalistinfo
"Function not found: ~x0"
fn)
nil nil nil))
((eq fn (caar opalist))
(let ((info (cdar opalist)))
(mv (car info)
(cadr info)
(caddr info)
(cdddr info))))
(t (opalistinfo fn (cdr opalist)))))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;;; III. HASH OPERATIONS ;;;;;;;;;;;;;;;;;;;;;;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(defmacro ifopcode () 3)
(defmacro hashsize ()
; Do not quote the body of this definition. We want it computed at
; definition/compile time!
; At one time we used a defconst here, but then we realized that we would
; (apparently, at least, in GCL) have to pay the price both of looking up the
; value of that variable and also unboxing it for fixnum operations. Although
; a little experimentation did not yield meaningful evidence that there is
; really an impact on performance, we proceed with a macro.
; WARNING: Do not increase this size too close to (fixnumbound). See the
; warning in ophashindexevg.
(1 (expt 2 15)))
; We have two hash arrays, 'ifht for assigning uniqueids to csts, and 'opht
; for memoizing the merge operators. In each case the array assigns "buckets"
; to indices.
; Buckets in an ifht are lists of nonleaf csts.
; Buckets in an opht are lists of entries of the form (cst op . args), where
; args is a list of csts. The length of the list is the arity of op.
; Exception: op can be quote, in which case args is a list containing a single
; evg.
(defmacro ifhashindex (x y z)
; Note that (+ 131 2 1) does not exceed 153. See the comment about mxidbound
; in ophashindex1. There is probably nothing sacred about the choices of
; these three numbers 131, 2, and 1, although it seems good that they are
; relatively prime.
`(logandf (+f (*f 131 (uniqueid ,x))
(*f 2 (uniqueid ,y))
(uniqueid ,z))
(hashsize)))
(defmacro *f (&rest args)
(xxxjoinfixnum '* args 1))
(defun ophashindex1 (args i acc)
; There should be no more than 16 args before we "turn around", so that the
; multiplier on uniqueids is no more than (1+ (+ 2 3 ... 17)) = 153. (The
; `1+' is because in ophashindex we add in the opcode as well. Opcodes are
; also bounded by mxidbound  see opalist  as are of course uniqueids.)
; See the comment in mxidbound.
; If we want to increase the (mxidbound), we believe that we could start the
; "turnaround" here earlier. But we have not yet checked this claim carefully.
(declare (type (signedbyte 29) i acc)
(xargs :measure (acl2count args)))
(thefixnum
(cond
((endp args) (if (< acc 0) ( acc) acc))
((or (= (thefixnum i) 18)
(= (thefixnum i) 1))
(if (> acc 0)
(ophashindex1 args 17 acc)
(ophashindex1 args 2 acc)))
(t (ophashindex1 (cdr args)
(1+f i)
(+f acc
(*f i
(uniqueid (car args)))))))))
(defmacro ophashindex (opcode args)
`(logandf (+f ,opcode
(ophashindex1 ,args 2 1))
(hashsize)))
(defmacro ophashindex2 (opcode arg1 arg2)
; This special case of ophashindex is used for commutative operators in
; chkmemo2.
`(logandf (+f ,opcode
(*f 2 (uniqueid ,arg1))
(*f 3 (uniqueid ,arg2)))
(hashsize)))
(defmacro ophashindexif (arg1 arg2 arg3)
`(logandf (+f (ifopcode)
(*f 2 (uniqueid ,arg1))
(*f 3 (uniqueid ,arg2))
(*f 4 (uniqueid ,arg3)))
(hashsize)))
; Having found the bucket associated with the hashindex, here is how
; we search it.
(defun ifsearchbucket (x y z lst)
; Here lst is a list of nonleaf csts.
(cond ((null lst) nil)
((and (cst= x (tst (car lst)))
(cst= y (tbr (car lst)))
(cst= z (fbr (car lst))))
(car lst))
(t (ifsearchbucket x y z (cdr lst)))))
(defun cst=lst (x y)
(cond
((endp x) t)
(t (and (cst= (car x) (car y))
(cst=lst (cdr x) (cdr y))))))
(defmacro eqop (x y)
; This test must change if we start allowing LAMBDAs as operators.
`(eq ,x ,y))
(defun opsearchbucket (op args lst)
; Here op is a function symbol and lst is a tail of a bucket from an opht.
; Thus, lst is a list of elements of the form (cst op0 . args0), where args0 is
; a list of csts unless op0 is 'quote, which it is not if op0 is op.
(cond ((null lst) nil)
((and (eqop op
(cadr (car lst)))
(cst=lst args (cddr (car lst))))
(car (car lst)))
(t (opsearchbucket op args (cdr lst)))))
(defun opsearchbucket2 (op arg1 arg2 lst)
; This is a version of opsearchbucket for binary functions. This is merely
; an optimization we use for commutative operators, since we know that they are
; binary. We could of course use this for all binary operators, but the point
; here is that for commutative operators we delay consing up the commuted
; argument list until it is necessary. See combineopcstscomm.
(cond ((null lst) nil)
((and (eqop op
(cadr (car lst)))
(let ((args (cddr (car lst))))
(and (cst= arg1 (car args))
(cst= arg2 (cadr args)))))
(car (car lst)))
(t (opsearchbucket2 op arg1 arg2 (cdr lst)))))
(defun opsearchbucketif (arg1 arg2 arg3 lst)
; This is a version of opsearchbucket that does not require us to cons up the
; arguments into a list, used in chkmemoif. This is merely an optimization
; we use since IF is such a common operation.
(cond ((null lst) nil)
((and (eqop 'if
(cadr (car lst)))
(let ((args (cddr (car lst))))
(and (cst= arg1 (car args))
(cst= arg2 (cadr args))
(cst= arg3 (caddr args)))))
(car (car lst)))
(t (opsearchbucketif arg1 arg2 arg3 (cdr lst)))))
(defun chkmemo (opcode op args opht)
; If <op,arg1,arg2,...> has an entry in opht, return 0 and the entry.
; Otherwise, return the hash index for <opcode,arg1,arg2,...> (simply to avoid
; its recomputation) and NIL. Entries are of the form (result op . args). We
; return the hash index as the first value so that we can avoid boxing up a
; fixnum for it in GCL.
(declare (type (signedbyte 29) opcode))
(themv
2
(signedbyte 29)
(let ((n (ophashindex opcode args)))
(declare (type (signedbyte 29) n))
(let ((ans (opsearchbucket op args (aref1 'opht opht n))))
(cond (ans (mvf 0 ans))
(t (mvf n nil)))))))
(defun chkmemo2 (opcode op arg1 arg2 opht)
; This is merely an optimization of chkmemo for the case where the operator is
; binary, in particularly for commutative operators; see the comment in
; opsearchbucket2.
(declare (type (signedbyte 29) opcode))
(themv
2
(signedbyte 29)
(let ((n (ophashindex2 opcode arg1 arg2)))
(declare (type (signedbyte 29) n))
(let ((ans (opsearchbucket2 op arg1 arg2 (aref1 'opht opht n))))
(cond (ans (mvf 0 ans))
(t (mvf n nil)))))))
(defun chkmemoif (arg1 arg2 arg3 opht)
; This is merely an optimization of chkmemo for the case where the operator is
; if, which is likely very common. Note that by treating this special case as
; we do, we avoid consing up the list of arguments in some cases; see
; combineifcsts.
(themv
2
(signedbyte 29)
(let ((n (ophashindexif arg1 arg2 arg3)))
(declare (type (signedbyte 29) n))
(let ((ans (opsearchbucketif arg1 arg2 arg3 (aref1 'opht opht n))))
(cond (ans (mvf 0 ans))
(t (mvf n nil)))))))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;;; IV. HASH OPERATIONS: QUOTEPS ;;;;;;;;;;;;;;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(defmacro halfhashsize ()
(floor (hashsize) 2))
(defmacro fourthhashsize ()
(floor (hashsize) 4))
(defun ophashindexstring (index acc string)
(declare (type (signedbyte 29) index acc))
(thefixnum
(cond
((= index 0) acc)
(t (let ((index (1 (thefixnum index))))
(declare (type (signedbyte 29) index))
(ophashindexstring
index
(logandf (hashsize)
(+f acc (charcode (char string index))))
string))))))
(defun ophashindexevg (evg)
(thefixnum
(cond
((integerp evg)
(logandf (hashsize) evg))
((rationalp evg)
(logandf (hashsize)
(+ (numerator evg)
(* 17 (denominator evg)))))
((acl2numberp evg)
(logandf (hashsize)
(+f (ophashindexevg (realpart evg))
(ophashindexevg (imagpart evg)))))
((characterp evg)
(+f (fourthhashsize)
(charcode evg)))
((symbolp evg)
(logandf (hashsize)
; WARNING: Here we assume that (* 19 (hashsize)) is a fixnum. We know it is
; because the hash index is at most (hashsize), which is well under
; (fixnumbound).
(*f 19 (ophashindexevg (symbolname evg)))))
((stringp evg)
(thefixnum
(ophashindexstring (thefixnum! (length evg) 'bdd)
(halfhashsize) evg)))
(t ;cons
(logandf (hashsize)
(+f (ophashindexevg (car evg))
(*f 2 (ophashindexevg (cdr evg)))))))))
(defun opsearchbucketquote (evg bucket)
(cond ((null bucket) nil)
((and (eqop 'quote
(cadr (car bucket)))
(equal evg (caddr (car bucket))))
(car (car bucket)))
(t (opsearchbucketquote evg (cdr bucket)))))
(defun chkmemoquotep (term opht)
(themv
2
(signedbyte 29)
(let ((n (ophashindexevg (cadr term))))
(declare (type (signedbyte 29) n))
(let ((ans (opsearchbucketquote
(cadr term)
(aref1 'opht opht n))))
; One might think that the calls of thefixnum just below are not necessary,
; but in fact they do appear to produce better compiled code in GCL.
(cond (ans (mvf 0 ans))
(t (mvf n nil)))))))
(defun bddquotep (term opht mxid)
(declare (type (signedbyte 29) mxid))
(themv
3
(signedbyte 29)
(cond
((equal term *t*)
(mvf mxid *cstt* opht))
((equal term *nil*)
(mvf mxid *cstnil* opht))
(t
(mvlet (hashindex ans)
(chkmemoquotep term opht)
(declare (type (signedbyte 29) hashindex))
(cond
(ans (mvf mxid ans opht))
(t (let ((newmxid (1+mxid mxid)))
(declare (type (signedbyte 29) newmxid))
(let ((newcst (makeleafcst
newmxid
term
nil)))
(mvf newmxid
newcst
(aset1 'opht opht hashindex
(cons
; The following is the same as (list newcst 'quote (cadr term)), but saves a
; cons.
(cons newcst term)
(aref1 'opht opht hashindex)))))))))))))
(defmacro bddquotep+ (term opht ifht mxid ttree)
`(mvlet (mxid cst opht)
(bddquotep ,term ,opht ,mxid)
(declare (type (signedbyte 29) mxid))
(mvf mxid cst opht ,ifht ,ttree)))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;;; V. BDD RULES AND ONEWAY UNIFIER ;;;;;;;;;;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; We could just use the rewriterule data structures already existing in the
; ACL2 world. However, we suspect that it is a good idea, in order to support
; computationally intensive bdd computations, to avoid having to look at the
; enabled structure or dig deep into a rewrite rule in order to find the
; various fields we need. In fact, we want to have the lhs available as
; quickly as possible, since that field is used the most.
(defrec bddrule
(lhs rhs . rune)
t)
(defun rewriteruletobddrule (lemma)
(make bddrule
:lhs (access rewriterule lemma :lhs)
:rhs (access rewriterule lemma :rhs)
:rune (access rewriterule lemma :rune)))
(defun bddrulesalist1
(recp lemmas ens allfns nondefrules defrules newfns)
; This function returns lists of definitional and nondefinitional bddrules
; corresponding to the lemmas of a given function symbol. The arguments are as
; follows.
; recp: True when the toplevel function symbol for the lemmas is recursive
; lemmas: The rewriterule structures that we want to convert to bddrules
; ens: The current enabled structure
; allfns: List of all function symbols already encountered in bdd rules built
; nondefrules: Bddrules accumulated so far not from definition rules
; defrules: Bddrules accumulated so far from definition rules
; newfns: List of function symbols to be added to allfns (an accumulator)
; At this point, we do not support backchaining: that is, we assume that each
; rule has :hyps field of NIL. We also do not allow free variables in the
; :rhs, and we require :lhs to be a function symbol call. We also require a
; null loopstopper (:heuristicinfo for subclass 'backchain), rather than
; attempting to control looping during the bdd computation. Perhaps some of
; these restrictions can be removed after some thought and additional
; implementation work.
; We require that the :rhs only contain function symbols that are known in the
; opalist. In order to enforce this requirement, we simply pass back two
; values: a list of new function symbols to consider (i.e., ones not in
; allfns that occur in :rhs fields) and the list of bddrules.
; As noted in a comment in bddrulesalist, the lists of lemmas returned by
; this function need to be reversed, because they have the oldest rules at the
; front. That could easily be changed, though the natural way to do this would
; presumably render this function nontail recursive. At this point the issue
; seems sufficiently minor that we are satisfied to leave things this way.
(cond
((endp lemmas) (mv newfns nondefrules defrules))
(t (let ((subclass (access rewriterule (car lemmas) :subclass)))
(cond
((and (eq (access rewriterule (car lemmas) :equiv) 'equal)
(enablednumep (access rewriterule (car lemmas) :nume) ens)
(case subclass
(definition
(and (null recp)
(null (access rewriterule (car lemmas) :hyps))
(subsetpeq
(allvars (access rewriterule (car lemmas)
:rhs))
(allvars (access rewriterule (car lemmas)
:lhs)))))
(abbreviation
(subsetpeq
(allvars (access rewriterule (car lemmas) :rhs))
(allvars (access rewriterule (car lemmas) :lhs))))
(backchain
(and (null (access rewriterule (car lemmas)
:hyps))
(null (access rewriterule (car lemmas)
:heuristicinfo))
(subsetpeq
(allvars (access rewriterule (car lemmas)
:rhs))
(allvars (access rewriterule (car lemmas)
:lhs)))))
(otherwise nil)))
(bddrulesalist1 recp (cdr lemmas) ens allfns
(if (eq subclass 'definition)
nondefrules
(cons (rewriteruletobddrule (car lemmas)) nondefrules))
(if (eq subclass 'definition)
(cons (rewriteruletobddrule (car lemmas)) defrules)
defrules)
(unioneq (setdifferenceeq
(allfnnames (access rewriterule (car lemmas) :rhs))
allfns)
newfns)))
(t (bddrulesalist1 recp (cdr lemmas) ens allfns
nondefrules defrules newfns)))))))
(defun extrarulesforbdds (fn wrld)
; We include certain trivial rewrite rules regardless of whether there are
; explicit rewrite rules that corrrespond to them.
(cond
((eq fn 'equal)
(list (make rewriterule
:nume nil :hyps nil :equiv 'equal
; Rockwell Addition: I have totally stripped out all vestiges of the
; aborted attempt to implement :OUTSIDEIN rewrite rules. I won't comment
; on subsequent differences of this sort.
:subclass 'backchain
:heuristicinfo nil
:backchainlimitlst *initialdefaultbackchainlimit*
:rune *fakeruneforanonymousenabledrule*
:lhs (fconsterm* 'equal *nil* 'x)
:freevarsplhs t
:rhs (fconsterm* 'if 'x *nil* *t*))
(make rewriterule
:nume nil :hyps nil :equiv 'equal
:subclass 'backchain
:heuristicinfo nil
:backchainlimitlst *initialdefaultbackchainlimit*
:rune *fakeruneforanonymousenabledrule*
:lhs (fconsterm* 'equal 'x *nil*)
:freevarsplhs t
:rhs (fconsterm* 'if 'x *nil* *t*))))
((equivalencerelationp fn wrld)
; We do not need to include reflexivity when fn is 'equal, because it is
; hardwired into the definition of combineopcsts.
(list (make rewriterule
:nume nil :hyps nil :equiv 'equal
:subclass 'abbreviation
:heuristicinfo nil
:backchainlimitlst *initialdefaultbackchainlimit*
:rune (equivalencerune fn wrld)
:lhs (fconsterm* fn 'x 'x)
:freevarsplhs t
:rhs *t*)))
((eq fn 'mvnth)
(list (make rewriterule
:nume nil :hyps nil :equiv 'equal
:subclass 'backchain
:heuristicinfo nil
:backchainlimitlst *initialdefaultbackchainlimit*
:rune (fnrunenume 'mvnth nil nil wrld)
:lhs (fconsterm* 'mvnth 'n (fconsterm* 'cons 'x 'y))
:freevarsplhs t
; (if (zp n) x (mvnth ( n 1) y))
:rhs (fconsterm* 'if
(fconsterm* 'zp 'n)
'x
(fconsterm* 'mvnth
(fconsterm* 'binary+
'n
(kwote 1))
'y)))))
(t nil)))
(defun bddrulesalist (fns allfns bddrulesalist ens wrld)
; Call this with a list fns of function symbols that does not include 'if, and
; allfns the result of adding 'if to that list. The parameter bddrulesalist
; is the accumulator, initially nil.
; WARNING: Be sure to modify this function to account for hypotheses if we
; implement conditional rewriting with BDDs.
; Invariant: fns is a subset of allfns. This is important for not just
; termination, but in fact to guarantee that the same function (car fns) is
; never processed twice by bddrulesalist1.
; NOTE: Do we store entries when there are no rules, or not? Not. Suppose
; there are p elements of fns with a nonnil set of rules and q elements of fns
; with a nil set of rules. Then the average number of CDRs required for lookup
; (assuming each function symbol is looked up the same number of times) is
; roughly (p+q)/2 if we store entries for nil sets of rules; and if we don't,
; it's: [1/(p+q)]*(p*p/2 + q*p), which equals [p/2(p+q)]*(p + 2q).
; Now we can see that we're better off the second way, not storing nil entries:
; p+q >= [p/(p+q)]*(p + 2q) ?
; (p+q)^2 >= p^2 + 2pq ?
; q^2 >= 0 !
; Yes, in fact the inequality is strict if q > 0.
(cond
((endp fns) (mv allfns bddrulesalist))
(t (mvlet (newfns nondefrules defrules)
(bddrulesalist1
(recursivep (car fns) wrld)
(append (getprop
(car fns) 'lemmas nil 'currentacl2world wrld)
(extrarulesforbdds (car fns) wrld))
ens
(cons (car fns) allfns)
nil
nil
nil)
(cond ((or defrules nondefrules)
(bddrulesalist
(append newfns (cdr fns))
(append newfns allfns)
(cons (cons (car fns)
; The calls of reverse below ensure that rules will be tried in the appropriate
; order, i.e., most recent ones first. See the comment in bddrulesalist1.
(cons (reverse nondefrules)
(reverse defrules)))
bddrulesalist)
ens
wrld))
; Otherwise do not store an entry for (car fns) in bddrulesalist, as argued
; in the comment above.
(t (bddrulesalist (cdr fns) allfns bddrulesalist ens
wrld)))))))
; We now adapt ACL2's onewayunifier for terms to the realms of csts.
(defmacro onewayunify1cst2 (mxid p1 p2 cst1 cst2 alist opht)
`(mvlet (mxid ans alist1 opht)
(onewayunify1cst ,mxid ,p1 ,cst1 ,alist ,opht)
(declare (type (signedbyte 29) mxid))
(cond
(ans
(mvlet (mxid ans alist2 opht)
(onewayunify1cst mxid ,p2 ,cst2 alist1 opht)
(declare (type (signedbyte 29) mxid))
(cond
(ans (mvf mxid t alist2 opht))
(t (mvf mxid nil ,alist opht)))))
(t (mvf mxid nil ,alist opht)))))
(defmacro onewayunify1cst3 (mxid p1 p2 p3 cst1 cst2 cst3 alist opht)
`(mvlet (mxid ans alist2 opht)
(onewayunify1cst2 ,mxid ,p1 ,p2 ,cst1 ,cst2 ,alist ,opht)
(declare (type (signedbyte 29) mxid))
(cond
(ans
(mvlet (mxid ans alist3 opht)
(onewayunify1cst mxid ,p3 ,cst3 alist2 opht)
(declare (type (signedbyte 29) mxid))
(cond
(ans (mvf mxid t alist3 opht))
(t (mvf mxid nil ,alist opht)))))
(t (mvf mxid nil ,alist opht)))))
(mutualrecursion
; The following functions are adapted from onewayunify1 and the like.
(defun onewayunify1cst (mxid pat cst alist opht)
(declare (type (signedbyte 29) mxid))
(themv
4
(signedbyte 29)
(cond ((variablep pat)
(let ((pair (assoceq pat alist)))
(cond (pair (cond ((cst= (cdr pair) cst)
(mvf mxid t alist opht))
(t (mvf mxid nil alist opht))))
(t (mvf mxid t (cons (cons pat cst) alist) opht)))))
((not (leafp cst))
(cond
((fquotep pat)
(mvf mxid nil alist opht))
((eq (ffnsymb pat) 'if)
(onewayunify1cst3 mxid
(fargn pat 1) (fargn pat 2) (fargn pat 3)
(tst cst) (tbr cst) (fbr cst)
alist opht))
(t
(mvf mxid nil alist opht))))
(t (let ((term (trm cst)))
(cond
((fquotep pat)
(cond ((equal pat term) (mvf mxid t alist opht))
(t (mvf mxid nil alist opht))))
((variablep term) (mvf mxid nil alist opht))
((fquotep term) ;term is not a term, but fquotep is ok here
(cond ((acl2numberp (cadr term))
(let ((ffnsymb (ffnsymb pat)))
(case ffnsymb
(binary+
(cond ((quotep (fargn pat 1))
(mvlet (mxid cst opht)
(bddquotep
(kwote ( (cadr term)
(fix (cadr (fargn pat
1)))))
opht mxid)
(declare (type (signedbyte 29)
mxid))
(onewayunify1cst
mxid (fargn pat 2)
cst alist opht)))
((quotep (fargn pat 2))
(mvlet (mxid cst opht)
(bddquotep
(kwote ( (cadr term)
(fix (cadr (fargn pat
2)))))
opht mxid)
(declare (type (signedbyte 29)
mxid))
(onewayunify1cst
mxid (fargn pat 1)
cst alist opht)))
(t (mvf mxid nil alist opht))))
(binary*
(cond ((and (quotep (fargn pat 1))
(integerp (cadr (fargn pat 1)))
(> (abs (cadr (fargn pat 1))) 1))
(mvlet (mxid cst opht)
(bddquotep
(kwote (/ (cadr term)
(cadr (fargn pat 1))))
opht mxid)
(declare (type (signedbyte 29)
mxid))
(onewayunify1cst
mxid (fargn pat 2)
cst alist opht)))
((and (quotep (fargn pat 2))
(integerp (cadr (fargn pat 2)))
(> (abs (cadr (fargn pat 2))) 1))
(mvlet (mxid cst opht)
(bddquotep
(kwote (/ (cadr term)
(cadr (fargn pat 2))))
opht mxid)
(declare (type (signedbyte 29)
mxid))
(onewayunify1cst
mxid (fargn pat 1)
cst alist opht)))
(t (mvf mxid nil alist opht))))
(unary (cond ((>= (+ (realpart (cadr term))
(imagpart (cadr term)))
0)
(mvf mxid nil alist opht))
(t (mvlet (mxid cst opht)
(bddquotep
(kwote ( (cadr term)))
opht mxid)
(declare (type
(signedbyte
27)
mxid))
(onewayunify1cst
mxid (fargn pat 1)
cst alist
opht)))))
(unary/ (cond ((or (>= (* (cadr term)
(conjugate (cadr term)))
1)
(eql 0 (cadr term)))
(mvf mxid nil alist opht))
(t (mvlet (mxid cst opht)
(bddquotep
(kwote (/ (cadr term)))
opht mxid)
(declare (type
(signedbyte
27)
mxid))
(onewayunify1cst
mxid (fargn pat 1)
cst alist opht)))))
(otherwise (mvf mxid nil alist opht)))))
; We try to avoid some complications by avoiding interninpackageofsymbol
; and coerce for now. We are not aware of any reason why they should present
; undue difficulties, however.
((consp (cadr term))
(cond ((eq (ffnsymb pat) 'cons)
; We have to be careful with alist below so we are a no change loser.
(mvlet
(mxid cst1 opht)
(bddquotep
(kwote (car (cadr term)))
opht mxid)
(declare (type (signedbyte 29) mxid))
(mvlet
(mxid ans alist1 opht)
(onewayunify1cst
mxid (fargn pat 1) cst1 alist opht)
(declare (type (signedbyte 29) mxid))
(cond
(ans
(mvlet
(mxid cst2 opht)
(bddquotep
(kwote (cdr (cadr term)))
opht mxid)
(declare (type (signedbyte 29) mxid))
(mvlet (mxid ans alist2 opht)
(onewayunify1cst
mxid (fargn pat 2) cst2 alist1
opht)
(declare (type (signedbyte 29)
mxid))
(cond (ans (mvf mxid t alist2
opht))
(t (mvf mxid nil alist
opht))))))
(t (mvf mxid nil alist opht))))))
(t (mvf mxid nil alist opht))))
(t (mvf mxid nil alist opht))))
((eq (ffnsymb pat) (ffnsymb term))
; Note: We do not allow lambda expressions at this point. If that changes,
; then we should consider that case too.
(cond ((eq (ffnsymb pat) 'equal)
(onewayunify1cstequal mxid
(fargn pat 1) (fargn pat 2)
(fargn term 1) (fargn term 2)
alist opht))
(t (mvlet (mxid ans alist1 opht)
(onewayunify1cstlst mxid
(fargs pat)
(fargs term)
alist opht)
(declare (type (signedbyte 29) mxid))
(cond (ans (mvf mxid t alist1 opht))
(t (mvf mxid nil alist opht)))))))
(t (mvf mxid nil alist opht))))))))
(defun onewayunify1cstlst (mxid pl cstl alist opht)
; This function is NOT a No Change Loser.
(declare (type (signedbyte 29) mxid))
(themv
4
(signedbyte 29)
(cond ((null pl) (mvf mxid t alist opht))
(t (mvlet (mxid ans alist opht)
(onewayunify1cst mxid (car pl) (car cstl) alist opht)
(declare (type (signedbyte 29) mxid))
(cond
(ans
(onewayunify1cstlst mxid (cdr pl) (cdr cstl) alist
opht))
(t (mvf mxid nil alist opht))))))))
(defun onewayunify1cstequal (mxid pat1 pat2 cst1 cst2 alist opht)
(declare (type (signedbyte 29) mxid))
(themv
4
(signedbyte 29)
(mvlet (mxid ans alist opht)
(onewayunify1cst2 mxid pat1 pat2 cst1 cst2 alist opht)
(declare (type (signedbyte 29) mxid))
(cond
(ans (mvf mxid t alist opht))
(t (onewayunify1cst2 mxid pat2 pat1 cst1 cst2 alist
opht))))))
)
(defun someonewayunifycstlst (cstlst rules opht mxid ttree)
(declare (type (signedbyte 29) mxid))
(themv
6
(signedbyte 29)
(cond
((endp rules)
(mvf mxid nil nil nil opht ttree))
(t (mvlet (mxid ans alist opht)
(onewayunify1cstlst
mxid (fargs (access bddrule (car rules) :lhs))
cstlst nil opht)
(declare (type (signedbyte 29) mxid))
(cond
(ans (mvf mxid t
(access bddrule (car rules) :rhs)
alist opht
(pushlemma (access bddrule (car rules) :rune)
ttree)))
(t (someonewayunifycstlst cstlst (cdr rules)
opht mxid ttree))))))))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;;; VI. SOME INTERFACE UTILITIES
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; We will ignore declaration opportunities in this section, especially for
; declaring mxid to be a fixnum, because efficiency is a minor issue here.
(defun leafcstlist (lst boolvars acc mxid)
; Here lst is a list of variables from the input term. Returns a list of leaf
; csts for those variables, i.e., elements of the form (uniqueid variable
; bool), where if bool is t then variable is known to be Boolean.
(cond
((endp lst) (mv mxid acc))
(t (mvlet (mxid acc)
(cond ((assoceq (car lst) acc)
(mv mxid acc))
(t (let ((newmxid (1+mxid mxid)))
(mv newmxid
(cons (makeleafcst
newmxid
(car lst)
(membereq (car lst) boolvars))
acc)))))
(leafcstlist (cdr lst) boolvars acc mxid)))))
(mutualrecursion
(defun decodecst (cst cstarray)
; This takes a cst and returns a term and an updated cstarray, whose nth entry
; is the decoding of the cst with unique id n.
(let ((term (aref1 'cstarray cstarray (uniqueid cst))))
(cond
(term (mv term cstarray))
((leafp cst)
(cond
((or (variablep (trm cst))
(fquotep (trm cst)))
(mv (trm cst) cstarray))
(t (mvlet (args cstarray)
(decodecstlst (fargs (trm cst)) cstarray)
(let ((x (consterm (ffnsymb (trm cst))
args)))
(mv x
(aset1 'cstarray
cstarray
(uniqueid cst)
x)))))))
(t (mvlet
(tst cstarray)
(decodecst (tst cst) cstarray)
(mvlet
(tbr cstarray)
(decodecst (tbr cst) cstarray)
(mvlet
(fbr cstarray)
(decodecst (fbr cst) cstarray)
(let ((x (mconsterm* 'if tst tbr fbr)))
(mv x
(aset1 'cstarray
cstarray
(uniqueid cst)
x))))))))))
(defun decodecstlst (cstlst cstarray)
(cond
((endp cstlst)
(mv nil cstarray))
(t (mvlet (first cstarray)
(decodecst (car cstlst) cstarray)
(mvlet (rest cstarray)
(decodecstlst (cdr cstlst) cstarray)
(mv (cons first rest)
cstarray))))))
)
(defun decodecstalist1 (alist cstarray)
(cond
((endp alist) (mv nil cstarray))
(t (mvlet (term cstarray)
(decodecst (cdar alist) cstarray)
(mvlet (rest cstarray)
(decodecstalist1 (cdr alist) cstarray)
(mv (cons (list (caar alist)
term)
rest)
cstarray))))))
(defun decodecstalist (cstalist cstarray)
(mvlet (alist cstarray)
(decodecstalist1 cstalist cstarray)
(declare (ignore cstarray))
alist))
(defun leafcstlistarray (mxid)
(let ((dim (1+ mxid)))
(compress1 'cstarray
`((:header :dimensions (,dim)
:maximumlength ,(+ 10 dim)
:default nil)))))
(defconst *somenonnilvalue* "Some nonnil value")
(defun falsifyingassignment1 (cst acc cstarray)
; Returns a list of doublets (var bool) that provide an environment for
; falsifying the given cst. Also returns a new cstarray; we have to do that
; so that we always pass in the "current" cstarray, in order to avoid slow
; array access.
(cond
((cstnilp cst)
(mv acc cstarray))
((quotep (trm cst))
(mv (er hard 'falsifyingassignment1
"Tried to falsify ~x0!"
(trm cst))
cstarray))
((leafp cst)
(mvlet (term cstarray)
(decodecst cst cstarray)
(mv (cons (list term nil) acc)
cstarray)))
((cstnonnilp (tbr cst))
(mvlet (term cstarray)
(decodecst (tst cst) cstarray)
(falsifyingassignment1 (fbr cst)
(cons (list term nil)
acc)
cstarray)))
(t
(mvlet (term cstarray)
(decodecst (tst cst) cstarray)
(falsifyingassignment1 (tbr cst)
(cons (list term (if (cstboolp (tst cst))
t
*somenonnilvalue*))
acc)
cstarray)))))
(defun falsifyingassignment (cst mxid)
(mvlet (asst cstarray)
(falsifyingassignment1 cst nil (leafcstlistarray mxid))
(declare (ignore cstarray))
(reverse asst)))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;;; VII. MAIN ALGORITHM ;;;;;;;;;;;;;;;;;;;;;;;;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(defun makeif (mxid n op args x y z opht ifht bddconstructors)
; This function returns either
; (mvf mxid cst opht ifht)
; or (culling this from an "erroneous" return of makeifcst below)
; (mvf mxid fmtstring fmtalist badcst)
; Intuitively, this function makes a cst representing (IF x y z). But
; we know that this is the answer to the merge op(args) and we
; know that n is the hash index of <op,arg1,...>. We know
; <op,arg1,...> is not in the opht. We first look in the ifht to
; see if (IF x y z) is there. If so, we return it. If not, we build
; an appropriate one, assigning the next unique id, which is (1+
; mxid), and add it to the ifht. In any case, before returning, we
; store the returned cst as the answer for op(arg1,...) in opht. We
; thus have to return four results: the new mxid, the cst, and the
; two hash arrays.
(declare (type (signedbyte 29) n mxid))
(themv
4
(signedbyte 29)
(cond ((cst= y z) (mvf mxid
y
; The following aset1 was added after Moore's first presentation of this
; work. Its absence was discovered during a codewalk with Jim
; Bitner. The times improved slightly on most examples, except mul08
; where we lost a few more seconds. The times shown in
; ~moore/text/pchacking.mss  the most recent version of a talk on
; this work  have been updated to show the performance of this
; version of the code.
(aset1 'opht opht n
(cons (list* y op args)
(aref1 'opht opht n)))
ifht))
(t (let ((m (ifhashindex x y z)))
(declare (type (signedbyte 29) m))
(let* ((bucket (aref1 'ifht ifht m))
(oldif (ifsearchbucket x y z bucket)))
(cond (oldif (mvf mxid
oldif
(aset1 'opht opht n
(cons (list* oldif op args)
(aref1 'opht opht n)))
ifht))
((and (csttp y)
(cstnilp z)
(cstboolp x))
(mvf mxid
x
(aset1 'opht opht n
(cons (list* x op args)
(aref1 'opht opht n)))
ifht))
(t (let ((mxid (1+mxid mxid)))
(declare (type (signedbyte 29) mxid))
(mvlet
(erp newif)
(makeifcst mxid x y z bddconstructors)
(cond
(erp (mvf mxid
(car erp) ;fmtstring
(cdr erp) ;fmtalist
newif ;bad cst
))
(t
(mvf mxid
newif
(aset1 'opht opht n
(cons (list* newif op args)
(aref1 'opht opht n)))
(aset1 'ifht ifht m
(cons newif bucket)))))))))))))))
(defun makeifnomemo (mxid x y z opht ifht bddconstructors)
; Same as makeif, except that we do not change opht, and we assume that y and
; z are already known to be distinct.
(declare (type (signedbyte 29) mxid))
(themv
4
(signedbyte 29)
(let ((m (ifhashindex x y z)))
(declare (type (signedbyte 29) m))
(let* ((bucket (aref1 'ifht ifht m))
(oldif (ifsearchbucket x y z bucket)))
(cond (oldif (mvf mxid oldif opht ifht))
((and (csttp y)
(cstnilp z)
(cstboolp x))
(mvf mxid x opht ifht))
(t (let ((mxid (1+mxid mxid)))
(declare (type (signedbyte 29) mxid))
(mvlet
(erp newif)
(makeifcst mxid x y z bddconstructors)
(cond
(erp (mvf mxid
(car erp) ;fmtstring
(cdr erp) ;fmtalist
newif ;bad cst
))
(t
(mvf mxid newif opht
(aset1 'ifht ifht m
(cons newif bucket)))))))))))))
(defmacro splitvar (cst)
; The variable to split on from cst. If cst is a leaf, then we only split on
; it if it is a cstvarp (i.e., not the representation of T or NIL) and is
; known to be Boolean.
`(if (leafp ,cst)
(if (and (cstvarp ,cst)
(cstboolp ,cst))
,cst
nil)
(tst ,cst)))
(defun minvar (acc args)
; Args is a list of csts. We return nil if there is no variable to split on.
; Otherwise, we return the leaf cst with the smallest uniqueid. Call this
; with acc = nil.
(declare (xargs :measure (acl2count args)))
(if (endp args)
acc
(let ((var (splitvar (car args))))
(if (null var)
(minvar acc (cdr args))
(minvar (cond
((null acc)
var)
((< (uniqueid var) (uniqueid acc))
var)
(t acc))
(cdr args))))))
(defun combineopcsts1 (varid args)
; Args is a list of csts, and varid is the uniqueid of a term that is not
; necessarily Booleanvalued. We return (mv truebranchargs
; falsebranchargs), where under the assumption that varid is the unique id
; of a term that is not (semantically) nil, args represents the same list of
; terms as truebranchargs; and under the assumption that varid is the unique
; id of a term that (semantically) equals nil, args represents the same list of
; terms as falsebranchargs.
(declare (type (signedbyte 29) varid))
(if (endp args)
(mv nil nil)
(mvlet (x y)
(combineopcsts1 varid (cdr args))
(cond
((leafp (car args))
(if (and (= (thefixnum varid) (uniqueid (car args)))
; Even though we are splitting on varid, we need to know that it is the unique
; id of a boolean variable in order to simplify as shown below. Note that
; varid need only be the uniqueid of a Boolean cst when splitvar returns it
; by virtue of its being a leaf; it could be nonBoolean if splitvar
; encounters it as a test.
(cstboolp (car args)))
(mv (cons *cstt* x) (cons *cstnil* y))
(mv (cons (car args) x) (cons (car args) y))))
(t
(if (= (thefixnum varid) (uniqueid (tst (car args))))
(mv (cons (tbr (car args)) x) (cons (fbr (car args)) y))
(mv (cons (car args) x) (cons (car args) y))))))))
(defun boolflg (args mask)
; Checks that for each "bit" set in mask, the corresponding arg in args is
; known to be Boolean. In the case that mask is (typically) from a type
; prescription, this allows us to conclude, assuming that the given function
; symbol's base type is Boolean, then the application of that function to args
; is Boolean.
; If this function returns a nonnil value, then that value is a type
; prescription rune.
(cond
((endp args)
; Then mask is a type prescription rune.
mask)
((car mask)
(and (cstboolp (car args))
(boolflg (cdr args) (cdr mask))))
(t (boolflg (cdr args) (cdr mask)))))
(defun somebddconstructorp (args bddconstructors)
(cond
((endp args) nil)
(t (or (and (leafp (car args))
(bddconstructortrmp (trm (car args)) bddconstructors))
(somebddconstructorp (cdr args) bddconstructors)))))
(defun combineopcstssimple
(hashindex op mask args opht ifht mxid bddconstructors ttree)
; Make a new leafcst for (op . args). Note: this function returns an "error"
; in the sense described in the bdd nest if the call attempts to build a
; nonbddconstructor node when some argument is a bddconstructor. Pass in
; bddconstructors = nil if no such attempt is possible; otherwise, we know
; that op is not a member of bddconstructors.
(declare (type (signedbyte 29) hashindex mxid))
(themv
5
(signedbyte 29)
(let ((newmxid (1+mxid mxid))
(rune (and mask
; If mask is nonnil, we guarantee that op corresponds to a function whose type
; is Boolean modulo that mask (for its type prescription).
(boolflg args mask))))
(declare (type (signedbyte 29) newmxid))
(let ((newcst (makeleafcst
newmxid
(cons op args)
rune)))
(cond
((and bddconstructors
; We presumably know that (not (membereq op bddconstructors)).
(somebddconstructorp args bddconstructors))
(bdderror
newmxid
"Attempted to create ~x0 node during BDD processing with an argument ~
that is a call of ~#1~[a bddconstructor~/CONS~], which would ~
produce a nonBDD term (as defined in :DOC bddalgorithm). See ~
:DOC showbdd."
(list (cons #\0 op)
(cons #\1 (if (equal bddconstructors '(cons))
1
0)))
newcst
ttree))
(t
(mvf newmxid
newcst
(aset1 'opht opht hashindex
(cons (list* newcst op args)
(aref1 'opht opht hashindex)))
ifht
(if rune (pushlemma rune ttree) ttree))))))))
(defmacro mvlet? (vars form body)
; The idea here is that we want to allow functions in the bdd nest to return
; multiple values of the sort returned by the macro bdderror.
; Combineifcsts+ gets special treatment.
; This macro should only be used when the first var has a fixnum value. We go
; even further by requiring that the first var be mxid. Whenever we write
; (mvlet? vars form body)
; we assume that body returns the same number of values as does form.
; Keep this in sync with bdderror, as indicated in a comment below. The code
; below is the only place, as of this writing, where we update the
; bddcallstack.
(declare (xargs :guard
(and (truelistp vars)
(eq (car vars) 'mxid)
(< 2 (length vars))
(consp form)
(truelistp form)
(membereq
(car form)
'(combineifcsts+
combineopcsts combineopcsts+
combineopcstsguts combineopcstscomm
bdd bddalist bddlist)))))
`(mvlet ,vars
,form
(declare (type (signedbyte 29) mxid))
(if (stringp ,(cadr vars))
,(cond
((eq (car form) 'bdd)
; Vars is of the form returned by bdderror:
; (mv mxid fmtstring (cons fmtalist badcst) callstack ttree).
; We want to push the current term onto the callstack.
(list 'mvf
(car vars)
(cadr vars)
(caddr vars)
(list 'cons
; Keep this in sync with the definition of bdd. Here, (cadr form) is really
; the first argument of bdd, which should be a term, and (caddr form) is the
; second argument, which should be an alist. The cons we generate here is the
; new value of the callstack.
(list 'cons (cadr form) (caddr form))
(cadddr vars))
(cadddr (cdr vars))))
(t
; Then vars represents an "error", and we want to return an error of the same
; sort. This sort will be different for combineifcsts+ than for the other
; allowable functions (from the guard expresssion above), but no matter.
(cons 'mvf vars)))
,body)))
(defmacro combineifcsts+ (cst1 cst2 cst3 opht ifht mxid bddconstructors)
`(cond
((cstnilp ,cst1)
(mvf ,mxid ,cst3 ,opht ,ifht))
((cstnonnilp ,cst1)
(mvf ,mxid ,cst2 ,opht ,ifht))
(t (combineifcsts ,cst1 ,cst2 ,cst3 ,opht ,ifht ,mxid
,bddconstructors))))
(defun combineifcsts1 (varid args)
; This function is identical to combineopcsts1, except that the op is
; assumed to be IF.
(declare (type (signedbyte 29) varid))
(mvlet (x y)
(combineopcsts1 varid (cdr args))
(cond
((leafp (car args))
(if (= (thefixnum varid) (uniqueid (car args)))
(mv (cons *cstt* x)
(cons *cstnil* y))
(mv (cons (car args) x)
(cons (car args) y))))
(t
(if (= (thefixnum varid) (uniqueid (tst (car args))))
(mv (cons (tbr (car args)) x) (cons (fbr (car args)) y))
(mv (cons (car args) x) (cons (car args) y)))))))
(defun combineifcsts
(testcst truecst falsecst opht ifht mxid bddconstructors)
; Similarly to the bdd nest, this function returns either
; (mvf mxid cst opht ifht)
; or
; (mvf mxid fmtstring (cons fmtalist badcst) nil).
; We assume here that testcst is not the cst of a quotep, and that the input
; csts are really all csts (not error strings).
(declare (type (signedbyte 29) mxid))
(themv
4
(signedbyte 29)
(cond
((cst= truecst falsecst)
(mvf mxid truecst opht ifht))
((cst= testcst falsecst)
(combineifcsts testcst truecst *cstnil* opht ifht mxid
bddconstructors))
((and (cst= testcst truecst)
(cstboolp truecst))
(combineifcsts testcst *cstt* falsecst opht ifht mxid
bddconstructors))
((and (cstnilp falsecst)
(if (csttp truecst)
(cstboolp testcst)
(cst= testcst truecst)))
(mvf mxid testcst opht ifht))
(t (let ((truevar (splitvar truecst))
(falsevar (splitvar falsecst)))
(cond
((and (leafp testcst)
(or (null truevar)
(< (uniqueid testcst) (uniqueid truevar)))
(or (null falsevar)
(< (uniqueid testcst) (uniqueid falsevar))))
; Then the test is the appropriate variable to split on for building a bdd, so
; we proceed to build a bdd. Some test data suggests that it is more efficient
; to avoid opht memoization in this case; it makes sense anyhow that ifht
; memoization would suffice here. After all, very little work would be done
; inbetween looking in the opht and looking in the ifht. So, we neither
; consult nor use the opht when the testcst is already in the right position.
(makeifnomemo mxid testcst truecst falsecst opht ifht
bddconstructors))
(t
(mvlet
(hashindex ans)
(chkmemoif testcst truecst falsecst opht)
(declare (type (signedbyte 29) hashindex))
(cond
(ans (mvf mxid ans opht ifht))
(t (let* ((args (list testcst truecst falsecst))
(minvar (minvar nil args)))
; Note that minvar is nonnil; otherwise splitvar returns nil for each arg,
; and the previous case would apply.
(mvlet
(args1 args2)
(combineifcsts1 (uniqueid minvar) args)
(mvlet?
(mxid cst1 opht ifht)
(combineifcsts+ (car args1) (cadr args1) (caddr args1)
opht ifht mxid bddconstructors)
(mvlet?
(mxid cst2 opht ifht)
(combineifcsts+ (car args2) (cadr args2) (caddr args2)
opht ifht mxid bddconstructors)
(makeif mxid hashindex 'if args minvar cst1 cst2
opht ifht bddconstructors)))))))))))))))
(defun cstlisttoevglist (cstlst)
(cond
((endp cstlst) nil)
(t (cons (cadr (trm (car cstlst)))
(cstlisttoevglist (cdr cstlst))))))
(defun cstquotelistp (cstlst)
(cond
((endp cstlst) t)
((and (leafp (car cstlst))
(quotep (trm (car cstlst))))
(cstquotelistp (cdr cstlst)))
(t nil)))
(defrec bddspv
; Bddspv stands for "BDD special variables", in analogy to pspv. We simply
; prefer not to pass around such long argument lists. In addition, we expect
; the code to be easier to modify this way; for example, the addition of
; bddconstructors as a field in the bddspv avoids the need to massive
; modification of function calls.
(opalist bddrulesalist . bddconstructors)
t)
(defun bddevfncall
(mxid hashindex op mask args opht ifht bddconstructors rune ttree state)
(declare (type (signedbyte 29) hashindex mxid))
(themv
5
(signedbyte 29)
(mvlet (erp val latches)
(evfncall op (cstlisttoevglist args) state nil nil)
(declare (ignore latches))
(cond
(erp
; How can this case happen? Evfncall can only "return an error" if there is a
; guard violation (not possible in this context) or a call of a constrained
; function (introduced locally in an encapsulate or introduced by defchoose).
; Although we have guaranteed that op is not constrained (see the code for
; opalist), still the body of op could contain calls of constrained functions.
(combineopcstssimple
hashindex op mask args opht ifht mxid
(and (not (membereq op bddconstructors))
; See the comment in combineopcstssimple. The idea is that if op is in
; bddconstructors, then we may suppress a certain check.
bddconstructors)
ttree))
(t (bddquotep+ (list 'quote val) opht ifht mxid
(pushlemma rune ttree)))))))
(defmacro combineopcsts+ (mxid commp enabledexecp opcode op mask args opht
ifht opbddrules ttree bddspv)
; In combineopcstsguts we want to call either combineopcsts or
; combineopcstscomm, depending on the commp argument. It would be slightly
; more efficient if we simply had two versions of combineopcstsguts: one
; that calls combineopcsts and one that calls combineopcstscomm. But the
; savings seems quite trivial, so we devise this macro to call the appropriate
; function.
`(if ,commp
(combineopcstscomm ,mxid ,commp ,enabledexecp ,opcode ,op ,mask
(car ,args) (cadr ,args) ,args ,opht ,ifht
,opbddrules ,ttree ,bddspv state)
(combineopcsts ,mxid ,enabledexecp ,opcode ,op ,mask
,args ,opht ,ifht ,opbddrules
,ttree ,bddspv state)))
(defun makeifforop
(mxid hashindex op args testcst truecst falsecst
opht ifht bddconstructors)
(declare (type (signedbyte 29) hashindex mxid))
(themv
4
(signedbyte 29)
(cond
((cst= truecst falsecst)
; Keep this case in sync with makeif.
(mvf mxid truecst
(aset1 'opht opht hashindex
(cons (list* truecst op args)
(aref1 'opht opht hashindex)))
ifht))
((let ((truesplitvar (splitvar truecst))
(falsesplitvar (splitvar falsecst))
(testid (uniqueid testcst)))
(declare (type (signedbyte 29) testid))
(and (or (null truesplitvar)
(< testid (uniqueid truesplitvar)))
(or (null falsesplitvar)
(< testid (uniqueid falsesplitvar)))))
(makeif
mxid hashindex op args testcst truecst falsecst
opht ifht bddconstructors))
(t
(mvlet? (mxid cst opht ifht)
(combineifcsts+
testcst truecst falsecst opht ifht mxid bddconstructors)
(mvf mxid
cst
(aset1 'opht opht hashindex
(cons (list* cst op args)
(aref1 'opht opht hashindex)))
ifht))))))
(mutualrecursion
; All functions in this nest return either
; (mvf mxid cst opht ifht ttree)
; or (as returned by bdderror)
; (mvf mxid fmtstring (fmtalist . badcst) callstack ttree)
(defun combineopcsts (mxid enabledexecp opcode op mask args opht
ifht opbddrules ttree bddspv state)
; Returns a cst for (op . args). For special treatment of the case where the
; operator is commutative, in order to avoid some consing, use
; combineopcstscomm.
(declare (type (signedbyte 29) opcode mxid))
(themv
5
(signedbyte 29)
(mvlet
(hashindex ans)
(chkmemo opcode op args opht)
(declare (type (signedbyte 29) hashindex))
(cond
(ans (mvf mxid ans opht ifht ttree))
((and enabledexecp
(cstquotelistp args))
(bddevfncall mxid hashindex op mask args opht ifht
(access bddspv bddspv :bddconstructors)
enabledexecp ttree state))
((and (eq op 'booleanp)
(cstboolp (car args)))
(mvf mxid *cstt* opht ifht
(pushlemma (fnrunenume 'booleanp nil nil (w state)) ttree)))
(t (combineopcstsguts
mxid nil hashindex enabledexecp opcode op mask args opht
ifht opbddrules ttree bddspv state))))))
(defun combineopcstscomm (mxid commp enabledexecp opcode op mask arg1
arg2 args opht ifht opbddrules ttree
bddspv state)
; Returns a cst for (op arg1 arg2) where op is commutative and commp is a rune
; justifying commutativity of op.
; When args is nonnil, it is (list arg1 arg2). The idea is to avoid making a
; cons when possible.
(declare (type (signedbyte 29) opcode mxid))
(themv
5
(signedbyte 29)
(cond
((and (eq op 'equal)
(cst= arg1 arg2))
; Alternatively, we could wait until after the chkmemo2 test below. But in
; that case, we should make the appropriate entry in the opht so that we don't
; waste our time the next time the same call of 'equal arises, looking for an
; entry in opht that has not been (and will never be) put there. But we
; prefer to avoid the opht entirely in this trivial case, and also avoid the
; computations having to do with commutativity.
; Actually, a few experiments suggest that we should have left this branch
; where it was, jut before the next branch involving 'equal. But that makes no
; sense! Since the performance degradation seemed to be at most a couple of
; percent, we'll leave it this way for now.
(mvf mxid *cstt* opht ifht
(pushlemma (fnrunenume 'equal nil nil (w state)) ttree)))
(t
(mvlet
(arg1 arg2 args ttree)
(cond ((and (quotep arg2)
(not (quotep arg1)))
(mv arg2 arg1 nil (pushlemma commp ttree)))
((< (uniqueid arg2)
(uniqueid arg1))
(mv arg2 arg1 nil (pushlemma commp ttree)))
(t (mv arg1 arg2 args ttree)))
(mvlet
(hashindex ans)
(chkmemo2 opcode op arg1 arg2 opht)
(declare (type (signedbyte 29) hashindex))
(cond
(ans (mvf mxid ans opht ifht ttree))
((and (eq op 'equal)
(csttp arg1)
(cstboolp arg2))
; Note: We are tempted to worry about the term (equal 'nil 't), which would
; not get caught by this case and hence, we fret, could fall through to a call
; of bddevfncall (which may be rather slower than we wish). However, since
; the unique id is 1 for T and 2 for NIL, and we have already commuted the args
; if necessary, then there is nothing to worry about.
(mvf mxid arg2 opht ifht
(pushlemma (fnrunenume 'equal nil nil (w state)) ttree)))
((and enabledexecp
(quotep (trm arg1))
(quotep (trm arg2)))
(bddevfncall mxid hashindex op mask (or args (list arg1 arg2)) opht
ifht
(access bddspv bddspv :bddconstructors)
enabledexecp ttree state))
(t (combineopcstsguts
mxid commp hashindex enabledexecp opcode op mask
; It is tempting to avoid consing up the following list, just in case it will
; be torn apart again. However, this list is the one that is ultimately
; memoized, so we need it anyhow.
(or args (list arg1 arg2))
opht ifht opbddrules ttree bddspv state)))))))))
(defun combineopcstsguts
(mxid commp hashindex enabledexecp opcode op mask args opht ifht
opbddrules ttree bddspv state)
; Note that opbddrules is a pair of the form (bddlemmas . bdddefs). These
; are all the bdd rules that rewrite calls of the function symbol op.
(declare (type (signedbyte 29) opcode mxid hashindex))
(themv
5
(signedbyte 29)
(mvlet
(mxid ans rhs alist opht ttree)
(someonewayunifycstlst args (car opbddrules)
opht mxid ttree)
(declare (type (signedbyte 29) mxid))
(cond
(ans
(mvlet?
(mxid cst opht ifht ttree)
(bdd rhs alist opht ifht mxid ttree bddspv state)
; We could consider avoiding the following memoization for the application of
; lemmas. The "be" benchmarks suggest mixed results.
(mvf mxid cst
(aset1 'opht opht hashindex
(cons (list* cst op args)
(aref1 'opht opht hashindex)))
ifht
ttree)))
(t (let ((bddconstructors (access bddspv bddspv :bddconstructors)))
(cond
((membereq op bddconstructors)
; Then build a leaf node. We do not distribute IF through calls of
; bddconstructors.
(combineopcstssimple
hashindex op mask args opht ifht mxid nil ttree))
(t (mvlet
(mxid ans rhs alist opht ttree)
(someonewayunifycstlst args (cdr opbddrules)
opht mxid ttree)
(declare (type (signedbyte 29) mxid))
(cond
(ans
(mvlet?
(mxid cst opht ifht ttree)
(bdd rhs alist opht ifht mxid ttree bddspv state)
; We could consider avoiding the following memoization for the application of
; definitions. The "be" benchmarks suggest mixed results.
(mvf mxid cst
(aset1 'opht opht hashindex
(cons (list* cst op args)
(aref1 'opht opht hashindex)))
ifht ttree)))
(t
(let ((minvar (minvar nil args)))
; There is certainly a potential here for more case splitting than me might
; desire. For, notice that minvar could be nonnil even though all of the
; args are leaves, because splitvar (called by minvar) is happy to return a
; leaf that is known to be Boolean (and not t or nil). However, our current
; model of how OBDDs will be used suggests that we rarely get to this part of
; the code anyhow, because operators not belonging to bddconstructors will
; have been expanded away using rewrite rules or definitions. So, we see no
; need at this point to take pains to avoid case splitting. Instead, we prefer
; to err on the side of "completeness".
(cond
((null minvar)
(combineopcstssimple
hashindex op mask args opht ifht mxid
; At this point we know that op is a not a member of bddconstructors. So we
; must pass in bddconstructors here rather than nil. See the comment in
; combineopcstssimple.
bddconstructors ttree))
(t (mvlet
(args1 args2)
(combineopcsts1 (uniqueid minvar) args)
; Collect args1 for the true branch and args2 for the false branch. For
; example, (foo x0 (if minvar x1 x2) (if minvar x3 x4)) yields
; (mv (list x0 x1 x3) (list x0 x2 x4)). More reifically:
; (combineopcsts1 3 '((4 x0 t)
; (9 (3 y t) t (5 x1 t) . (6 x2 t))
; (10 (3 y t) t (7 x3 t) . (8 x4 t))))
; is equal to
; (mv ((4 X0 T) (5 X1 T) (7 X3 T))
; ((4 X0 T) (6 X2 T) (8 X4 T)))
(mvlet?
(mxid cst1 opht ifht ttree)
(combineopcsts+ mxid commp enabledexecp
opcode op mask args1 opht
ifht opbddrules ttree bddspv)
(mvlet?
(mxid cst2 opht ifht ttree)
(combineopcsts+ mxid commp enabledexecp
opcode op mask args2 opht
ifht opbddrules ttree bddspv)
(mvlet
(mxid ans opht ifht)
(makeifforop
mxid hashindex op args minvar cst1 cst2
opht ifht bddconstructors)
(declare (type (signedbyte 29) mxid))
(cond ((stringp ans)
(bdderror mxid ans opht ifht ttree))
(t
(mvf mxid ans opht ifht
ttree)))))))))))))))))))))
(defun bdd (term alist opht ifht mxid ttree bddspv state)
(declare (xargs :measure (acl2count term)
:guard (pseudotermp term))
(type (signedbyte 29) mxid))
(themv
5
(signedbyte 29)
(cond
((variablep term)
(mvf mxid
(or (cdr (assoceq term alist))
(er hard 'bdd
"Didn't find variable ~x0!"
term))
opht ifht ttree))
((fquotep term)
(cond
((eq (cadr term) t)
(mvf mxid *cstt* opht ifht ttree))
((eq (cadr term) nil)
(mvf mxid *cstnil* opht ifht ttree))
(t (bddquotep+ term opht ifht mxid ttree))))
((or (eq (ffnsymb term) 'if)
(eq (ffnsymb term) 'if*))
(mvlet?
(mxid testcst opht ifht ttree)
(bdd (fargn term 1) alist opht ifht
mxid
; We will need to note the use of if* eventually, so for simplicity we do it
; now.
(if (eq (ffnsymb term) 'if)
ttree
(pushlemma (fnrunenume 'if* nil nil (w state)) ttree))
bddspv state)
; Note that we don't simply call combineifcsts+, because we want to avoid
; applying bdd to one of the branches if the test already decides the issue.
(cond
((cstnilp testcst)
(bdd (fargn term 3) alist opht ifht mxid ttree bddspv state))
((cstnonnilp testcst)
(bdd (fargn term 2) alist opht ifht mxid ttree bddspv state))
((eq (ffnsymb term) 'if*)
(bdderror
mxid
"Unable to resolve test of IF* for term~~%~p0~~%under the ~
bindings~~%~x1~~% use SHOWBDD to see a backtrace."
(list (cons #\0 (untranslate term nil (w state)))
(cons #\1
(decodecstalist alist
(leafcstlistarray mxid))))
; We need a cst next, though we don't care about it.
*cstt*
ttree))
(t
(mvlet?
(mxid truecst opht ifht ttree)
(bdd (fargn term 2) alist opht ifht mxid ttree bddspv state)
(mvlet?
(mxid falsecst opht ifht ttree)
(bdd (fargn term 3) alist opht ifht mxid ttree bddspv state)
(mvlet
(mxid cst opht ifht)
(combineifcsts testcst truecst falsecst opht ifht mxid
(access bddspv bddspv :bddconstructors))
(declare (type (signedbyte 29) mxid))
(cond
((stringp cst)
(bdderror mxid cst opht ifht ttree))
(t
(mvf mxid cst opht ifht ttree))))))))))
((flambdap (ffnsymb term))
(mvlet? (mxid alist opht ifht ttree)
(bddalist (lambdaformals (ffnsymb term))
(fargs term)
alist opht ifht
mxid ttree bddspv state)
(bdd (lambdabody (ffnsymb term))
alist opht ifht mxid ttree bddspv state)))
(t (mvlet
(opcode commp enabledexecp mask)
(opalistinfo (ffnsymb term)
(access bddspv bddspv :opalist))
(declare (type (signedbyte 29) opcode))
(cond
(commp
(mvlet?
(mxid arg1 opht ifht ttree)
(bdd (fargn term 1) alist opht ifht mxid ttree bddspv state)
(mvlet?
(mxid arg2 opht ifht ttree)
(bdd (fargn term 2) alist opht ifht mxid ttree bddspv state)
(combineopcstscomm mxid commp enabledexecp opcode
(ffnsymb term) mask
arg1 arg2 nil opht ifht
(cdr (assoceq (ffnsymb term)
(access bddspv bddspv
:bddrulesalist)))
ttree bddspv state))))
(t
(mvlet? (mxid lst opht ifht ttree)
(bddlist (fargs term) alist opht ifht mxid ttree bddspv
state)
(combineopcsts mxid enabledexecp opcode
(ffnsymb term) mask
; For a first cut I'll keep this simple. Later, we may want to avoid consing
; up lst in the first place if we're only going to mess with it.
lst opht ifht
(cdr (assoceq (ffnsymb term)
(access bddspv bddspv
:bddrulesalist)))
ttree bddspv state)))))))))
(defun bddalist (formals actuals alist opht ifht mxid ttree bddspv state)
(declare (type (signedbyte 29) mxid))
(themv
5
(signedbyte 29)
(cond
((endp formals)
(mvf mxid nil opht ifht ttree))
(t (mvlet? (mxid bdd opht ifht ttree)
(bdd (car actuals) alist opht ifht mxid ttree bddspv state)
(mvlet? (mxid restalist opht ifht ttree)
(bddalist (cdr formals) (cdr actuals)
alist opht ifht mxid ttree bddspv state)
(mvf mxid
(cons (cons (car formals) bdd)
restalist)
opht ifht ttree)))))))
(defun bddlist (lst alist opht ifht mxid ttree bddspv state)
(declare (type (signedbyte 29) mxid))
(themv
5
(signedbyte 29)
(cond
((endp lst)
(mvf mxid nil opht ifht ttree))
(t (mvlet? (mxid bdd opht ifht ttree)
(bdd (car lst) alist opht ifht mxid ttree bddspv state)
(mvlet? (mxid rest opht ifht ttree)
(bddlist (cdr lst) alist opht ifht mxid ttree
bddspv state)
(mvf mxid (cons bdd rest) opht ifht ttree)))))))
)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;;; VIII. TOPLEVEL (INTERFACE) ROUTINES ;;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; We will ignore declaration opportunities in this section, especially for
; declaring mxid to be a fixnum, because efficiency is a minor issue at this
; level.
; See axioms.lisp for the definition of if*.
(defun ifhtmaxlength (state)
(if (fboundpglobal 'ifhtmaxlength state)
(fgetglobal 'ifhtmaxlength state)
(+ 100000 (hashsize))))
(defun ophtmaxlength (state)
(if (fboundpglobal 'ophtmaxlength state)
(fgetglobal 'ophtmaxlength state)
(+ 100000 (hashsize))))
(defun leafcstlisttoalist (leafcstlist)
; Leafcstlist is a list of leaf csts of the form (uniqueid var boolflg).
; We return a corresponding alist in which each variable is paired with its
; cst.
(cond
((endp leafcstlist)
nil)
(t (cons (cons (trm (car leafcstlist))
(car leafcstlist))
(leafcstlisttoalist (cdr leafcstlist))))))
#+(and gcl (not acl2looponly))
(defvar *requestbiggerfixnumtable*
(fboundp 'system::allocatebiggerfixnumrange))
(defun bddtop (term inputvars boolvars bddconstructors clid ens state)
; This function returns a bddnote, where if an "error" occurs then the cst is
; nil. This bddnote has an empty :term field.
; Inputvars should be the list of all variables, with the highest priority
; variables (those which will have the lowest uniqueids) listed first. At any
; rate, all variables in boolvars are to be considered Booleanvalued.
; This function is allowed to assume that we are in a context where only
; propositional equivalence need be maintained.
(let* ((fns (allfnnames term))
(wrld (w state)))
(mvlet (fns bddrulesalist)
(bddrulesalist (remove1eq 'if fns)
(addtoseteq 'if fns)
nil
ens
wrld)
(let ((opalist (opalist fns nil 6 ens wrld))
(ifht (compress1 'ifht
`((:header :dimensions
(,(1+ (hashsize)))
:maximumlength
,(ifhtmaxlength state)
:default nil))))
(opht (compress1 'opht
`((:header :dimensions
(,(1+ (hashsize)))
:maximumlength
,(ophtmaxlength state)
:default nil))))
(allvars (let ((termvars (reverse (allvars term))))
; So, termvars has the variables in print order of first occurrence, a very
; unsatisfying but very simple heuristic.
(cond ((not (symbollistp inputvars))
(er hard 'bddtop
"The second argument of BDDTOP must ~
be a list of variables, but ~x0 is ~
not."
inputvars))
((subsetpeq termvars inputvars)
inputvars)
(t (er hard 'bddtop
"The following variables are free ~
in the input term, ~x0, but not do ~
not occur in the specified input ~
variables, ~x1: ~x2."
term inputvars
(setdifferenceeq termvars
inputvars)))))))
#+(and (not acl2looponly) akcl)
(cond ((and (fboundp 'si::sgcon)
(si::sgcon))
(fms "NOTE: Turning off SGC. If you wish to turn SGC ~
back on again, execute (SI::SGCON T) in raw Lisp.~"
nil (standardco *thelivestate*)
*thelivestate* nil)
(si::sgcon nil)))
#+(and gcl (not acl2looponly))
(cond (*requestbiggerfixnumtable*
(allocatefixnumrange 0 (hashsize))
(setq *requestbiggerfixnumtable* nil)))
(mvlet (mxid leafcstlist)
(leafcstlist allvars
boolvars
nil
(max (uniqueid *cstnil*)
(uniqueid *cstt*)))
(mvlet (mxid cst opht ifht ttree)
(bdd term (leafcstlisttoalist leafcstlist)
opht ifht mxid nil
(make bddspv
:opalist opalist
:bddrulesalist bddrulesalist
:bddconstructors bddconstructors)
state)
(cond
((stringp cst)
; Then we actually have
; (mv mxid fmtstring (cons fmtalist badcst) callstack ttree).
(make bddnote
:clid clid
:goalterm term
:mxid mxid
:errstring cst
:fmtalist (car opht)
:cst (cdr opht)
:term nil
:bddcallstack ifht
:ttree ttree))
(t
(make bddnote
:clid clid
:goalterm term
:mxid mxid
:errstring nil
:fmtalist nil
:cst cst
:term nil
:bddcallstack nil
:ttree ttree)))))))))
(defun getboolvars (vars typealist ttree acc)
(cond
((endp vars) (mv acc ttree))
(t (let ((entry
; We use the lowlevel function assoceq here so that it is clear we are not
; depending on the ACL2 world.
(assoceq (car vars) typealist)))
(cond
((and entry
(tssubsetp (cadr entry) *tsboolean*))
(getboolvars (cdr vars)
typealist
(constagtrees (cddr entry) ttree)
(cons (car vars) acc)))
(t (getboolvars (cdr vars) typealist ttree acc)))))))
(defun bddclause1 (hintalist typealist cl position ttree0 clid ens wrld
state)
; Returns (mv hitp x y), where:
; if hitp is 'error then x is a msg and y is nil or a bddnote;
; if hitp is 'miss then x is nil and y is a bddnote;
; else hitp is 'hit, in which case x is a list of clauses and y is a ttree.
(let* ((term (case position
(:conc (mconsterm* 'if (car (last cl)) *t* *nil*))
(:all (mconsterm* 'if (disjoin cl) *t* *nil*))
(otherwise
(let ((lit (nth position cl)))
(casematch
lit
(('not x)
(mconsterm* 'if x *t* *nil*))
(t (mconsterm* 'not lit)))))))
(allvars (allvars term))
(varshint (cdr (assoceq :vars hintalist)))
(provehint (if (assoceq :prove hintalist)
(cdr (assoceq :prove hintalist))
t))
(bddconstructorshint
(if (assoceq :bddconstructors hintalist)
(cdr (assoceq :bddconstructors hintalist))
(bddconstructors wrld))))
(mvlet
(boolvars ttree1)
(getboolvars allvars typealist ttree0 nil)
(cond
((not (subsetpeq (if (eq varshint t) allvars varshint)
boolvars))
(let ((badvars
(setdifferenceeq (if (eq varshint t) allvars varshint)
boolvars)))
(mv 'error
(msg "The following variable~#0~[ is~/s are~] not known to be ~
Boolean by trivial (type set) reasoning: ~&0. Perhaps you ~
need to add hypotheses to that effect. Alternatively, you ~
may want to prove :typeprescription rules (see :DOC ~
typeprescription) or :forwardchaining (see :DOC ~
forwardchaining) rules to help with the situation, or ~
perhaps to start with the hint ~x1."
badvars
(list :cases
(if (consp (cdr badvars))
(list (cons 'and
(pairlis$
(makelist (length badvars)
:initialelement 'booleanp)
(pairlis$ badvars nil))))
`((booleanp ,(car badvars))))))
nil)))
(t
(let* ((realvarshint (if (eq varshint t) nil varshint))
(bddnote (bddtop term
(append realvarshint
(setdifferenceeq
(reverse allvars)
realvarshint))
boolvars
bddconstructorshint
clid
ens
state))
(cst (access bddnote bddnote :cst))
(errstring (access bddnote bddnote :errstring))
(ttree (access bddnote bddnote :ttree)))
(cond
(errstring
; An error occurred; we aborted the bdd computation.
(if provehint
(mv 'error
(cons (access bddnote bddnote :errstring)
(access bddnote bddnote :fmtalist))
bddnote)
(mv 'miss nil bddnote)))
((csttp cst)
(mv 'hit
nil
(addtotagtree
'bddnote
bddnote
(consintottree ttree ttree1))))
(provehint
(mv 'error
(list "The :BDD hint for the current goal has ~
successfully simplified this goal, but has ~
failed to prove it. Consider using (SHOWBDD) ~
to suggest a counterexample; see :DOC showbdd.")
bddnote))
(t (mvlet
(newterm cstarray)
(decodecst
cst
(leafcstlistarray
(access bddnote bddnote :mxid)))
(declare (ignore cstarray))
(let* ((bddnote (change bddnote bddnote
:term newterm))
(ttree (addtotagtree
'bddnote
bddnote
(consintottree ttree ttree1))))
(cond
((eq position :conc)
(mv 'hit
(list (addliteral newterm
(butlast cl 1)
t))
ttree))
((eq position :all)
(mv 'hit
(list (addliteral newterm nil nil))
ttree))
(t ; hypothesis
(mv 'hit
(list (substforntharg (dumbnegatelit newterm)
position
cl))
ttree)))))))))))))
(defmacro expandandorsimple+
(term bool fnstobeignoredbyrewrite wrld ttree)
; Unlike expandandorsimple, the list of terms (second value) returned by
; this macro is always ``correct,'' and the hitp value is always nonnil.
`(mvlet (hitp lst ttree1)
(expandandorsimple
,term ,bool ,fnstobeignoredbyrewrite ,wrld ,ttree)
(cond (hitp (mv hitp lst ttree1))
(t (mv t (list ,term) ,ttree)))))
(defun expandandorsimple
(term bool fnstobeignoredbyrewrite wrld ttree)
; See the comment in expandclause. This is a simple version of expandandor
; that does not expand abbreviations or, in fact, use lemmas at all (just the
; definitions of NOT, IF, and IMPLIES). We expand the toplevel fn symbol of
; term provided the expansion produces a conjunction  when bool is nil  or
; a disjunction  when bool is t. We return three values: a hitp flag
; denoting success, the resulting list of terms (to be conjoined or disjoined
; to produce a term equivalent to term), and a new ttree. If the hitp flag is
; nil then we make no guarantees about the ``resulting list of terms,'' which
; in fact (for efficiency) is typically nil.
; Note that this function only guarantees propositional (iff) equivalence of
; term with the resulting conjunction or disjunction.
(cond ((variablep term)
(mv nil nil ttree))
((fquotep term)
(cond
((equal term *nil*)
(if bool (mv t nil ttree) (mv nil nil ttree)))
((equal term *t*)
(if bool (mv nil nil ttree) (mv t nil ttree)))
(t
(if bool (mv t (list *t*) ttree) (mv t nil ttree)))))
((memberequal (ffnsymb term) fnstobeignoredbyrewrite)
(mv nil nil ttree))
((flambdaapplicationp term)
; We don't use (andorp (lambdabody (ffnsymb term)) bool) here because that
; approach ignores nested lambdas.
(mvlet (hitp lst ttree0)
(expandandorsimple
(lambdabody (ffnsymb term))
bool fnstobeignoredbyrewrite wrld ttree)
(cond
(hitp (mv hitp
(subcorvarlst
(lambdaformals (ffnsymb term))
(fargs term)
lst)
ttree0))
(t (mv nil nil ttree)))))
((eq (ffnsymb term) 'not)
(mvlet (hitp lst ttree0)
(expandandorsimple (fargn term 1) (not bool)
fnstobeignoredbyrewrite wrld ttree)
(cond (hitp
(mv hitp
(dumbnegatelitlst lst)
(pushlemma (fnrunenume 'not nil nil wrld)
ttree0)))
(t (mv nil nil ttree)))))
((and (eq (ffnsymb term) 'implies)
bool)
(expandandorsimple
(subcorvar (formals 'implies wrld)
(fargs term)
(body 'implies t wrld))
bool fnstobeignoredbyrewrite wrld
(pushlemma (fnrunenume 'implies nil nil wrld)
ttree)))
((eq (ffnsymb term) 'if)
(let ((t1 (fargn term 1))
(t2 (fargn term 2))
(t3 (fargn term 3)))
(cond
((or (equal t1 *nil*)
(equal t2 t3))
(expandandorsimple+ t3 bool fnstobeignoredbyrewrite
wrld ttree))
((quotep t1)
(expandandorsimple+ t2 bool fnstobeignoredbyrewrite
wrld ttree))
((and (quotep t2) (quotep t3))
(cond
((equal t2 *nil*)
; We already know t2 is not t3, so we have t3 = *t* up to iffequivalence, and
; hence we are looking at (not t1) up to iffequivalence.
(mvlet (hitp lst ttree)
(expandandorsimple t1 (not bool)
fnstobeignoredbyrewrite
wrld ttree)
(mv t
(if hitp
(dumbnegatelitlst lst)
(list (dumbnegatelit t1)))
ttree)))
((equal t3 *nil*)
(expandandorsimple+ t1 bool
fnstobeignoredbyrewrite
wrld ttree))
(t
(expandandorsimple *t* bool
fnstobeignoredbyrewrite
wrld ttree))))
((and (quotep t3)
(eq (not bool) (equal t3 *nil*)))
; We combine the cases (or (not t1) t2) [bool = t] and (and t1 t2) [bool =
; nil].
(mvlet (hitp lst1 ttree)
(expandandorsimple+ t1 nil
fnstobeignoredbyrewrite
wrld ttree)
(declare (ignore hitp))
(mvlet (hitp lst2 ttree)
(expandandorsimple+
t2 bool
fnstobeignoredbyrewrite wrld ttree)
(declare (ignore hitp))
(if bool
(mv t
(unionequal (dumbnegatelitlst lst1)
lst2)
ttree)
(mv t (unionequal lst1 lst2) ttree)))))
((and (quotep t2)
(eq (not bool) (equal t2 *nil*)))
; We combine the cases (or t1 t3) [bool = t] and (and (not t1) t3)
; [bool = nil].
(mvlet (hitp lst1 ttree)
(expandandorsimple+ t1 t
fnstobeignoredbyrewrite
wrld ttree)
(declare (ignore hitp))
(mvlet (hitp lst2 ttree)
(expandandorsimple+
t3 bool
fnstobeignoredbyrewrite wrld ttree)
(declare (ignore hitp))
(if bool
(mv t (unionequal lst1 lst2) ttree)
(mv t
(unionequal (dumbnegatelitlst lst1)
lst2)
ttree)))))
(t (mv nil nil ttree)))))
(t (mv nil nil ttree))))
(defun expandclause
(cl fnstobeignoredbyrewrite wrld ttree acc)
; A classic form for a bdd problem is something like the following.
; (let ((x (list x0 x1 ...))
; (implies (booleanlistp x)
; ...)
; How do we let the bdd package know that x0, x1, ... are Boolean? It needs to
; know that x really is (list x0 x1 ...), and then it needs to forwardchain
; from (booleanlistp (list x0 x1 ...)) to the conjunction of (booleanp xi).
; However, the clause handed to bddclause may be a oneelement clause with the
; literal displayed above, so here we "flatten" this literal into a clause that
; is more amenable to forwardchaining.
(cond
((endp cl) (mv acc ttree))
(t (mvlet (hitp lst ttree)
(expandandorsimple+
(car cl) t fnstobeignoredbyrewrite wrld ttree)
(declare (ignore hitp))
(expandclause (cdr cl) fnstobeignoredbyrewrite wrld
ttree (unionequal lst acc))))))
(defun bddclause (bddhint clid topclause pspv wrld state)
; This function is analogous to simplifyclause (except that bddhint is passed
; in here), and shares much code with simplifyclause1. It is separated out
; from applytophintsclause for readability. We return 4 values, as required
; by applytophintsclause.
; Unlike simplifyclause1, we do not call oktoforce, but instead we do not
; force during forwardchaining. We may want to revisit that decision, but
; for now, we prefer to minimize forcing during bdd processing.
(let ((rcnst (access provespecvar pspv :rewriteconstant))
(literalhint (or (cdr (assoceq :literal bddhint))
:all)))
(cond
((and (integerp literalhint)
; Note that literalhint is a 0based index; see translatebddhint1. We know
; that literalhint is nonnegative, translatebddhint1 never returns a
; negative literalhint.
(not (< literalhint (1 (length topclause)))))
(mv 'error
(msg "There ~#0~[are no hypotheses~/is only one hypothesis~/are only ~
~n0 hypotheses~] in this goal, but your :BDD hint suggested ~
that there would be at least ~x1 ~
~#1~[~/hypothesis~/hypotheses]."
(1 (length topclause))
(1+ literalhint))
nil
pspv))
(t
(mvlet (hitp currentclause currentclausepts
removetrivialequivalencesttree)
(removetrivialequivalences topclause
(enumerateelements topclause 0)
t
(access rewriteconstant rcnst
:currentenabledstructure)
wrld state nil nil nil)
(declare (ignore hitp))
(let ((position (cond ((integerp literalhint)
(position literalhint
currentclausepts))
(t literalhint))))
(cond
((or (null position)
(and (eq literalhint :conc)
(not (member (1 (length topclause))
currentclausepts))))
(mv 'error
(msg "The attempt to use a :BDD hint for the goal named ~
\"~@0\" has failed. The problem is that the hint ~
specified that BDD processing was to be used on ~
the ~#1~[~n2 hypothesis~/conclusion~], which has ~
somehow disappeared. One possibility is that this ~
literal is an equivalence that has disappeared ~
after being used for substitution into the rest of ~
the goal. Another possibility is that this ~
literal has merged with another. We suspect, ~
therefore, that you would benefit by reconsidering ~
this :BDD hint, possibly attaching it to a ~
subsequent goal instead."
(tilde@clauseidphrase clid)
(if (null position) 0 1)
(if (null position) (1+ literalhint) 0))
nil
pspv))
(t
(let ((ens (access rewriteconstant rcnst
:currentenabledstructure)))
(mvlet (expandedclause ttree)
(expandclause
currentclause
(access rewriteconstant
rcnst
:fnstobeignoredbyrewrite)
wrld removetrivialequivalencesttree nil)
(mvlet
(contradictionp typealist fcpairlst)
(forwardchain expandedclause
nil
nil ; Let's not force
t ; donotreconsiderp
wrld
ens
(matchfreeoverride wrld)
state)
(cond
(contradictionp
; Note: When forwardchain returns with contradictionp = t, then the
; "fcpairlst" is really a ttree. We must add the removetrivial
; equivalences ttree to the ttree returned by forwardchain and we must
; remember our earlier case splits.
(mv t
nil
(constagtrees ttree fcpairlst)
pspv))
(t (mvlet (changedp clauses ttree)
; Ttree is either nil or a bddnote if changedp is 'miss or 'error. See
; waterfallstep.
(bddclause1 bddhint typealist
currentclause position
ttree
clid ens wrld state)
(mv changedp clauses ttree
pspv)))))))))))))))
; See showbdd and successive definitions for code used to inspect the
; results of using OBDDs.
(deflabel obdd
:doc
":DocSection Miscellaneous
ordered binary decision diagrams with rewriting~/
~l[bdd] for information on this topic.~/~/")
(deflabel bddalgorithm
; Note: the ``IFliftingforIF loop'' described here is really
; combineifcsts+.
:doc
":DocSection Bdd
summary of the BDD algorithm in ACL2~/
The BDD algorithm in ACL2 uses a combination of manipulation of
~c[IF] terms and unconditional rewriting. In this discussion we
begin with some relevant mathematical theory. This is followed by a
description of how ACL2 does BDDs, including concluding discussions
of soundness, completeness, and efficiency.
We recommend that you read the other documentation about BDDs in
ACL2 before reading the rather technical material that follows.
~l[BDD].~/
Here is an outline of our presentation. Readers who want a user
perspective, without undue mathematical theory, may wish to skip to
Part (B), referring to Part (A) only on occasion if necessary.
(A) ~st[Mathematical Considerations]
~bq[]
(A1) BDD term order
(A2) BDDconstructors and BDD terms, and their connection with
aborting the BDD algorithm
(A3) Canonical BDD terms
(A4) A theorem stating the equivalence of provable and syntactic
equality for canonical BDD terms
~eq[]
(B) ~st[Algorithmic Considerations]
~bq[]
(B1) BDD rules (rules used by the rewriting portion of the ACL2 BDD
algorithm)
(B2) Terms ``known to be Boolean''
(B3) An ``IFlifting'' operation used by the algorithm, as well as an
iterative version of that operation
(B4) The ACL2 BDD algorithm
(B5) Soundness and Completeness of the ACL2 BDD algorithm
(B6) Efficiency considerations
~eq[]
(A) ~st[Mathematical Considerations]
(A1) ~em[BDD term order]
Our BDD algorithm creates a total ``BDD term order'' on ACL2 terms,
on the fly. We use this order in our discussions below of
IFlifting and of canonical BDD terms, and in the algorithm's use of
commutativity. The particular order is unimportant, except that we
guarantee (for purposes of commutative functions) that constants are
smaller in this order than nonconstants.
(A2) ~em[BDDconstructors] (assumed to be ~c['(cons)]) and ~em[BDD terms]
We take as given a list of function symbols that we call the
``BDDconstructors.'' By default, the only BDDconstructor is
~ilc[cons], although it is legal to specify any list of function
symbols as the BDDconstructors, either by using the
~il[acl2defaultstable] (~pl[acl2defaultstable]) or by
supplying a ~c[:BDDCONSTRUCTORS] hint (~pl[hints]). Warning:
this capability is largely untested and may produce undesirable
results. Henceforth, except when explicitly stated to the contrary,
we assume that BDDconstructors is ~c['(cons)].
Roughly speaking, a ~il[BDD] term is the sort of ~il[term] produced
by our BDD algorithm, namely a tree with all ~ilc[cons] nodes lying
above all non~c[CONS] nodes. More formally, a ~il[term] is said to
be a ~il[BDD] term if it contains ~st[no] subterm of either of the
following forms, where ~c[f] is not ~c[CONS].
~bv[]
(f ... (CONS ...) ...)
(f ... 'x ...) ; where (consp x) = t
~ev[]
We will see that whenever the BDD algorithm attempts to create a
~il[term] that is not a ~il[BDD] term, it aborts instead. Thus,
whenever the algorithm completes without aborting, it creates a
~il[BDD] term.
(A3) ~em[Canonical BDD terms]
We can strengthen the notion of ``BDD term'' to a notion of
``canonical BDD term'' by imposing the following additional
requirements, for every subterm of the form ~c[(IF x y z)]:
~bq[]
(a) ~c[x] is a variable, and it precedes (in the BDD term order)
every variable occurring in ~c[y] or ~c[z];
(b) ~c[y] and ~c[z] are syntactically distinct; and,
(c) it is not the case that ~c[y] is ~c[t] and ~c[z] is ~c[nil].
~eq[]
We claim that it follows easily from our description of the BDD
algorithm that every term it creates is a canonical BDD term,
assuming that the variables occurring in all such terms are treated
by the algorithm as being Boolean (see (B2) below) and that the
terms contain no function symbols other than ~c[IF] and ~c[CONS].
Thus, under those assumptions the following theorem shows that the
BDD algorithm never creates distinct terms that are provably equal,
a property that is useful for completeness and efficiency (as we
explain in (B5) and (B6) below).
(A4) ~em[Provably equal canonical BDD terms are identical]
We believe that the following theorem and proof are routine
extensions of a standard result and proof to terms that allow calls
of ~c[CONS].
~st[Theorem]. Suppose that ~c[t1] and ~c[t2] are canonical BDD terms
that contain no function symbols other than ~c[IF] and ~c[CONS]. Also
suppose that ~c[(EQUAL t1 t2)] is a theorem. Then ~c[t1] and ~c[t2]
are syntactically identical.
Proof of theorem: By induction on the total number of symbols
occurring in these two terms. First suppose that at least one term
is a variable; without loss of generality let it be ~c[t1]. We must
prove that ~c[t2] is syntactically the same as ~c[t1]. Now it is
clearly consistent that ~c[(EQUAL t1 t2)] is false if ~c[t2] is a call
of ~c[CONS] (to see this, simply let ~c[t1] be an value that is not a
~c[CONSP]). Similarly, ~c[t2] cannot be a constant or a variable
other than ~c[t1]. The remaining possibility to rule out is that
~c[t2] is of the form ~c[(IF t3 t4 t5)], since by assumption its
function symbol must be ~c[IF] or ~c[CONS] and we have already handled
the latter case. Since ~c[t2] is canonical, we know that ~c[t3] is a
variable. Since ~c[(EQUAL t1 t2)] is provable, i.e.,
~bv[]
(EQUAL t1 (if t3 t4 t5))
~ev[]
is provable, it follows that we may substitute either ~c[t] or ~c[nil]
for ~c[t3] into this equality to obtain two new provable equalities.
First, suppose that ~c[t1] and ~c[t3] are distinct variables. Then
these substitutions show that ~c[t1] is provably equal to both ~c[t4]
and ~c[t5] (since ~c[t3] does not occur in ~c[t4] or ~c[t5] by property
(a) above, as ~c[t2] is canonical), and hence ~c[t4] and ~c[t5] are
provably equal to each other, which implies by the inductive
hypothesis that they are the same term ~[] and this contradicts the
assumption that ~c[t2] is canonical (property (b)). Therefore ~c[t1]
and ~c[t3] are the same variable, i.e., the equality displayed above
is actually ~c[(EQUAL t1 (if t1 t4 t5))]. Substituting ~c[t] and then
~c[nil] for ~c[t1] into this provable equality lets us prove ~c[(EQUAL t t4)]
and ~c[(EQUAL nil t5)], which by the inductive hypothesis implies
that ~c[t4] is (syntactically) the term ~c[t] and ~c[t5] is ~c[nil].
That is, ~c[t2] is ~c[(IF t1 t nil)], which contradicts the assumption
that ~c[t2] is canonical (property (c)).
Next, suppose that at least one term is a call of ~c[IF]. Our first
observation is that the other term is also a call of ~c[IF]. For if
the other is a call of ~c[CONS], then they cannot be provably equal,
because the former has no function symbols other than ~c[IF] and
hence is Boolean when all its variables are assigned Boolean values.
Also, if the other is a constant, then both branches of the ~c[IF]
term are provably equal to that constant and hence these branches
are syntactically identical by the inductive hypothesis,
contradicting property (b). Hence, we may assume for this case that
both terms are calls of ~c[IF]; let us write them as follows.
~bv[]
t0: (IF t1 t2 t3)
u0: (IF u1 u2 u3)
~ev[]
Note that ~c[t1] and ~c[u1] are variables, by property (a) of
canonical BDD terms. First we claim that ~c[t1] does not strictly
precede ~c[u1] in the BDD term order. For suppose ~c[t1] does
strictly precede ~c[u1]. Then property (a) of canonical BDD terms
guarantees that ~c[t1] does not occur in ~c[u0]. Hence, an argument
much like one used above shows that ~c[u0] is provably equal to both
~c[t2] (substituting ~c[t] for ~c[t1]) and ~c[t3] (substituting ~c[nil]
for ~c[t1]), and hence ~c[t2] and ~c[t3] are provably equal. That
implies that they are identical terms, by the inductive hypothesis,
which then contradicts property (b) for ~c[t0]. Similarly, ~c[u1]
does not strictly precede ~c[t1] in the BDD term order. Therefore,
~c[t1] and ~c[u1] are the same variable. By substituting ~c[t] for
this variable we see that ~c[t2] and ~c[u2] are provably equal, and
hence they are equal by the inductive hypothesis. Similarly, by
substituting ~c[nil] for ~c[t1] (and ~c[u1]) we see that ~c[t3] and
~c[u3] are provably, hence syntactically, equal.
We have covered all cases in which at least one term is a variable
or at least one term is a call of ~c[IF]. If both terms are
constants, then provable and syntactic equality are clearly
equivalent. Finally, then, we may assume that one term is a call of
~c[CONS] and the other is a constant or a call of ~c[CONS]. The
constant case is similar to the ~c[CONS] case if the constant is a
~c[CONSP], so we omit it; while if the constant is not a ~c[CONSP]
then it is not provably equal to a call of ~c[CONS]; in fact it is
provably ~em[not] equal!
So, we are left with a final case, in which canonical BDD terms
~c[(CONS t1 t2)] and ~c[(CONS u1 u2)] are provably equal, and we want
to show that ~c[t1] and ~c[u1] are syntactically equal as are ~c[t2]
and ~c[u2]. These conclusions are easy consequences of the inductive
hypothesis, since the ACL2 axiom ~c[CONSEQUAL] (which you can
inspect using ~c[:]~ilc[PE]) shows that equality of the given terms is
equivalent to the conjunction of ~c[(EQUAL t1 t2)] and ~c[(EQUAL u1 u2)].
Q.E.D.
(B) ~st[Algorithmic Considerations]
(B1) ~em[BDD rules]
A rule of class ~c[:]~ilc[rewrite] (~pl[ruleclasses]) is said to be
a ``~il[BDD] rewrite rule'' if and only if it satisfies the
following criteria. (1) The rule is ~il[enable]d. (2) Its
~il[equivalence] relation is ~ilc[equal]. (3) It has no hypotheses.
(4) Its ~c[:]~ilc[loopstopper] field is ~c[nil], i.e., it is not a
permutative rule. (5) All variables occurring in the rule occur in
its lefthand side (i.e., there are no ``free variables'';
~pl[rewrite]). A rule of class ~c[:]~ilc[definition]
(~pl[ruleclasses]) is said to be a ``~il[BDD] definition rule''
if it satisfies all the criteria above (except (4), which does not
apply), and moreover the top function symbol of the lefthand side
was not recursively (or mutually recursively) defined. Technical
point: Note that this additional criterion is independent of
whether or not the indicated function symbol actually occurs in the
righthand side of the rule.
Both BDD rewrite rules and BDD definition rules are said to be ``BDD
rules.''
(B2) ~em[Terms ''known to be Boolean'']
We apply the BDD algorithm in the context of a toplevel goal to
prove, namely, the goal at which the ~c[:BDD] hint is attached. As
we run the BDD algorithm, we allow ourselves to say that a set of
~il[term]s is ``known to be Boolean'' if we can verify that the goal
is provable from the assumption that at least one of the terms is
not Boolean. Equivalently, we allow ourselves to say that a set of
terms is ``known to be Boolean'' if we can verify that the original
goal is provably equivalent to the assertion that if all terms in
the set are Boolean, then the goal holds. The notion ``known to be
Boolean'' is conservative in the sense that there are generally sets
of terms for which the above equivalent criteria hold and yet the
sets of terms are not noted as as being ``known to be Boolean.''
However, ACL2 uses a number of tricks, including ~il[typeset]
reasoning and analysis of the structure of the toplevel goal, to
attempt to establish that a sufficiently inclusive set of terms is
known to be Boolean.
From a practical standpoint, the algorithm determines a set of terms
known to be Boolean; we allow ourselves to say that each term in
this set is ``known to be Boolean.'' The algorithm assumes that
these terms are indeed Boolean, and can make use of that assumption.
For example, if ~c[t1] is known to be Boolean then the algorithm
simplifies ~c[(IF t1 t nil)] to ~c[t1]; see (iv) in the discussion
immediately below.
(B3) ~em[IFlifting] and the ~em[IFliftingforIF loop]
Suppose that one has a ~il[term] of the form ~c[(f ... (IF test x y) ...)],
where ~c[f] is a function symbol other than ~c[CONS]. Then we say
that ``IFlifting'' ~c[test] ``from'' this term produces the
following term, which is provably equal to the given term.
~bv[]
(if test
(f ... x ...) ; resulting true branch
(f ... y ...)) ; resulting false branch
~ev[]
Here, we replace each argument of ~c[f] of the form ~c[(IF test .. ..)],
for the same ~c[test], in the same way. In this case we say that
``IFlifting applies to'' the given term, ``yielding the test''
~c[test] and with the ``resulting two branches'' displayed above.
Whenever we apply IFlifting, we do so for the available ~c[test]
that is least in the BDD term order (see (A1) above).
We consider arguments ~c[v] of ~c[f] that are ``known to be Boolean''
(see above) to be replaced by ~c[(IF v t nil)] for the purposes of
IFlifting, i.e., before IFlifting is applied.
There is one special case, however, for IFlifting. Suppose that
the given term is of the form ~c[(IF v y z)] where ~c[v] is a variable
and is the test to be lifted out (i.e., it is least in the BDD term
order among the potential tests). Moroever, suppose that neither
~c[y] nor ~c[z] is of the form ~c[(IF v W1 W2)] for that same ~c[v].
Then IFlifting does not apply to the given term.
We may now describe the IFliftingforIF loop, which applies to
terms of the form ~c[(IF test tbr fbr)] where the algorithm has
already produced ~c[test], ~c[tbr], and ~c[fbr]. First, if ~c[test] is
~c[nil] then we return ~c[fbr], while if ~c[test] is a non~c[nil]
constant or a call of ~c[CONS] then we return ~c[tbr]. Otherwise, we
see if IFlifting applies. If IFlifting does not apply, then we
return ~c[(IF test tbr fbr)]. Otherwise, we apply IFlifting to
obtain a term of the form ~c[(IF x y z)], by lifting out the
appropriate test. Now we recursively apply the IFliftingforIF
loop to the term ~c[(IF x y z)], unless any of the following special
cases apply.
~bq[]
(i) If ~c[y] and ~c[z] are the same term, then return ~c[y].
(ii) Otherwise, if ~c[x] and ~c[z] are the same term, then replace
~c[z] by ~c[nil] before recursively applying IFliftingforIF.
(iii) Otherwise, if ~c[x] and ~c[y] are the same term and ~c[y] is
known to be Boolean, then replace ~c[y] by ~c[t] before recursively
applying IFliftingforIF.
(iv) If ~c[z] is ~c[nil] and either ~c[x] and ~c[y] are the same term or
~c[x] is ``known to be Boolean'' and ~c[y] is ~c[t], then return ~c[x].
~eq[]
NOTE: When a variable ~c[x] is known to be Boolean, it is easy to
see that the form ~c[(IF x t nil)] is always reduced to ~c[x] by this
algorithm.
(B4) ~em[The ACL2 BDD algorithm]
We are now ready to present the BDD algorithm for ACL2. It is given
an ACL2 ~il[term], ~c[x], as well as an association list ~c[va] that
maps variables to terms, including all variables occurring in ~c[x].
We maintain the invariant that whenever a variable is mapped by
~c[va] to a term, that term has already been constructed by the
algorithm, except: initially ~c[va] maps every variable occurring in
the toplevel term to itself. The algorithm proceeds as follows.
We implicitly ordain that whenever the BDD algorithm attempts to
create a ~il[term] that is not a ~il[BDD] term (as defined above in
(A2)), it aborts instead. Thus, whenever the algorithm completes
without aborting, it creates a ~il[BDD] term.
~bq[]
If ~c[x] is a variable, return the result of looking it up in ~c[va].
If ~c[x] is a constant, return ~c[x].
If ~c[x] is of the form ~c[(IF test tbr fbr)], then first run the
algorithm on ~c[test] with the given ~c[va] to obtain ~c[test']. If
~c[test'] is ~c[nil], then return the result ~c[fbr'] of running the
algorithm on ~c[fbr] with the given ~c[va]. If ~c[test'] is a constant
other than ~c[nil], or is a call of ~c[CONS], then return the result
~c[tbr'] of running the algorithm on ~c[tbr] with the given ~c[va]. If
~c[tbr] is identical to ~c[fbr], return ~c[tbr]. Otherwise, return the
result of applying the IFliftingforIF loop (described above) to
the term ~c[(IF test' tbr' fbr')].
If ~c[x] is of the form ~c[(IF* test tbr fbr)], then compute the
result exactly as though ~ilc[IF] were used rather than ~ilc[IF*], except
that if ~c[test'] is not a constant or a call of ~c[CONS] (see
paragraph above), then abort the BDD computation. Informally, the
tests of ~ilc[IF*] terms are expected to ``resolve.'' NOTE: This
description shows how ~ilc[IF*] can be used to implement conditional
rewriting in the BDD algorithm.
If ~c[x] is a ~c[LAMBDA] expression ~c[((LAMBDA vars body) . args)]
(which often corresponds to a ~ilc[LET] term; ~pl[let]), then first
form an alist ~c[va'] by binding each ~c[v] in ~c[vars] to the result
of running the algorithm on the corresponding member of ~c[args],
with the current alist ~c[va]. Then, return the result of the
algorithm on ~c[body] in the alist ~c[va'].
Otherwise, ~c[x] is of the form ~c[(f x1 x2 ... xn)], where ~c[f] is a
function symbol other than ~ilc[IF] or ~ilc[IF*]. In that case, let
~c[xi'] be the result of running the algorithm on ~c[xi], for ~c[i]
from 1 to ~c[n], using the given alist ~c[va]. First there are a few
special cases. If ~c[f] is ~ilc[EQUAL] then we return ~c[t] if ~c[x1'] is
syntactically identical to ~c[x2'] (where this test is very fast; see
(B6) below); we return ~c[x1'] if it is known to be Boolean and
~c[x2'] is ~c[t]; and similarly, we return ~c[x2'] if it is known to be
Boolean and ~c[x1'] is ~c[t]. Next, if each ~c[xi'] is a constant and
the ~c[:]~ilc[executablecounterpart] of ~c[f] is enabled, then the
result is obtained by computation. Next, if ~c[f] is ~ilc[BOOLEANP] and
~c[x1'] is known to be Boolean, ~c[t] is returned. Otherwise, we
proceed as follows, first possibly swapping the arguments if they
are out of (the BDD term) order and if ~c[f] is known to be
commutative (see below). If a BDD rewrite rule (as defined above)
matches the term ~c[(f x1'... xn')], then the most recently stored
such rule is applied. If there is no such match and ~c[f] is a
BDDconstructor, then we return ~c[(f x1'... xn')]. Otherwise, if a
BDD definition rule matches this term, then the most recently stored
such rule (which will usually be the original definition for most
users) is applied. If none of the above applies and neither does
IFlifting, then we return ~c[(f x1'... xn')]. Otherwise we apply
IFlifting to ~c[(f x1'... xn')] to obtain a term ~c[(IF test tbr fbr)];
but we aren't done yet. Rather, we run the BDD algorithm (using the
same alist) on ~c[tbr] and ~c[fbr] to obtain terms ~c[tbr'] and
~c[fbr'], and we return ~c[(IF test tbr' fbr')] unless ~c[tbr'] is
syntactically identical to ~c[fbr'], in which case we return ~c[tbr'].
~eq[]
When is it the case that, as said above, ``~c[f] is known to be
commutative''? This happens when an enabled rewrite rule is of the
form ~c[(EQUAL (f X Y) (f Y X))]. Regarding swapping the arguments
in that case: recall that we may assume very little about the BDD
term order, essentially only that we swap the two arguments when the
second is a constant and the first is not, for example, in ~c[(+ x 1)].
Other than that situation, one cannot expect to predict accurately
when the arguments of commutative operators will be swapped.
(B5) Soundness and Completeness of the ACL2 BDD algorithm
Roughly speaking, ``soundness'' means that the BDD algorithm should
give correct answers, and ``completeness'' means that it should be
powerful enough to prove all true facts. Let us make the soundness
claim a little more precise, and then we'll address completeness
under suitable hypotheses.
~st[Claim] (Soundness). If the ACL2 BDD algorithm runs to
completion on an input term ~c[t0], then it produces a result that is
provably equal to ~c[t0].
We leave the proof of this claim to the reader. The basic idea is
simply to check that each step of the algorithm preserves the
meaning of the term under the bindings in the given alist.
Let us start our discussion of completeness by recalling the theorem
proved above in (A4).
~st[Theorem]. Suppose that ~c[t1] and ~c[t2] are canonical BDD terms
that contain no function symbols other than ~c[IF] and ~c[CONS]. Also
suppose that ~c[(EQUAL t1 t2)] is a theorem. Then ~c[t1] and ~c[t2]
are syntactically identical.
Below we show how this theorem implies the following completeness
property of the ACL2 BDD algorithm. We continue to assume that
~c[CONS] is the only BDDconstructor.
~st[Claim] (Completeness). Suppose that ~c[t1] and ~c[t2] are
provably equal terms, under the assumption that all their variables
are known to be Boolean. Assume further that under this same
assumption, toplevel runs of the ACL2 BDD algorithm on these terms
return terms that contain only the function symbols ~c[IF] and
~c[CONS]. Then the algorithm returns the same term for both ~c[t1]
and ~c[t2], and the algorithm reduces ~c[(EQUAL t1 t2)] to ~c[t].
Why is this claim true? First, notice that the second part of the
conclusion follows immediately from the first, by definition of the
algorithm. Next, notice that the terms ~c[u1] and ~c[u2] obtained by
running the algorithm on ~c[t1] and ~c[t2], respectively, are provably
equal to ~c[t1] and ~c[t2], respectively, by the Soundness Claim. It
follows that ~c[u1] and ~c[u2] are provably equal to each other.
Since these terms contain no function symbols other than ~c[IF] or
~c[CONS], by hypothesis, the Claim now follows from the Theorem above
together with the following lemma.
~st[Lemma]. Suppose that the result of running the ACL2 BDD
algorithm on a toplevel term ~c[t0] is a term ~c[u0] that contains
only the function symbols ~c[IF] and ~c[CONS], where all variables of
~c[t0] are known to be Boolean. Then ~c[u0] is a canonical BDD term.
Proof: left to the reader. Simply follow the definition of the
algorithm, with a separate argument for the IFliftingforIF loop.
Finally, let us remark on the assumptions of the Completeness Claim
above. The assumption that all variables are known to be Boolean is
often true; in fact, the system uses the forwardchaining rule
~c[booleanlistpforward] (you can see it using ~c[:]~ilc[pe]) to try to
establish this assumption, if your theorem has a form such as the
following.
~bv[]
(let ((x (list x0 x1 ...))
(y (list y0 y1 ...)))
(implies (and (booleanlistp x)
(booleanlistp y))
...))
~ev[]
Moreover, the ~c[:BDD] hint can be used to force the prover to abort
if it cannot check that the indicated variables are known to be
Boolean; ~pl[hints].
Finally, consider the effect in practice of the assumption that the
terms resulting from application of the algorithm contain calls of
~c[IF] and ~c[CONS] only. Typical use of BDDs in ACL2 takes place in
a theory (~pl[theories]) in which all relevant nonrecursive
function symbols are enabled and all recursive function symbols
possess enabled BDD rewrite rules that tell them how open up. For
example, such a rule may say how to expand on a given function
call's argument that has the form ~c[(CONS a x)], while another may
say how to expand when that argument is ~c[nil]). (See for example
the rules ~c[appendcons] and ~c[appendnil] in the documentation for
~ilc[IF*].) We leave it to future work to formulate a theorem that
guarantees that the BDD algorithm produces terms containing calls
only of ~c[IF] and ~c[CONS] assuming a suitably ``complete''
collection of rewrite rules.
(B6) ~em[Efficiency considerations]
Following Bryant's algorithm, we use a graph representation of
~il[term]s created by the BDD algorithm's computation. This
representation enjoys some important properties.
~bq[]
(Time efficiency) The test for syntactic equality of BDD terms is
very fast.
(Space efficiency) Equal BDD data structures are stored identically
in memory.
~eq[]
~em[Implementation note.] The representation actually uses a sort
of hash table for BDD terms that is implemented as an ACL2
1dimensional array. ~l[arrays]. In addition, we use a second
such hash table to avoid recomputing the result of applying a
function symbol to the result of running the algorithm on its
arguments. We believe that these uses of hash tables are standard.
They are also discussed in Moore's paper on BDDs; ~pl[bdd] for
the reference.")
(deflabel bddintroduction
:doc
":DocSection Bdd
examples illustrating the use of BDDs in ACL2~/
~l[bdd] for a brief introduction to BDDs in ACL2 and for
pointers to other documentation on BDDs in ACL2. Here, we
illustrate the use of BDDs in ACL2 by way of some examples.
For a further example, ~pl[if*].~/
Let us begin with a really simple example. (We will explain the
~c[:bdd] hint ~c[(:vars nil)] below.)
~bv[]
ACL2 !>(thm (equal (if a b c) (if (not a) c b))
:hints ((\"Goal\" :bdd (:vars nil)))) ; Prove with BDDs
[Note: A hint was supplied for our processing of the goal above.
Thanks!]
But simplification with BDDs (7 nodes) reduces this to T, using the
:definitions EQUAL and NOT.
Q.E.D.
Summary
Form: ( THM ...)
Rules: ((:DEFINITION EQUAL) (:DEFINITION NOT))
Warnings: None
Time: 0.18 seconds (prove: 0.05, print: 0.02, other: 0.12)
Proof succeeded.
ACL2 !>
~ev[]
The ~c[:bdd] hint ~c[(:vars nil)] indicates that BDDs are to be used
on the indicated goal, and that any socalled ``variable ordering''
may be used: ACL2 may use a convenient order that is far from
optimal. It is beyond the scope of the present documentation to
address the issue of how the user may choose good variable
orderings. Someday our implementation of BDDs may be improved to
include heuristicallychosen variable orderings rather than rather
random ones.
Here is a more interesting example.
~bv[]
(defun vnot (x)
; Complement every element of a list of Booleans.
(if (consp x)
(cons (not (car x)) (vnot (cdr x)))
nil))
; Now we prove a rewrite rule that explains how to open up vnot on
; a consp.
(defthm vnotcons
(equal (vnot (cons x y))
(cons (not x) (vnot y))))
; Finally, we prove for 7bit lists that vnot is selfinverting.
(thm
(let ((x (list x0 x1 x2 x3 x4 x5 x6)))
(implies (booleanlistp x)
(equal (vnot (vnot x)) x)))
:hints ((\"Goal\" :bdd
;; Note that this time we specify a variable order.
(:vars (x0 x1 x2 x3 x4 x5 x6)))))
~ev[]
It turns out that the variable order doesn't seem to matter in this
example; using several orders we found that 30 nodes were created,
and the proof time was about 1/10 of a second on a (somewhat
enhanced) Sparc 2. The same proof took about a minute and a half
without any ~c[:bdd] hint! This observation is a bit misleading
perhaps, since the theorem for arbitrary ~c[x],
~bv[]
(thm
(implies (booleanlistp x)
(equal (vnot (vnot x)) x)))
~ev[]
only takes about 1.5 times as long as the ~c[:bdd] proof for 7 bits,
above! Nevertheless, BDDs can be very useful in reducing proof
time, especially when there is no regular structure to facilitate
proof by induction, or when the induction scheme is so complicated
to construct that significant user effort is required to get the
proof by induction to go through.
Finally, consider the preceding example, with a ~c[:bdd] hint of
(say) ~c[(:vars nil)], but with the rewrite rule ~c[vnotcons] above
disabled. In that case, the proof fails, as we see below. That is
because the BDD algorithm in ACL2 uses hypothesisfree
~c[:]~il[rewrite] rules, ~c[:]~ilc[executablecounterpart]~c[s], and
nonrecursive definitions, but it does not use recursive definitions.
Notice that when we issue the ~c[(showbdd)] command, the system's
response clearly shows that we need a rewrite rule for simplifying
terms of the form ~c[(vnot (cons ...))].
~bv[]
ACL2 !>(thm
(let ((x (list x0 x1 x2 x3 x4 x5 x6)))
(implies (booleanlistp x)
(equal (vnot (vnot x)) x)))
:hints ((\"Goal\" :bdd (:vars nil)
:intheory (disable vnotcons))))
[Note: A hint was supplied for our processing of the goal above.
Thanks!]
ACL2 Error in ( THM ...): Attempted to create VNOT node during BDD
processing with an argument that is a call of a bddconstructor,
which would produce a nonBDD term (as defined in :DOC
bddalgorithm). See :DOC showbdd.
Summary
Form: ( THM ...)
Rules: NIL
Warnings: None
Time: 0.58 seconds (prove: 0.13, print: 0.00, other: 0.45)
******** FAILED ******** See :DOC failure ******** FAILED ********
ACL2 !>(showbdd)
BDD computation on Goal yielded 17 nodes.
==============================
BDD computation was aborted on Goal, and hence there is no
falsifying assignment that can be constructed. Here is a backtrace
of calls, starting with the toplevel call and ending with the one
that led to the abort. See :DOC showbdd.
(LET ((X (LIST X0 X1 X2 X3 X4 X5 ...)))
(IMPLIES (BOOLEANLISTP X)
(EQUAL (VNOT (VNOT X)) X)))
alist: ((X6 X6) (X5 X5) (X4 X4) (X3 X3) (X2 X2) (X1 X1) (X0 X0))
(EQUAL (VNOT (VNOT X)) X)
alist: ((X (LIST X0 X1 X2 X3 X4 X5 ...)))
(VNOT (VNOT X))
alist: ((X (LIST X0 X1 X2 X3 X4 X5 ...)))
(VNOT X)
alist: ((X (LIST X0 X1 X2 X3 X4 X5 ...)))
ACL2 !>
~ev[]
The term that has caused the BDD algorithm to abort is thus
~c[(VNOT X)], where ~c[X] has the value ~c[(LIST X0 X1 X2 X3 X4 X5 ...)],
i.e., ~c[(CONS X0 (LIST X1 X2 X3 X4 X5 ...))]. Thus, we see the utility
of introducing a rewrite rule to simplify terms of the form
~c[(VNOT (CONS ...))]. The moral of this story is that if you get
an error of the sort shown above, you may find it useful to execute
the command ~c[(showbdd)] and use the result as advice that suggests
the left hand side of a rewrite rule.
Here is another sort of failed proof. In this version we have
omitted the hypothesis that the input is a bit vector. Below we use
~c[showbdd] to see what went wrong, and use the resulting
information to construct a counterexample. This failed proof
corresponds to a slightly modified input theorem, in which ~c[x] is
bound to the 4element list ~c[(list x0 x1 x2 x3)].
~bv[]
ACL2 !>(thm
(let ((x (list x0 x1 x2 x3)))
(equal (vnot (vnot x)) x))
:hints ((\"Goal\" :bdd
;; This time we do not specify a variable order.
(:vars nil))))
[Note: A hint was supplied for our processing of the goal above.
Thanks!]
ACL2 Error in ( THM ...): The :BDD hint for the current goal has
successfully simplified this goal, but has failed to prove it.
Consider using (SHOWBDD) to suggest a counterexample; see :DOC
showbdd.
Summary
Form: ( THM ...)
Rules: NIL
Warnings: None
Time: 0.18 seconds (prove: 0.07, print: 0.00, other: 0.12)
******** FAILED ******** See :DOC failure ******** FAILED ********
ACL2 !>(showbdd)
BDD computation on Goal yielded 73 nodes.
==============================
Falsifying constraints:
((X0 \"Some nonnil value\")
(X1 \"Some nonnil value\")
(X2 \"Some nonnil value\")
(X3 \"Some nonnil value\")
((EQUAL 'T X0) T)
((EQUAL 'T X1) T)
((EQUAL 'T X2) T)
((EQUAL 'T X3) NIL))
==============================
Term obtained from BDD computation on Goal:
(IF X0
(IF X1
(IF X2 (IF X3 (IF # # #) (IF X3 # #))
(IF X2 'NIL (IF X3 # #)))
(IF X1 'NIL
(IF X2 (IF X3 # #) (IF X2 # #))))
(IF X0 'NIL
(IF X1 (IF X2 (IF X3 # #) (IF X2 # #))
(IF X1 'NIL (IF X2 # #)))))
ACL2 Query (:SHOWBDD): Print the term in full? (N, Y, W or ?):
n ; I've seen enough. The assignment shown above suggests
; (though not conclusively) that if we bind x3 to a nonnil
; value other than T, and bind x0, x1, and x2 to t, then we
; this may give us a counterexample.
ACL2 !>(let ((x0 t) (x1 t) (x2 t) (x3 7))
(let ((x (list x0 x1 x2 x3)))
;; Let's use LIST instead of EQUAL to see how the two
;; lists differ.
(list (vnot (vnot x)) x)))
((T T T T) (T T T 7))
ACL2 !>
~ev[]
~l[if*] for another example.")
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;;; IX. COMPILING THIS FILE AND OTHER HELPFUL TIPS
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
#
In order to check for slow code, you can execute the following from ACL2 inside
raw Lisp.
(compilefile "bdd.lisp" :cfile t)
Then, search the file bdd.c for make_fixnum and number_ for slow stuff. Note
that you'll find a lot of these, but you only need to worry about them in the
workhorse functions, and you don't need to worry about CMPmake_fixnum when it
is used for an error or for a new mxid.
When you find one of these, search upward for `local entry' to see which
function or macro you are in. Don't worry, for example, about commutativep,
which is a database kind of function rather than a workhorse function.
You'll see things like the following (from local entry to BDD). The idea here
is is that we are boxing a fixnum and pushing it on a stack, but why? LnkLI253
appears to be a function call, which is found near the end of the file to
correspond to leafcstlistarray. If we're still not clear on what's going
on, we can look up 273 as well. When we do this, we find that we are probably
in the part of the BDD code shown at the end, which is not a problem.
V1570 = CMPmake_fixnum(V1549);
V1571= (*(LnkLI253))(/* INLINEARGS */V1569,V1570);
V1572= (*(LnkLI273))((V1525),/* INLINEARGS */V1571);
....
static object LnkTLI273(va_alist)va_dcl{va_list ap;va_start(ap);return(object )call_proc(VV[273],&LnkLI273,2,ap);} /* DECODECSTALIST */
static object LnkTLI253(va_alist)va_dcl{va_list ap;va_start(ap);return(object )call_proc(VV[253],&LnkLI253,2,ap);} /* LEAFCSTLISTARRAY */
; Source code from (defun bdd ...) [an earlier version]:
(bdderror
mxid
"Unable to resolve test of IF* for term~~%~p0~~%under the ~
bindings~~%~x1~~% use SHOWBDD to see a backtrace."
(list (cons #\0 (untranslate term nil))
(cons #\1
(decodecstalist alist
(leafcstlistarray
(stripcdrs alist)
mxid))))
; We need a cst next, though we don't care about it.
*cstt*
ttree)
#
