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 4027 4028 4029 4030 4031 4032 4033 4034 4035 4036 4037 4038 4039 4040 4041 4042 4043 4044 4045 4046 4047 4048 4049 4050 4051 4052 4053 4054 4055 4056 4057 4058 4059 4060 4061 4062 4063 4064 4065 4066 4067 4068 4069 4070 4071 4072 4073 4074 4075 4076 4077 4078 4079 4080 4081 4082 4083 4084 4085 4086 4087 4088 4089 4090 4091 4092 4093 4094 4095 4096 4097 4098 4099 4100 4101 4102 4103 4104 4105 4106 4107 4108 4109 4110 4111 4112 4113 4114 4115 4116 4117 4118 4119 4120 4121 4122 4123 4124 4125 4126 4127 4128 4129 4130 4131 4132 4133 4134 4135 4136 4137 4138 4139 4140 4141 4142 4143 4144 4145 4146 4147 4148 4149 4150 4151 4152 4153 4154 4155 4156 4157 4158 4159 4160 4161 4162 4163 4164 4165 4166 4167 4168 4169 4170 4171 4172 4173 4174 4175 4176 4177 4178 4179 4180 4181 4182 4183 4184 4185 4186 4187 4188 4189 4190 4191 4192 4193 4194 4195 4196 4197 4198 4199 4200 4201 4202 4203 4204 4205 4206 4207 4208 4209 4210 4211 4212 4213 4214 4215 4216 4217 4218 4219 4220 4221 4222 4223 4224 4225 4226 4227 4228 4229 4230 4231 4232 4233 4234 4235 4236 4237 4238 4239 4240 4241 4242 4243 4244 4245 4246 4247 4248 4249 4250 4251 4252 4253 4254 4255 4256 4257 4258 4259 4260 4261 4262 4263 4264 4265 4266 4267 4268 4269 4270 4271 4272 4273 4274 4275 4276 4277 4278 4279 4280 4281 4282 4283 4284 4285 4286 4287 4288 4289 4290 4291 4292 4293 4294 4295 4296 4297 4298 4299 4300 4301 4302 4303 4304 4305 4306 4307 4308 4309 4310 4311 4312 4313 4314 4315 4316 4317 4318 4319 4320 4321 4322 4323 4324 4325 4326 4327 4328 4329 4330 4331 4332 4333 4334 4335 4336 4337 4338 4339 4340 4341 4342 4343 4344 4345 4346 4347 4348 4349 4350 4351 4352 4353 4354 4355 4356 4357 4358 4359 4360 4361 4362 4363 4364 4365 4366 4367 4368 4369 4370 4371 4372 4373 4374 4375 4376 4377 4378 4379 4380 4381 4382 4383 4384 4385 4386 4387 4388 4389 4390 4391 4392 4393 4394 4395 4396 4397 4398 4399 4400 4401 4402 4403 4404 4405 4406 4407 4408 4409 4410 4411 4412 4413 4414 4415 4416 4417 4418 4419 4420 4421 4422 4423 4424 4425 4426 4427 4428 4429 4430 4431 4432 4433 4434 4435 4436 4437 4438 4439 4440 4441 4442 4443 4444 4445 4446 4447 4448 4449 4450 4451 4452 4453 4454 4455 4456 4457 4458 4459 4460 4461 4462 4463 4464 4465 4466 4467 4468 4469 4470 4471 4472 4473 4474 4475 4476 4477 4478 4479 4480 4481 4482 4483 4484 4485 4486 4487 4488 4489 4490 4491 4492 4493 4494 4495 4496 4497 4498 4499 4500 4501 4502 4503 4504 4505 4506 4507 4508 4509 4510 4511 4512 4513 4514 4515 4516 4517 4518 4519 4520 4521 4522 4523 4524 4525 4526 4527 4528 4529 4530 4531 4532 4533 4534 4535 4536 4537 4538 4539 4540 4541 4542 4543 4544 4545 4546 4547 4548 4549 4550 4551 4552 4553 4554 4555 4556 4557 4558 4559 4560 4561 4562 4563 4564 4565 4566 4567 4568 4569 4570 4571 4572 4573 4574 4575 4576 4577 4578 4579 4580 4581 4582 4583 4584 4585 4586 4587 4588 4589 4590 4591 4592 4593 4594 4595 4596 4597 4598 4599 4600 4601 4602 4603 4604 4605 4606 4607 4608 4609 4610 4611 4612 4613 4614 4615 4616 4617 4618 4619 4620 4621 4622 4623 4624 4625 4626 4627 4628 4629 4630 4631 4632 4633 4634 4635 4636 4637 4638 4639 4640 4641 4642 4643 4644 4645 4646 4647 4648 4649 4650 4651 4652 4653 4654 4655 4656 4657 4658 4659 4660 4661 4662 4663 4664 4665 4666 4667 4668 4669 4670 4671 4672 4673 4674 4675 4676 4677 4678 4679 4680 4681 4682 4683 4684 4685 4686 4687 4688 4689 4690 4691 4692 4693 4694 4695 4696 4697 4698 4699 4700 4701 4702 4703 4704 4705 4706 4707 4708 4709 4710 4711 4712 4713 4714 4715 4716 4717 4718 4719 4720 4721 4722 4723 4724 4725 4726 4727 4728 4729 4730 4731 4732 4733 4734 4735 4736 4737 4738 4739 4740 4741 4742 4743 4744 4745 4746 4747 4748 4749 4750 4751 4752 4753 4754 4755 4756 4757 4758 4759 4760 4761 4762 4763 4764 4765 4766 4767 4768 4769 4770 4771 4772 4773 4774 4775 4776 4777 4778 4779 4780 4781 4782 4783 4784 4785 4786 4787 4788 4789 4790 4791 4792 4793 4794 4795 4796 4797 4798 4799 4800 4801 4802 4803 4804 4805 4806 4807 4808 4809 4810 4811 4812 4813 4814 4815 4816 4817 4818 4819 4820 4821 4822 4823 4824 4825 4826 4827 4828 4829 4830 4831 4832 4833 4834 4835 4836 4837 4838 4839 4840 4841 4842 4843 4844 4845 4846 4847 4848 4849 4850 4851 4852 4853 4854 4855 4856 4857 4858 4859 4860 4861 4862 4863 4864 4865 4866 4867 4868 4869 4870 4871 4872 4873 4874 4875 4876 4877 4878 4879 4880 4881 4882 4883 4884 4885 4886 4887 4888 4889 4890 4891 4892 4893 4894 4895 4896 4897 4898 4899 4900 4901 4902 4903 4904 4905 4906 4907 4908 4909 4910 4911 4912 4913 4914 4915 4916 4917 4918 4919 4920 4921 4922 4923 4924 4925 4926 4927 4928 4929 4930 4931 4932 4933 4934 4935 4936 4937 4938 4939 4940 4941 4942 4943 4944 4945 4946 4947 4948 4949 4950 4951 4952 4953 4954 4955 4956 4957 4958 4959 4960 4961 4962 4963 4964 4965 4966 4967 4968 4969 4970 4971 4972 4973 4974 4975 4976 4977 4978 4979 4980 4981 4982 4983 4984 4985 4986 4987 4988 4989 4990 4991 4992 4993 4994 4995 4996 4997 4998 4999 5000 5001 5002 5003 5004 5005 5006 5007 5008 5009 5010 5011 5012 5013 5014 5015 5016 5017 5018 5019 5020 5021 5022 5023 5024 5025 5026 5027 5028 5029 5030 5031 5032 5033 5034 5035 5036 5037 5038 5039 5040 5041 5042 5043 5044 5045 5046 5047 5048 5049 5050 5051 5052 5053 5054 5055 5056 5057 5058 5059 5060 5061 5062 5063 5064 5065 5066 5067 5068 5069 5070 5071 5072 5073 5074 5075 5076 5077 5078 5079 5080 5081 5082 5083 5084 5085 5086 5087 5088 5089 5090 5091 5092 5093 5094 5095 5096 5097 5098 5099 5100 5101 5102 5103 5104 5105 5106 5107 5108 5109 5110 5111 5112 5113 5114 5115 5116 5117 5118 5119 5120 5121 5122 5123 5124 5125 5126 5127 5128 5129 5130 5131 5132 5133 5134 5135 5136 5137 5138 5139 5140 5141 5142 5143 5144 5145 5146 5147 5148 5149 5150 5151 5152 5153 5154 5155 5156 5157 5158 5159 5160 5161 5162 5163 5164 5165 5166 5167 5168 5169 5170 5171 5172 5173 5174 5175 5176 5177 5178 5179 5180 5181 5182 5183 5184 5185 5186 5187 5188 5189 5190 5191 5192 5193 5194 5195 5196 5197 5198 5199 5200 5201 5202 5203 5204 5205 5206 5207 5208 5209 5210 5211 5212 5213 5214 5215 5216 5217 5218 5219 5220 5221 5222 5223 5224 5225 5226 5227 5228 5229 5230 5231 5232 5233 5234 5235 5236 5237 5238 5239 5240 5241 5242 5243 5244 5245 5246 5247 5248 5249 5250 5251 5252 5253 5254 5255 5256 5257 5258 5259 5260 5261 5262 5263 5264 5265 5266 5267 5268 5269 5270 5271 5272 5273 5274 5275 5276 5277 5278 5279 5280 5281 5282 5283 5284 5285 5286 5287 5288 5289 5290 5291 5292 5293 5294 5295 5296 5297 5298 5299 5300 5301 5302 5303 5304 5305 5306 5307 5308 5309 5310 5311 5312 5313 5314 5315 5316 5317 5318 5319 5320 5321 5322 5323 5324 5325 5326 5327 5328 5329 5330 5331 5332 5333 5334 5335 5336 5337 5338 5339 5340 5341 5342 5343 5344 5345 5346 5347 5348 5349 5350 5351 5352 5353 5354 5355 5356 5357 5358 5359 5360 5361 5362 5363 5364 5365 5366 5367 5368 5369 5370 5371 5372 5373 5374 5375 5376 5377 5378 5379 5380 5381 5382 5383 5384 5385 5386 5387 5388 5389 5390 5391 5392 5393 5394 5395 5396 5397 5398 5399 5400 5401 5402 5403 5404 5405 5406 5407 5408 5409 5410 5411 5412 5413 5414 5415 5416 5417 5418 5419 5420 5421 5422 5423 5424 5425 5426 5427 5428 5429 5430 5431 5432 5433 5434 5435 5436 5437 5438 5439 5440 5441 5442 5443 5444 5445 5446 5447 5448 5449 5450 5451 5452 5453 5454 5455 5456 5457 5458 5459 5460 5461 5462 5463 5464 5465 5466 5467 5468 5469 5470 5471 5472 5473 5474 5475 5476 5477 5478 5479 5480 5481 5482 5483 5484 5485 5486 5487 5488 5489 5490 5491 5492 5493 5494 5495 5496 5497 5498 5499 5500 5501 5502 5503 5504 5505 5506 5507 5508 5509 5510 5511 5512 5513 5514 5515 5516 5517 5518 5519 5520 5521 5522 5523 5524 5525 5526 5527 5528 5529 5530 5531 5532 5533 5534 5535 5536 5537 5538 5539 5540 5541 5542 5543 5544 5545 5546 5547 5548 5549 5550 5551 5552 5553 5554 5555 5556 5557 5558 5559 5560 5561 5562 5563 5564 5565 5566 5567 5568 5569 5570 5571 5572 5573 5574 5575 5576 5577 5578 5579 5580 5581 5582 5583 5584 5585 5586 5587 5588 5589 5590 5591 5592 5593 5594 5595 5596 5597 5598 5599 5600 5601 5602 5603 5604 5605 5606 5607 5608 5609 5610 5611 5612 5613 5614 5615 5616 5617 5618 5619 5620 5621 5622 5623 5624 5625 5626 5627 5628 5629 5630 5631 5632 5633 5634 5635 5636 5637 5638 5639 5640 5641 5642 5643 5644 5645 5646 5647 5648 5649 5650 5651 5652 5653 5654 5655 5656 5657 5658 5659 5660 5661 5662 5663 5664 5665 5666 5667 5668 5669 5670 5671 5672 5673 5674 5675 5676 5677 5678 5679 5680 5681 5682 5683 5684 5685 5686 5687 5688 5689 5690 5691 5692 5693 5694 5695 5696 5697 5698 5699 5700 5701 5702 5703 5704 5705 5706 5707 5708 5709 5710 5711 5712 5713 5714 5715 5716 5717 5718 5719 5720 5721 5722 5723 5724 5725 5726 5727 5728 5729 5730 5731 5732 5733 5734 5735 5736 5737 5738 5739 5740 5741 5742 5743 5744 5745 5746 5747 5748 5749 5750 5751 5752 5753 5754 5755 5756 5757 5758 5759 5760 5761 5762 5763 5764 5765 5766 5767 5768 5769 5770 5771 5772 5773 5774 5775 5776 5777 5778 5779 5780 5781 5782 5783 5784 5785 5786 5787 5788 5789 5790 5791 5792 5793 5794 5795 5796 5797 5798 5799 5800 5801 5802 5803 5804 5805 5806 5807 5808 5809 5810 5811 5812 5813 5814 5815 5816 5817 5818 5819 5820 5821 5822 5823 5824 5825 5826 5827 5828 5829 5830 5831 5832 5833 5834 5835 5836 5837 5838 5839 5840 5841 5842 5843 5844 5845 5846 5847 5848 5849 5850 5851 5852 5853 5854 5855 5856 5857 5858 5859 5860 5861 5862 5863 5864 5865 5866 5867 5868 5869 5870 5871 5872 5873 5874 5875 5876 5877 5878 5879 5880 5881 5882 5883 5884 5885 5886 5887 5888 5889 5890 5891 5892 5893 5894 5895 5896 5897 5898 5899 5900 5901 5902 5903 5904 5905 5906 5907 5908 5909 5910 5911 5912 5913 5914 5915 5916 5917 5918 5919 5920 5921 5922 5923 5924 5925 5926 5927 5928 5929 5930 5931 5932 5933 5934 5935 5936 5937 5938 5939 5940 5941 5942 5943 5944 5945 5946 5947 5948 5949 5950 5951 5952 5953 5954 5955 5956 5957 5958 5959 5960 5961 5962 5963 5964 5965 5966 5967 5968 5969 5970 5971 5972 5973 5974 5975 5976 5977 5978 5979 5980 5981 5982 5983 5984 5985 5986 5987 5988 5989 5990 5991 5992 5993 5994 5995 5996 5997 5998 5999 6000 6001 6002 6003 6004 6005 6006 6007 6008 6009 6010 6011 6012 6013 6014 6015 6016 6017 6018 6019 6020 6021 6022 6023 6024 6025 6026 6027 6028 6029 6030 6031 6032 6033 6034 6035 6036 6037 6038 6039 6040 6041 6042 6043 6044 6045 6046 6047 6048 6049 6050 6051 6052 6053 6054 6055 6056 6057 6058 6059 6060 6061 6062 6063 6064 6065 6066 6067 6068 6069 6070 6071 6072 6073 6074 6075 6076 6077 6078 6079 6080 6081 6082 6083 6084 6085 6086 6087 6088 6089 6090 6091 6092 6093 6094 6095 6096 6097 6098 6099 6100 6101 6102 6103 6104 6105 6106 6107 6108 6109 6110 6111 6112 6113 6114 6115 6116 6117 6118 6119 6120 6121 6122 6123 6124 6125 6126 6127 6128 6129 6130 6131 6132 6133 6134 6135 6136 6137 6138 6139 6140 6141 6142 6143 6144 6145 6146 6147 6148 6149 6150 6151 6152 6153 6154 6155 6156 6157 6158 6159 6160 6161 6162 6163 6164 6165 6166 6167 6168 6169 6170 6171 6172 6173 6174 6175 6176 6177 6178 6179 6180 6181 6182 6183 6184 6185 6186 6187 6188 6189 6190 6191 6192 6193 6194 6195 6196 6197 6198 6199 6200 6201 6202 6203 6204 6205 6206 6207 6208 6209 6210 6211 6212 6213 6214 6215 6216 6217 6218 6219 6220 6221 6222 6223 6224 6225 6226 6227 6228 6229 6230 6231 6232 6233 6234 6235 6236 6237 6238 6239 6240 6241 6242 6243 6244 6245 6246 6247 6248 6249 6250 6251 6252 6253 6254 6255 6256 6257 6258 6259 6260 6261 6262 6263 6264 6265 6266 6267 6268 6269 6270 6271 6272 6273 6274 6275 6276 6277 6278 6279 6280 6281 6282 6283 6284 6285 6286 6287 6288 6289 6290 6291 6292 6293 6294 6295 6296 6297 6298 6299 6300 6301 6302 6303 6304 6305 6306 6307 6308 6309 6310 6311 6312 6313 6314 6315 6316 6317 6318 6319 6320 6321 6322 6323 6324 6325 6326 6327 6328 6329 6330 6331 6332 6333 6334 6335 6336 6337 6338 6339 6340 6341 6342 6343 6344 6345 6346 6347 6348 6349 6350 6351 6352 6353 6354 6355 6356 6357 6358 6359 6360 6361 6362 6363 6364 6365 6366 6367 6368 6369 6370 6371 6372 6373 6374 6375 6376 6377 6378 6379 6380 6381 6382 6383 6384 6385 6386 6387 6388 6389 6390 6391 6392 6393 6394 6395 6396 6397 6398 6399

; 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.
(inpackage "ACL2")
; A quick sketch of the three main functions here
; We renamed these functions because their nqthm names were confusing to
; one of us.
; ACL2 Nqthm
; simplifyclause SIMPLIFYCLAUSE
; simplifyclause1 SIMPLIFYCLAUSE0
; rewriteclause SIMPLIFYCLAUSE1
; Simplifyclause is the toplevel clause simplifier but it does
; relatively little work. It merely determines what to expand and
; what not to, taking into account induction as described in comments
; in simplifyclause. The real workhorse of simplifyclause is its
; subroutine, simplifyclause1.
; Simplifyclause1 is nonrecursive. It does an enormous amount of
; clause level work: removing trivial equations, detecting
; propositional tautologies with typeset, setting up the
; simplifyclausepotlst for the later literalbyliteralrewriting,
; detecting linear arithmetic tautologies, and retrieving useful
; equalities from the linear arithmetic potlst. Once all that has
; happened, it calls rewriteclause which begins the classic sweep of
; the clause rewriting each literal.
; Rewriteclause is concerned only with rewriting the literals of a
; clause. It does not do any clause level work aside from that
; necessary to avoid tail biting. It rewrites each lit in turn,
; clausifies the result into a bunch of segments and splices them into
; the evolving set of answers.
; In this section we develop rewriteclause.
(defun dumbnegatelitlst (lst)
(cond ((null lst) nil)
(t (cons (dumbnegatelit (car lst))
(dumbnegatelitlst (cdr lst))))))
; Note: The following two functions are no longer called. The were
; called before we made typeset track dependencies. However, after
; that change, we found the burden of passing up the ttrees generated
; below to be so offputting that we eliminated their calls in favor
; of dumbnegatelit and a noop. It is our belief that these changes
; do not seriously weaken the system. Comments indicating the changes
; contain calls of the two functions so these decisions can be
; reconsidered.
(defun negatelit (term typealist ens forceflg wrld)
; This function returns a term equivalent to (not term) under the
; given typealist and wrld. It also returns a ttree justifying this
; result.
; Note Added After This Function Became Obsolete: Because
; knownwhethernil now may generate 'assumptions, negatelit may
; generate 'assumptions. Thus, use of this function is even more
; problematic since the ttrees not only must be tracked but the
; necessary case splits done.
(mvlet (knownp nilp ttree)
(knownwhethernil term typealist ens forceflg wrld nil)
(cond (knownp
(cond (nilp (mv *t* ttree))
(t (mv *nil* ttree))))
(t (mv (dumbnegatelit term) nil)))))
(defun pegatelit (term typealist ens forceflg wrld)
; Like negatelit but returns a term equivalent to term, and a ttree.
; Note Added After This Function Became Obsolete: Because
; knownwhethernil now may generate 'assumptions, negatelit may
; generate 'assumptions. Thus, use of this function is even more
; problematic since the ttrees not only must be tracked but the
; necessary case splits done.
(mvlet (knownp nilp ttree)
(knownwhethernil term typealist ens forceflg wrld nil)
(cond (knownp
(cond (nilp (mv *nil* ttree))
(t (mv *t* ttree))))
(t (mv term nil)))))
; Rockwell Addition: Now we know harderror returns nil too.
(defun addliteral (lit cl atendflg)
; We add lit to clause cl, optionally at the end as per the flag.
; We assume that lit has been subjected to rewriting modulo the geneqv
; iff. Therefore, though we check lit against *t* and *nil* we do
; not do more powerful typeset reasoning. In addition, we know that
; (harderror ctx str alist) is logically nil.
(cond ((quotep lit)
(cond ((equal lit *nil*) cl)
(t *trueclause*)))
((equal cl *trueclause*) *trueclause*)
((membercomplementterm lit cl) *trueclause*)
((variablep lit)
(cond ((memberterm lit cl) cl)
(atendflg (append cl (list lit)))
(t (cons lit cl))))
; Now we can take the ffnsymb of lit.
((eq (ffnsymb lit) 'harderror)
; (Harderror ctx str alist) = nil.
cl)
((and (eq (ffnsymb lit) 'rationalp)
(membercomplementterm1 (fconsterm 'integerp (fargs lit))
cl))
*trueclause*)
((and (eq (ffnsymb lit) 'not)
(nvariablep (fargn lit 1))
(not (fquotep (fargn lit 1)))
(eq (ffnsymb (fargn lit 1)) 'integerp)
(memberequal (fconsterm 'rationalp (fargs (fargn lit 1))) cl))
*trueclause*)
((memberterm lit cl) cl)
(atendflg (append cl (list lit)))
(t (cons lit cl))))
(defun addeachliteral (cl)
(cond ((null cl) nil)
(t (addliteral (car cl)
(addeachliteral (cdr cl))
nil))))
(mutualrecursion
(defun subsumesrec (count cl1 cl2 alist)
; Keep this nest in sync with the subsumes!rec nest, which is similar except
; that there is no restriction (count) on the number of onewayunify1 calls.
; We return a positive or negative integer, according to whether or not
; (respectively) some instance of cl1 via an extension of alist is a subset of
; clause cl2. In either case, the absolute value n of that integer is at most
; count, and ( count n) is the number of onewayunify1 calls that were made.
; Otherwise we return 0, indicating that we could not determine subsumption
; using fewer than count such calls.
; Here is why subsumesrec and subsumes1 take a "count" argument to limit the
; number of calls:
; Note that in the worst case, checking whether clause2 of length len2 is an
; instance of clause1 of length len1 is roughly on the order of len2^len1. For
; suppose every term in each clause is (integerp x) for a distinct x, except
; that the last term in the first clause is not a match for any member of the
; second clause. Then each (integerp x) in clause1 can be matched against any
; (integerp y) in clause2, so we have len2*len2*...*len2, len11 times.
(declare (type (signedbyte 29) count))
(the (signedbyte 29)
(cond ((eql count 0) 0)
((null cl1) count)
(t (subsumes1 count (car cl1) (cdr cl1) cl2 cl2 alist)))))
(defun subsumes1 (count lit tl1 tl2 cl2 alist)
; Keep this nest in sync with the subsumes!rec nest, which is similar except
; that there is no restriction (count) on the number of onewayunify1 calls.
; If we can extend alist to an alist1 so that lit/alist1 is a member of tl2 and
; tl1/alist1 is a subset of cl2, we return a positive integer obtained by
; decreasing count by the number of onewayunify1 calls. If we determine that
; there is no such alist, we return a negative integer whose absolute value is
; obtained by decreasing count as above. But, if the number of onewayunify1
; calls necessary is not less than count, we return 0.
(declare (type (signedbyte 29) count))
(the (signedbyte 29)
(cond ((eql count 0) 0)
((null tl2) (f count))
(t (mvlet
(wonp alist1)
(onewayunify1 lit (car tl2) alist)
(cond
((not wonp)
(subsumes1 (1f count) lit tl1 (cdr tl2) cl2 alist))
(t
(let ((newcount (subsumesrec (1f count) tl1 cl2 alist1)))
(declare (type (signedbyte 29) newcount))
(cond ((<= 0 newcount) newcount)
(t (subsumes1 (f newcount) lit tl1 (cdr tl2) cl2
alist)))))))))))
)
(mutualrecursion
(defun subsumes!rec (cl1 cl2 alist)
; Keep this nest in sync with the subsumes1 nest, which is similar except that
; there is a restriction (count) on the number of onewayunify1 calls.
; We return t if some instance of cl1 via an extension of alist is a subset of
; clause cl2, otherwise nil.
(cond ((null cl1) t)
(t (subsumes!1 (car cl1) (cdr cl1) cl2 cl2 alist))))
(defun subsumes!1 (lit tl1 tl2 cl2 alist)
; Keep this nest in sync with the subsumes1 nest, which is similar except that
; there is a restriction (count) on the number of onewayunify1 calls.
; If we can extend alist to an alist1 so that lit/alist1 is a member of tl2 and
; tl1/alist1 is a subset of cl2, we return t; otherwise, nil.
(cond ((null tl2) nil)
(t (mvlet
(wonp alist1)
(onewayunify1 lit (car tl2) alist)
(cond ((and wonp (subsumes!rec tl1 cl2 alist1))
t)
(t (subsumes!1 lit tl1 (cdr tl2) cl2 alist)))))))
)
(defconst *initsubsumescount*
(the (signedbyte 29)
; The following value is rather arbitrary, determined by experimentation so
; that subsumes doesn't run for more than a small fraction of a second on a
; 2.6GH P4 (depending on the underlying Lisp). The following takes about 0.04
; seconds to return '? (signalling that we have done 1,000,000 calls of
; onewayunify1) on that machine using GCL 2.6.7 and about 0.17 seconds using
; Allegro CL 7.0.
; (subsumes 1000000
; '((integerp x1) (integerp x2) (integerp x3) (integerp x4)
; (integerp x5) (integerp x6) (integerp x7) (integerp x8)
; (foo a))
; '((integerp x1) (integerp x2) (integerp x3) (integerp x4)
; (integerp x5) (integerp x6) (integerp x7) (integerp x8))
; nil)
1000000))
(defun subsumes (initsubsumescount cl1 cl2 alist)
; If initsubsumescount is not nil, then it is a nonnegative integer
; specifying a strict upper bound on the number of onewayunify1 calls. See
; the comment in subsumesrec for an explanation of why we may want this bound.
; If the return value is t, then we can extend alist to a substitution s such
; that cl1/s is a subset of cl2. If the return value is nil, then we cannot
; thus extend alist. Otherwise (only possible if initsubsumescount is not
; nil), the return value is '?, in which case we could not make such a
; determination with fewer than initsubsumescount onewayunify1 calls.
(cond
((timelimit4reachedp "Out of time in subsumes.") ; nil, or throws
nil)
((null initsubsumescount)
(subsumes!rec cl1 cl2 alist))
(t (let ((temp (subsumesrec initsubsumescount cl1 cl2 alist)))
(cond ((eql temp 0)
'?)
(t (< 0 temp)))))))
(defun somemembersubsumes (initsubsumescount clset cl acc)
; Returns t if some member of clset subsumes cl, acc if no member of clset
; subsumes cl, and '? (only possible if initsubsumescount is nonnil) if we
; don't know.
(cond ((null clset) acc)
(t (let ((temp (subsumes initsubsumescount (car clset) cl nil)))
(cond
((eq temp t))
(t (somemembersubsumes initsubsumescount (cdr clset) cl
(or temp acc))))))))
(defun conjoinclausetoclauseset (cl clset)
; Once upon a time, in particular, in the two weeks before January 25,
; 1990, we did a subsumption check here. The idea was that if cl was
; subsumed by some member of clset, don't add it and if it subsumes
; some member of clset, delete that member. That caused unsoundness.
; The reason is that clset is not a set of clauses that is
; necessarily going to be proved. For example, clset may contain a
; collection of clause segments to which we will eventually add some
; additional hypotheses. If clset contains the clause segment ((P
; I)) and then we conjoin the clause segment ((P (F X))) to it, we
; don't want the first segment to subsume the second because we may
; eventually add the additional hypothesis (INTEGERP I) to all the
; segments.
(cond ((memberequal *t* cl) clset)
((memberequal cl clset) clset)
(t (cons cl clset))))
(defun addeachliterallst (clset)
(cond ((null clset) nil)
(t (conjoinclausetoclauseset
(addeachliteral (car clset))
(addeachliterallst (cdr clset))))))
(defun conjoinclausesets (clset1 clset2)
(cond ((null clset1) clset2)
(t (conjoinclausetoclauseset
(car clset1)
(conjoinclausesets (cdr clset1) clset2)))))
(defun someelementmembercomplementterm (lst1 lst2)
(cond ((null lst1) nil)
((membercomplementterm (car lst1) lst2) t)
(t (someelementmembercomplementterm (cdr lst1) lst2))))
; Rockwell Addition: We used to just stick them together. Now we add
; each literal to catch cases like harderror.
(defun disjoinclauses1 (cl1 cl2)
; This is equivalent to (append cl1 (setdifferenceequal cl2 cl1))
; except that we add each literal with addliteral to check for
; complementary pairs, etc.
; Note: This function repeatedly adds literals from cl2 to cl1, at the
; end. So it copies cl1's spine as many times as there are literals
; to add. We used to use the append formulation above but found that
; complementary pairs were being missed once we extended the notion of
; complementary to include rational v integer.
(cond ((endp cl2) cl1)
(t (disjoinclauses1 (addliteral (car cl2) cl1 t)
(cdr cl2)))))
(defun disjoinclauses (cl1 cl2)
(cond ((or (equal cl1 *trueclause*)
(equal cl2 *trueclause*))
*trueclause*)
((null cl1) cl2)
((null cl2) cl1)
(t (disjoinclauses1 cl1 cl2))))
(defun disjoinclausesegmentstoclause (segments cl)
(cond ((null segments) nil)
(t (conjoinclausetoclauseset
(disjoinclauses (car segments) cl)
(disjoinclausesegmentstoclause (cdr segments) cl)))))
# ; See comment in disjoinclausesegmenttoclauseset.
(defun disjoinclausesegmenttoclausesetrec (segment clset acc)
(cond ((null clset) acc)
(t (disjoinclausesegmenttoclausesetrec
segment
(cdr clset)
(conjoinclausetoclauseset
(disjoinclauses segment (car clset))
acc)))))
#
(defun disjoinclausesegmenttoclauseset (segment clset)
; This code is not tailrecursive, but it could be. At one time it caused
; stack overflow problems in Lispworks 4.2.0. Below is some alternate code,
; with a reverse call in order to provide unchanged functionality. Would we
; gain efficiency by eliminating tail recursion at the cost of that reverse
; call? Maybe. A clearer win would be to avoid the reverse call, which should
; be logically OK but could change the prover's behavior, thus invaliding huge
; portions of the regression suite.
; The alternate code is simply the following line, in place of all that
; follows:
; (disjoinclausesegmenttoclausesetrec segment (reverse clset) nil)
(cond ((null clset) nil)
(t (conjoinclausetoclauseset
(disjoinclauses segment (car clset))
(disjoinclausesegmenttoclauseset segment (cdr clset))))))
(defun splitonassumptions (assumptions cl ans)
; Cl is a clause and ans is a set of clauses that will be our answer.
; Assumptions is a list of literals. For each lit in assumptions
; we add a new clause to ans, obtained by adding lit to cl.
(cond ((null assumptions) ans)
(t (splitonassumptions
(cdr assumptions)
cl
(conjoinclausetoclauseset
(addliteral (car assumptions) cl nil)
ans)))))
(defun rewriteclauseaction (lit branches)
; Lit is a term. Branches is the result of clausifying the result of
; rewriting lit. We want to know if anything has happened. The table
; below indicates our result:
; branches result meaning
; {} 'showntrue Lit was rewritten and clausified to
; the empty set, i.e., lit is T under our
; assumptions.
; {NIL} 'shownfalse Lit was rewritten and clausified to
; the set containing the empty clause, i.e.,
; lit is NIL under our assumptions.
; {{lit}} 'nochange Neither rewrite nor clausify did anything.
; otherwise 'change
(cond ((consp branches)
(cond ((null (cdr branches))
(cond ((null (car branches))
'shownfalse)
((and (null (cdr (car branches)))
(equal lit (car (car branches))))
'nochange)
(t 'change)))
(t 'change)))
(t 'showntrue)))
; Forward Chaining
; ACL2 implements a rudimentary form of forward chaining  though it
; is getting less rudimentary as time goes on! It sits at the
; toplevel of clause simplification. Before we begin to rewrite the
; literals of a clause, in the same place we set up the
; simplifyclausepotlst, we forward chain from the negations of the
; literals of the clause and construct a list of all the
; (heuristically approved) conclusions we can derive. Each concl is
; paired with a tree that contains the 'lemma and 'pt dependencies.
; That list of pairs is passed down to the rewriteclause level, where
; it is used to augment the typealist before rewriting any given
; literal.
; This is the third version of forward chaining. For an extensive
; comment on version II, see the historical plaque after the definition
; of forwardchain.
; A forward chaining rule is
(defrec forwardchainingrule
((rune . nume) trigger hyps concls . matchfree) nil)
; One of the main inefficiencies in our earlier forward chaining schemes
; was that if a rule began to fire but misfired because some hyp could
; not be relieved, we would reconsider firing it later and redo the work
; associated with the misfire. We avoid that by storing what we call a
; "forward chaining activation" record which permits us to suspend the
; attempt to fire a rule and resume it later.
(defrec fcactivation
(insthyp (hyps . ttree)
unifysubst insttrigger . rule) t)
; Warning: If you reorder the fields recode suspendfcactivation, which
; exploits the layout to conserve conses when modifying instances.
; An fcactivation represents an attempt to apply the given
; forwardchainingrule. Suppose a term of interest unifies with the
; trigger term of some rule. Then we try to relieve the hypotheses of
; that rule, using the current set of assumptions. Imagine that we
; relieve all those up to but not including hypn, producing an extended
; unify substitution and a ttree recording the dependencies. But then we
; learn that hypn is not yet definitely nil or definitely nonnil. Since
; the list of assumptions is growing, we may be able eventually to
; establish hypn. Therefore, instead of just quitting and starting over
; we suspend the attempted application of rule by producing an
; fcactivation record that records our current state.
; The current unifysubst, ttree and rule are stored in the slots of
; those names. The insttrigger is the term in the current problem
; that fired this rule. What about insthyps and hyps? What do they
; hold? There are two cases of interest: either hypn  the hyp we
; are trying to establish  contains free variables under unifysubst
; or it does not. If it does, then in the fcactivation, insthyp is
; *t* and hyps is the cdr of the hyps of the rule that starts with
; hypn. If it does not, then insthyp is hypn/unifysubst and hyps is
; the cdr of the rule that starts immediately after hypn. (Because we
; make an activation simply to begin processing a rule, there is the
; unusual case in which the rule has no hyps. In that case, insthyp
; is *t* and hyps is nil.)
(defun fcactivation (term rule ttree forceflg ens)
; If rule is enabled and the trigger of rule can be instantiated with some
; substitution unifysubst to be term, then we make an fcactivation for this
; pair, otherwise we return nil.
; The initial ttree of the activation is ttree. When we are building an
; activation for a term in the initial clause, this ttree will be nil. When we
; are building an activation for a term derived by some fc derivation, the
; ttree will contain just that 'fcderivation. The presence of that derivation
; in this activation will mean that the conclusion we eventually derive cannot
; be worse than the conclusion of the derivation from which this term sprang.
; Once upon a time this function did not take the ttree arg and just used nil.
; But that gave rise to infinite loops that were not stopped by our worsethan
; hacks because the terms from which the bad terms were derived were not
; logically dependent on their parents.
(cond ((not (enablednumep (access forwardchainingrule rule :nume)
ens))
nil)
(t
(mvlet (unifyans unifysubst)
(onewayunify (access forwardchainingrule rule :trigger)
term)
; Note: We do not start accumulating the persistence of this rule until we
; advance the fcactivation we create below.
(cond ((null unifyans) nil)
(t (let ((rulehyps
(access forwardchainingrule rule :hyps)))
(cond ((or (null rulehyps)
(freevarsp (car rulehyps)
unifysubst)
(and (nvariablep (car rulehyps))
(not (fquotep (car rulehyps)))
(or (eq (ffnsymb (car rulehyps))
'force)
(eq (ffnsymb (car rulehyps))
'casesplit))
forceflg))
(make fcactivation
:insthyp *t*
:hyps rulehyps
:ttree ttree
:unifysubst unifysubst
:insttrigger term
:rule rule))
(t (make fcactivation
:insthyp
(sublisvar unifysubst
(car rulehyps))
:hyps (cdr rulehyps)
:ttree ttree
:unifysubst unifysubst
:insttrigger term
:rule rule))))))))))
(defun fcactivationlst (term rulelst ttree forceflg ens)
; We create a list of all the possible forward chaining activations for
; term.
(cond ((null rulelst) nil)
(t (let ((act
(fcactivation term (car rulelst) ttree forceflg ens))
(rst
(fcactivationlst term (cdr rulelst) ttree forceflg ens)))
(if act (cons act rst) rst)))))
; A basic data structure of the forward chaining process is what we
; call the fcpotlst. It is a structure that enumerates all of the
; subterms of the current problem  the clause and all our derived
; conclusions  that have any forward chaining rules at all together
; with their still suspended fcactivations. It is important that the
; list include every term that has rules, even if the rules give rise
; to no activations. If we omitted a subterm because it gave rise to
; no activations then every time we generated a new subterm we would
; have to scan its rules to see if it permits any activations. Rather
; than do that, we keep all possible activations (even the empty list)
; and then only note that the subterm is not new.
(mutualrecursion
(defun addnewfcpots (term ttree forceflg wrld ens fcpotlst)
; A term consed onto the list of all fc activations for the term is
; called an "fc pot". We sweep term looking for every subterm of the
; form (fn ...) where fn is not a lambda or NOT and has at least one
; forwardchainingrule associated with it. We add an fc pot for each
; such subterm to fcpotlst.
(cond ((variablep term) fcpotlst)
((fquotep term) fcpotlst)
((flambdaapplicationp term)
(addnewfcpots (lambdabody (ffnsymb term))
ttree forceflg wrld ens
(addnewfcpotslst (fargs term)
ttree forceflg wrld ens
fcpotlst)))
((eq (ffnsymb term) 'not)
; Because some of the NOTs in clauses are not really present, we think it
; is confusing to allow a NOT to trigger a forward chaining.
(addnewfcpots (fargn term 1) ttree forceflg wrld ens fcpotlst))
((assocequal term fcpotlst) fcpotlst)
(t (let ((fcpotlst (addnewfcpotslst (fargs term)
ttree forceflg wrld ens
fcpotlst))
(rules (getprop (ffnsymb term)
'forwardchainingrules
nil
'currentacl2world
wrld)))
(cond ((null rules) fcpotlst)
(t
(cons (cons term
(fcactivationlst term
rules
ttree
forceflg
ens))
fcpotlst)))))))
(defun addnewfcpotslst (termlst ttree forceflg wrld ens fcpotlst)
(cond ((null termlst) fcpotlst)
(t (addnewfcpotslst (cdr termlst)
ttree forceflg wrld ens
(addnewfcpots (car termlst)
ttree forceflg wrld ens
fcpotlst)))))
)
(defun addnewfcpotslstlst
(termlst ttreelst forceflg wrld ens fcpotlst)
(cond ((null termlst) fcpotlst)
(t (addnewfcpotslstlst
(cdr termlst)
(cdr ttreelst)
forceflg wrld ens
(addnewfcpots (car termlst)
(car ttreelst)
forceflg wrld ens
fcpotlst)))))
; The above functions let us create a list of fcpots, each pot
; containing a list of activations. We now develop the code to fire up
; an activation and (a) derive a new conclusion, (b) abort and abandon
; the activation, or (c) replace it by a modified activation after
; possibly relieving some but not all of the hyps.
(defun suspendfcactivation (act insthyp hyps unifysubst ttree)
; This function is equivalent to
; (change fcactivation act
; :insthyp insthyp
; :hyps hyps
; :unifysubst unifysubst
; :ttree ttree)
; i.e., change all the fields but :insttrigger and :rule. But this
; function sometimes does fewer conses. The cases it tries to
; optimize are based on knowledge of how we change certain fields, but
; the correctness of its answer is independent of usage.
(cond ((equal unifysubst (access fcactivation act :unifysubst))
(cond ((and (equal hyps (access fcactivation act :hyps))
(equal insthyp (access fcactivation act :insthyp))
(equal ttree (access fcactivation act :ttree)))
act)
(t (change fcactivation act
:insthyp insthyp
:hyps hyps
:ttree ttree))))
(t (change fcactivation act
:insthyp insthyp
:hyps hyps
:unifysubst unifysubst
:ttree ttree))))
(mutualrecursion
; These two functions return nonnil when sublisvar (respectively,
; sublisvarlst) can return a term (resp. list of terms) different from the
; input.
(defun sublisvarp (alist term)
(declare (xargs :guard (and (symbolalistp alist)
(pseudotermp term))))
(cond ((variablep term)
(assoceq term alist))
((fquotep term)
nil)
(t (sublisvarlstp alist (fargs term)))))
(defun sublisvarlstp (alist l)
(declare (xargs :guard (and (symbolalistp alist)
(pseudotermlistp l))))
(if (null l)
nil
(or (sublisvarp alist (car l))
(sublisvarlstp alist (cdr l)))))
)
(defun multsearchtypealist (resthyps concls term typ typealist unifysubst
ttree oncep)
; This function is a variant of searchtypealist, instead searching for all
; instances of term that bind to a subset of typ. It returns a list of
; substitutions (which produce those instances) together with a corresponding
; list of tagtrees each extending ttree.
(cond ((null typealist)
(mv nil nil))
((tssubsetp (cadr (car typealist)) typ)
(mvlet (ans newunifysubst)
(onewayunify1 term (car (car typealist)) unifysubst)
(cond
(ans (let ((diffalist (alistdifferenceeq newunifysubst
unifysubst)))
(cond
((or oncep
(not (or (sublisvarlstp diffalist resthyps)
(sublisvarlstp diffalist concls))))
; We aren't going to look for additional bindings either because we're not
; supposed to (i.e. oncep is true) or there is no point. In the latter
; case the newlybound variables do not occur free in the remaining hyps or the
; conclusions of the forwardchaining rule under consideration. So, there is
; no point to looking for additional bindings.
(mv (list newunifysubst)
(list (constagtrees (cddr (car typealist))
ttree))))
; We found a new unifysubst but there may be additional interesting ones out
; there.
(t (mvlet (otherunifies otherttrees)
(multsearchtypealist resthyps concls
term
typ
(cdr typealist)
unifysubst
ttree
oncep)
(mv (cons newunifysubst otherunifies)
(cons (constagtrees
(cddr (car typealist)) ttree)
otherttrees)))))))
; We didn't find any new substitutions; try again.
(t (multsearchtypealist resthyps concls term
typ
(cdr typealist)
newunifysubst
ttree
oncep)))))
(t (multsearchtypealist resthyps concls term
typ
(cdr typealist)
unifysubst
ttree
oncep))))
(defun multlookuphyp (hyp resthyps concls typealist wrld unifysubst ttree
oncep)
; This function is a variant of lookuphyp, instead returning a list of
; unifysubsts and a corresponding list of tag trees. See the comment in
; multsearchtypealist.
(mvlet (term typ)
(termandtyptolookup hyp wrld)
(multsearchtypealist resthyps concls term typ typealist
unifysubst ttree oncep)))
(mutualrecursion
(defun evrespectingens (form alist state latches ttree ens wrld)
; This is a variant of ev (see also evrec) that avoids calling functions whose
; executable counterparts are disabled. Thus, here we return (mv erp val
; latches ttree), where ev would return (mv erp val latches) and ttree extends
; the given ttree by adding executablecounterpart runes justifying the
; evaluation. If erp is nonnil then val and ttree are to be taken as
; meaningless.
(cond ((or (variablep form)
(fquotep form))
(mvlet (erp val latches)
(ev form alist state latches t)
(mv erp val latches ttree)))
(t (let ((fn (ffnsymb form)))
(cond
((or (flambdap fn)
(enabledxfnp fn ens wrld))
(cond ((eq fn 'if)
(mvlet
(tester test latches ttree)
(evrespectingens (fargn form 1) alist state
latches ttree ens wrld)
(cond (tester (mv t test latches ttree))
(test (evrespectingens
(fargn form 2)
alist state latches
(pushlemma '(:EXECUTABLECOUNTERPART if)
ttree)
ens wrld))
(t (evrespectingens
(fargn form 3)
alist state latches
(pushlemma '(:EXECUTABLECOUNTERPART if)
ttree)
ens wrld)))))
(t (mvlet
(argser args latches ttree)
(evlstrespectingens (fargs form) alist state
latches ttree ens wrld)
(cond
(argser (mv t args latches ttree))
(t (cond
((flambdap fn)
(evrespectingens
(lambdabody (ffnsymb form))
(pairlis$ (lambdaformals (ffnsymb form))
args)
state latches ttree ens wrld))
(t (mvlet (erp val latches)
(evfncall fn args state latches t)
(mv erp val latches
(pushlemma
`(:EXECUTABLECOUNTERPART ,fn)
ttree)))))))))))
(t (mv t nil latches ttree)))))))
(defun evlstrespectingens (lst alist state latches ttree ens wrld)
(cond ((endp lst)
(mv nil nil latches ttree))
(t (mvlet (erp val latches ttree)
(evrespectingens (car lst) alist state latches ttree ens wrld)
(cond (erp (mv erp val latches ttree))
(t (mvlet (erp rst latches ttree)
(evlstrespectingens (cdr lst) alist state latches
ttree ens wrld)
(cond (erp (mv erp rst latches ttree))
(t (mv nil (cons val rst) latches ttree))))))))))
)
(mutualrecursion
(defun multrelievefchyps
(rune target hyps concls unifysubst typealist ens forceflg wrld state
ttree
acc1 acc2 acc3 acc4 oncep)
; We map over hyps and try to relieve each one. The idea is to return four
; results: new values for insthyp, hyps, unifysubst, and ttree. If we prove
; all the hyps, the new insthyp is *t* and the new hyps is nil. If we show
; some hyp false, the new insthyp is *nil*.
; However, each of these results is given as a list since a free variable may
; be bound in several ways, each of which generates a different conclusion.
; The four lists are in lock step with each other (e.g., the first result is
; the first element of each list). Thus, the lists will always have the same
; length. Moreover, for efficiency we accumulate into the four result lists
; that are passed in: acc1, acc2, acc3, acc4.
; We decided not to structure this function like relievehyps (giving
; rise to a relievefchyp) because the answer is so complicated since it
; is involved with state saving.
; We know four ways to relieve a hyp. If it has no free vars, we try
; typeset and we use evaluation (if it is ground). If it has free
; vars, we look it up in the typealist. In both cases we respect
; FORCEd and CASESPLITd hyps. The way we fail determines what we return.
; Note: Forward chaining was first coded before typeset could force
; 'assumptions. Thus, splitting on 'assumptions was uncommon, indeed,
; it was only done for the output of linear arithmetic, where we first
; used the idea in the late 70's. Thus, the forward chaining
; mechanism was designed so as not to produce any 'assumptions, i.e.,
; so as not to call rewrite. When typeset was extended, assumption
; generation and handling became more widespread. In particular,
; this function can generate assumptions due to the call of typeset
; below and those assumptions are handled by the caller of the
; forwardchaining module. So now, except for these historical
; comments, there is no rationale behind this function's abstinence
; from rewrite. Mixing forward and backward chaining so intimately
; might be interesting. It might also be a can of worms. It might
; also be inevitable. It just isn't the most important thing to do
; just yet.
(cond
((null hyps) (mv (cons *t* acc1)
(cons nil acc2)
(cons unifysubst acc3)
(cons ttree acc4)))
(t (let* ((forcep1 (and (nvariablep (car hyps))
(not (fquotep (car hyps)))
(or (eq (ffnsymb (car hyps)) 'force)
(eq (ffnsymb (car hyps)) 'casesplit))))
(forcerfn (and forcep1 (ffnsymb (car hyps))))
(hyp (if forcep1 (fargn (car hyps) 1) (car hyps))))
(cond
((freevarsp hyp unifysubst)
(mvlet (unifysubstlist ttreelist)
(multlookuphyp hyp (cdr hyps) concls
typealist wrld unifysubst ttree
oncep)
(cond
(unifysubstlist
(multrelieveallfchyps
rune target (cdr hyps) concls unifysubstlist typealist
ens forceflg wrld state ttreelist acc1 acc2 acc3 acc4
oncep))
(t
(mvlet
(forceflg ttree)
(cond
((or (not forcep1) (not forceflg))
(mv nil ttree))
(t
(forceassumption
rune
target
(sublisvarandmarkfree unifysubst hyp)
typealist nil
(immediateforcep forcerfn ens)
forceflg
ttree)))
(cond
(forceflg
(multrelievefchyps
rune target (cdr hyps) concls unifysubst typealist
ens forceflg wrld state ttree
acc1 acc2 acc3 acc4 oncep))
(t (mv (cons *t* acc1)
(cons hyps acc2)
(cons unifysubst acc3)
(cons ttree acc4)))))))))
(t (let ((insthyp (sublisvar unifysubst hyp)))
(mvlet (ts ttree1)
(typeset insthyp forceflg nil
typealist nil ens wrld nil
nil nil)
(cond ((ts= ts *tsnil*)
(mv (cons *nil* acc1)
(cons nil acc2)
(cons unifysubst acc3)
(cons ttree acc4)))
((tsintersectp ts *tsnil*)
(cond
((freevarsp insthyp nil)
(mvlet
(forceflg ttree)
(cond
((or (not forcep1) (not forceflg))
(mv nil ttree))
(t (forceassumption
rune target insthyp typealist nil
(immediateforcep forcerfn ens)
forceflg ttree)))
(cond
(forceflg
(multrelievefchyps
rune target (cdr hyps) concls unifysubst
typealist ens forceflg wrld state ttree
acc1 acc2 acc3 acc4 oncep))
(t (mv (cons insthyp acc1)
(cons (cdr hyps) acc2)
(cons unifysubst acc3)
(cons ttree acc4))))))
((programtermp insthyp wrld)
(mv (cons insthyp acc1)
(cons (cdr hyps) acc2)
(cons unifysubst acc3)
(cons ttree acc4)))
(t
(mvlet
(erp val latches ttree1)
(evrespectingens
insthyp nil state nil nil ens wrld)
(declare (ignore latches))
; If the evaluation is nonerroneous and produces a nonnil val, we
; succeeded. But if the hyp caused an error or if it produced nil, we
; not only fail but report that this hyp was disproved.
(cond
((and (not erp) val)
(multrelievefchyps
rune target (cdr hyps) concls unifysubst
typealist ens forceflg wrld state
(sconstagtrees ttree1 ttree)
acc1 acc2 acc3 acc4 oncep))
(t (mv (cons *nil* acc1)
(cons nil acc2)
(cons unifysubst acc3)
(cons ttree acc4))))))))
(t (multrelievefchyps
rune target (cdr hyps) concls unifysubst
typealist ens forceflg wrld state
(sconstagtrees ttree1 ttree) acc1 acc2 acc3
acc4 oncep)))))))))))
(defun multrelieveallfchyps (rune target hyps concls unifysubstlist
typealist ens forceflg wrld state
ttreelist
acc1 acc2 acc3 acc4 oncep)
; This function is a helper for multrelievefchyps. It calls
; multrelievefchyps once for each element of unifysubstlist and
; corresponding element of ttreelist, appending the respective return values
; of multrelievefchyps.
(if (not (consp unifysubstlist))
(mv acc1 acc2 acc3 acc4)
(mvlet (acc1 acc2 acc3 acc4)
(multrelievefchyps
rune target hyps concls (car unifysubstlist) typealist ens
forceflg wrld state (car ttreelist) acc1 acc2 acc3 acc4 oncep)
(multrelieveallfchyps
rune target hyps concls (cdr unifysubstlist) typealist ens
forceflg wrld state (cdr ttreelist) acc1 acc2 acc3 acc4
oncep))))
)
; Forward Chaining Derivations  fcderivation  fcd
; To implement forward chaining, especially to implement the heuristic
; controls on which derived conclusions to keep, we have to use ttrees in
; a rather subtle way that involves embedding a ttree in a tagged object
; in another ttree. These tagged objects holding ttrees are called
; "fcderivations". We motivate and discuss them here. However, no
; fcderivation gets out of the forward chaining module. That is, once
; forwardchain has done its job, the ttrees seen throughout the rest of
; the system are free of 'fcderivations.
; When we finally relieve all the hyps we will create the instantiated
; conclusion, concl. However, we do not just turn it loose in the world.
; We need to track it for two reasons. The first reason concerns the
; ultimate use of such derived conclusions: when we have finished all our
; forward chaining and go into the rewriting of literals we will need to
; choose from among the available forward chained concls those that don't
; depend upon the literal we are rewriting. For this it is sufficient to
; have the ttree of the conclusion. The second reason is closer to home:
; before we even get out of forward chaining we have to decide whether
; this derived concl is worth keeping. This is a heuristic decision,
; aimed primarily at preventing infinite forward chaining while
; permitting "desirable" forward chaining. Our heuristic is based on
; consideration of how the concl was derived. Roughly put, we will keep
; it unless it is worse than some concl in its derivation. So we need to
; record its derivation. That derivation must contain the names of the
; rules used and the derived conclusions used.
; The obvious thing to do is to add to the ttree of concl the name of the
; rule used and concl itself. That ttree will attach itself to every
; deduction using concl and by inspecting it we will see concl itself in
; the tree, and by induction, all the concls upon which it depends.
; Unfortunately, this is tricky because ttrees represent sets of all the
; things with a given tag. Thus, for example, if we were to tag the rule
; name with 'lemma and add it to the tree, we would not record the fact
; that name had perhaps been used twice; the previous occurrence of
; (lemma . name) in the tree would prevent addtotagtree from changing
; the tree. Similarly, while each concl used would be in the set of all
; things tagged 'concl, we couldn't tell which had been used where, how
; many times, or by which rules.
; So we do something very odd (because it results in a ttree being a
; component of an object stored in a ttree). We make what we call an
; "fcderivation" which is a structure of the form:
; (defrec fcderivation
; ((rune . concl) (fncnt . pfncnt) (insttrigger . ttree))
; t)
; Rune is the name of the rule applied, concl is the instantiated conclusion.
; Fncnt is the function symbol count of concl (as computed by fncount) and
; pfncnt is the pseudofunction count (see termorder). These are used in
; our heuristic for deciding whether to keep a concl. Ttree is the ttree that
; derived concl from name. Insttrigger is the term in the current problem
; that fired this rule.
; If we decide to keep concl then we make a ttree that contains its
; fcderivation as its only object, tagged 'fcderivation. That ttree is
; attached to the assumption of concl in the new typealist and will
; attach itself to all uses of concl. Given an fcderivation we can
; reconstruct the derivation of its concl as follows: concl was derived
; by applying name to all of the derived concls in all of the
; 'fcderivations in its ttree.
; When the internal forward chaining process is complete we will have
; collected a list of fcderivations deduced from the given clause.
; The ttree in each derivation will indicate the parent literals via
; 'pt tags. We can also recover the names of the forward chaining
; rules used. However, all of this information is not visible to the
; standard ttree scanners because there are ttrees nested inside of
; tagged 'fcderivations. For example, if during rewriting we were to
; assume the concl of some fcd and tag it with the ttree in that fcd,
; then that ttree might find its way into the ttree eventually
; returned by rewrite. That would in turn be looked at by the printer
; to determine which lemmas got used. And unless we coded the
; printer's sweep to know about the ttrees inside of 'fcderivations,
; it would miss the forward chaining rules. Similarly, the sweep to
; determine if a given 'pt is used would have to go into
; 'fcderivations. We have decided it is better if, upon finishing
; our forward chaining, we convert the recursively nested ttrees in
; 'fcderivations to standard ttrees. This destroys the information
; about exactly how concl was derived from its supporters but it lifts
; out and makes visible the 'lemmas and 'pt upon which the concl is
; based.
(defun makettreesfromfcderivations (fcderivations)
(cond ((null fcderivations) nil)
(t (cons (addtotagtree 'fcderivation (car fcderivations) nil)
(makettreesfromfcderivations (cdr fcderivations))))))
(defun expungefcderivations (ttree)
; We copy ttree, replacing each 'fcderivation in it by a new node which tags
; the rule name with 'lemma and lifts out the interior ttrees and expunges
; them. Thus, when we are done we have a ttree with no 'fcderivation tags,
; but which has 'lemma tags on the set of names in the 'fcderivations and
; which has all of the 'pt objects and 'assumptions (for example) that were
; recursively embedded in 'fcderivations.
; Note: This function must be able to find 'fcderivations anywhere within the
; ttree. In particular, before we removed ttrees from the typealists in
; 'assumptions, we had to expunge the fcderivations within the typealists.
; See the comment in forceassumptions. Remember that 'fcderivations are for
; heuristic use only, except that they may contain 'pt and 'assumption objects
; that we must lift out. So we should be ruthless about finding and expunging
; all 'fcderivations.
; Once upon a time we detected an 'fcderivation at the end of prove. It
; slipped into the final proof tree as follows: Forward chaining made two
; passes. During the first, hyp1 was concluded. During the second, hyp2 was
; concluded and forced an assumption. That assumption contained the typealist
; produced from the first pass, which had the 'fcderivation for hyp1. Now if
; forwardchaining had proved the theorem, we would be in good shape. But
; suppose it doesn't prove the theorem and we start rewriting. Suppose the
; rewriter appeals to hyp2. That causes it to raise the assumption. We then
; try, at the end of rewriteclause, to relieve the assumption by rewriting it
; under its typealist. Suppose that we use hyp1 during that successful
; relieving of the assumption: its 'fcderivation then enters our final proof
; tree. Here is a script that used to provoke this bug. The fix, below, is to
; expunge fcderivations from the :typealists of assumptions. We keep this
; script simply because it took a while to find the path down which the
; 'fcderivation migrated out of forwardchaining.
#
(erprogn
(defstub hyp1 (x) t)
(defstub hyp2 (x) t)
(defstub trig (x) t)
(defstub assumptionp (x) t)
(defstub concl (x) t)
(defaxiom fctohyp1
(hyp1 (trig x))
:ruleclasses ((:forwardchaining :triggerterms ((trig X)))))
(defaxiom thenfctohyp2
(implies (and (hyp1 x) (force (assumptionp x)))
(hyp2 x))
:ruleclasses :forwardchaining)
(defaxiom inrewriteusehyp2thusraisingtheassumption
(implies (hyp2 x) (concl x)))
(defaxiom andrelievetheassumptionbyappealtohyp1suckinginthefcderiv
(implies (hyp1 x) (assumptionp x)))
(thm (concl (trig a))))
#
(cond ((null ttree) nil)
((symbolp (caar ttree))
(cond ((eq (caar ttree) 'fcderivation)
(pushlemma
(access fcderivation (cdar ttree) :rune)
(constagtrees
(expungefcderivations
(access fcderivation (cdar ttree) :ttree))
(expungefcderivations (cdr ttree)))))
(t (addtotagtree (caar ttree)
(cdar ttree)
(expungefcderivations (cdr ttree))))))
(t (constagtrees (expungefcderivations (car ttree))
(expungefcderivations (cdr ttree))))))
; This completes the discussion of fcderivations and we now proceed to
; use them in the forward chaining process. We resume mainline
; development by coding the functions that resume a suspended activation
; of a forward chaining rule.
(defun addfcderivations (rune concls insttrigger ens wrld state ttree
fcdlst)
; For each concl in concls we generate an fcderivation with the given
; rune and ttree. We add each fcderivation to the list fcdlst and
; return the final fcdlst.
(cond ((null concls) fcdlst)
(t (mvlet
(flg concl newttree)
(evalgroundsubexpressions (car concls) ens wrld state ttree)
(declare (ignore flg))
(mvlet
(fncnt pfncnt)
(fncount concl)
(addfcderivations rune (cdr concls) insttrigger
ens wrld state ttree
(cons
(make fcderivation
:rune rune
:concl concl
:fncnt fncnt
:pfncnt pfncnt
:insttrigger insttrigger
:ttree newttree)
fcdlst)))))))
(defun multadvanceeachfcactivation1 (newinsthyplist newhypslist
newunifysubstlist
newttreelist
act ens wrld
state fcdlst)
; This function assumes we have gotten past the :insthyp of fcactivation act
; (either because it is *t* or because we relieved it with the given ttree).
; For each element in newinsthyplist (and the corresponding elements of the
; other lists), we work our way through the :hyps of act. We eventually return
; the two results promised by our superiors, multadvancefcactivation1 and
; multadvancefcactivation (q.v.): a list of suspended activations to use in
; place of act, which is nil if act is to be discontinued either because it
; terminated or aborted; and an extended fcdlst containing the derived
; conclusions.
(if (endp newinsthyplist) ; shouldn't happen the first time
(mv nil fcdlst)
(mvlet (newact newfcdlst)
(let ((newinsthyp (car newinsthyplist))
(newhyps (car newhypslist))
(newunifysubst (car newunifysubstlist))
(newttree (car newttreelist)))
(cond ((equal newinsthyp *t*)
(cond ((null newhyps)
(let* ((rule (access fcactivation act :rule)))
(mv nil
(addfcderivations
(access forwardchainingrule rule :rune)
(sublisvarlst newunifysubst
(access forwardchainingrule
rule
:concls))
(access fcactivation act :insttrigger)
ens wrld state
newttree
fcdlst))))
(t (mv (suspendfcactivation act
*t*
newhyps
newunifysubst
newttree)
fcdlst))))
((equal newinsthyp *nil*)
; This is the signal that we have disproved a hyp (or at least have
; chosen to abandon this activation).
(mv nil fcdlst))
(t (mv (suspendfcactivation act
newinsthyp
newhyps
newunifysubst
newttree)
fcdlst))))
(mvlet (newacts newfcdlst2)
(multadvanceeachfcactivation1 (cdr newinsthyplist)
(cdr newhypslist)
(cdr newunifysubstlist)
(cdr newttreelist)
act ens wrld
state newfcdlst)
(mv (if newact (cons newact newacts) newacts)
newfcdlst2)))))
(defun multadvancefcactivation1
(act ttree typealist ens oncepoverride forceflg wrld state fcdlst)
; This function assumes we have gotten past the :insthyp of fcactivation act
; (either because it is *t* or because we relieved it with the given ttree).
; It attempts to relieve the remaining hypotheses of the forwardchainingrule
; of act, then passes the results to multadvanceeachfcactivation1 to return
; a new list of fcactivations and a new fcdlst.
(mvlet (newinsthyplist newhypslist newunifysubstlist newttreelist)
(let ((rule (access fcactivation act :rule)))
(multrelievefchyps (access forwardchainingrule
rule
:rune)
(access fcactivation act :insttrigger)
(access fcactivation act :hyps)
(access forwardchainingrule
rule
:concls)
(access fcactivation act :unifysubst)
typealist
ens forceflg wrld state
(sconstagtrees ttree
(access fcactivation act
:ttree))
nil nil nil nil
(oncep oncepoverride
(access forwardchainingrule
rule
:matchfree)
(access forwardchainingrule
rule
:rune)
(access forwardchainingrule
rule
:nume))))
(multadvanceeachfcactivation1 newinsthyplist newhypslist
newunifysubstlist newttreelist act
ens wrld state fcdlst)))
(defun multadvancefcactivation (act typealist ens oncepoverride forceflg
wrld state fcdlst)
; Act is an fc activation. Fcdlst is a list of all of the
; fcderivations made so far (this pass). We try to relieve the hyps of
; act. We return two results. The first is either an activation to use
; in place of act or else is nil meaning act is being discontinued. The
; second is an extension of fcdlst containing all the newly derived
; conclusions (as fcderivations).
(withaccumulatedpersistence
(access forwardchainingrule
(access fcactivation act :rule)
:rune)
(act fcdlst)
(let ((insthyp (access fcactivation act :insthyp)))
(cond
((equal insthyp *t*)
(multadvancefcactivation1
act nil typealist ens oncepoverride forceflg wrld state fcdlst))
(t (mvlet (ts ttree)
(typeset insthyp forceflg nil typealist nil ens wrld nil
nil nil)
(cond ((ts= ts *tsnil*)
(mv nil fcdlst))
((tsintersectp ts *tsnil*)
(mv (list act) fcdlst))
(t (multadvancefcactivation1
act ttree typealist ens oncepoverride forceflg
wrld state fcdlst)))))))))
(defun advancefcactivations (lst typealist ens oncepoverride forceflg wrld
state fcdlst)
; Lst is of the form (act1 ... actn), where each acti is an fc
; activation. fcdlst is a list of fcderivations onto which we
; accumulate any derived conclusions (as fcderivations). We return two
; results: a new list of possibly advanced suspended activations and the
; accumulated fcdlst.
(cond ((null lst) (mv nil fcdlst))
(t (mvlet (acts fcdlst)
(advancefcactivations (cdr lst)
typealist
ens
oncepoverride
forceflg
wrld
state
fcdlst)
(mvlet (newacts fcdlst)
(multadvancefcactivation
(car lst) typealist
ens oncepoverride forceflg wrld state fcdlst)
(mv (append newacts acts)
fcdlst))))))
(defun advancefcpotlst
(fcpotlst typealist ens oncepoverride forceflg wrld state fcdlst)
; Fcpotlst is a list of fcpots, each of the form (term act1 ...
; actn). We advance all the activations, producing a new fcpotlst and
; an accumulated list of fcderivations containing the derived
; conclusions.
(cond ((null fcpotlst) (mv nil fcdlst))
(t (mvlet
(acts fcdlst)
(advancefcactivations (cdr (car fcpotlst))
typealist ens oncepoverride forceflg
wrld state fcdlst)
(mvlet
(rstfcpotlst fcdlst)
(advancefcpotlst (cdr fcpotlst) typealist ens oncepoverride
forceflg wrld state fcdlst)
(mv (cons (cons (car (car fcpotlst)) acts)
rstfcpotlst)
fcdlst))))))
; So by applying the above function we can make one pass over an fc pot
; list and derive a new pot list and a set of conclusions. We now
; develop the code for processing those conclusions. We want to assume
; each conclusion, tagged with a ttree that records its fcderivation, on
; an extension of typealist.
(defun typealistfcdlst (fcdlst typealist donotreconsiderp ens wrld)
; We take a list of fc histories and assume the truth of each concl,
; extending typealist. We return two results. The first is t or nil
; indicating whether a contradiction was found. When a contradiction is
; found, the second result is the ttree of that contradiction. It may
; mention 'fcderivations that contain rule names that should be reported
; and other ttrees with fcderivations in them. When no contradiction is
; found, the second result is the final typealist.
; Note that when we finish, (null fcdlst), we reconsider the typealist. This
; is analogous to typealistclausefinish. We have seen an example of forward
; chaining where we derived, in order, (< 0 x), (< x 1), (integerp x), and
; failed to recognize the contradiction, just as typealistclausefinish1
; fails to recognize that contradiction.
(cond
((null fcdlst)
(if donotreconsiderp
(mv nil typealist)
(mvlet (contradictionp xtypealist ttree)
(reconsidertypealist typealist typealist nil ens wrld nil
nil nil)
(cond
(contradictionp (mv t ttree))
(t (mv nil xtypealist))))))
(t (mvlet
(mbt mbf tta fta ttree)
(assumetruefalse
(access fcderivation (car fcdlst) :concl)
(addtotagtree 'fcderivation
(car fcdlst)
nil)
t nil typealist nil ens wrld
nil nil :fta)
(declare (ignore fta))
(cond (mbf (mv t ttree))
(mbt (typealistfcdlst (cdr fcdlst)
typealist donotreconsiderp ens wrld))
(t (typealistfcdlst (cdr fcdlst)
tta donotreconsiderp ens wrld)))))))
; When we have obtained a list of fc histories from forward chaining we
; get the opportunity to filter it on heuristic grounds. The problem is
; to avoid infinite forward chaining. So we define a predicate that
; determines whether we wish to keep a given derivation, given the
; current fcdlst.
(defun fcdrunep (rune ttree)
; Rune is the name of a forward chaining rule. We want to determine if
; rune has been used in any fcderivation in ttree. This function is
; analogous to tagtreeoccur except that it looks for the tag
; 'fcderivation and it recursively looks into the ttrees contained
; therein.
(cond ((null ttree) nil)
((symbolp (caar ttree))
(cond ((eq (caar ttree) 'fcderivation)
(or (equal rune (access fcderivation (cdar ttree) :rune))
(fcdrunep rune
(access fcderivation
(cdar ttree)
:ttree))
(fcdrunep rune (cdr ttree))))
(t (fcdrunep rune (cdr ttree)))))
(t (or (fcdrunep rune (car ttree))
(fcdrunep rune (cdr ttree))))))
(defun fcdworsethanorequal (concl fncnt pfncnt ttree)
; Concl is a term and fncnt is its function symbol count. If there
; exists a concl' with fn count fncnt' in an 'fcderivation of ttree
; such that fncnt >= fncnt' and concl is worsethanorequal to concl',
; then we return t. Otherwise we return nil.
(cond ((null ttree) nil)
((symbolp (caar ttree))
(cond ((eq (caar ttree) 'fcderivation)
(or (and (let ((fcfncnt (access fcderivation (cdar ttree)
:fncnt)))
(or (> fncnt fcfncnt)
(and (eql fncnt fcfncnt)
(>= pfncnt
(access fcderivation (cdar ttree)
:pfncnt)))))
(worsethanorequal concl
(access fcderivation
(cdar ttree)
:concl)))
(fcdworsethanorequal concl fncnt pfncnt
(access fcderivation
(cdar ttree)
:ttree))
(fcdworsethanorequal concl fncnt pfncnt
(cdr ttree))))
(t (fcdworsethanorequal concl fncnt pfncnt
(cdr ttree)))))
(t (or (fcdworsethanorequal concl fncnt pfncnt (car ttree))
(fcdworsethanorequal concl fncnt pfncnt (cdr ttree))))))
; Once upon a time we had heuristics for keeping concl if it there was
; a lit of the current clause that was worse than it or if there was a
; concl already kept that was worse than it. We have temporarily
; removed those and replaced them by the faster check that the
; triggering term occurs in the clause. But we'll keep the
; definitions in case we want to reinstate the heuristics.
#
(defun existslitworsethanorequal (cl concl fncnt)
(cond
((null cl) nil)
(t (or (and (>= (fncount (car cl)) fncnt)
(worsethanorequal (car cl) concl))
(existslitworsethanorequal (cdr cl)
concl
fncnt)))))
#
(defun existsfcdworsethanorequal (fcdlst concl fncnt pfncnt)
(cond
((null fcdlst) nil)
(t (or (and (let ((fcdfncnt (access fcderivation (car fcdlst) :fncnt)))
(or (> fcdfncnt fncnt)
(and (eql fcdfncnt fncnt)
(>= (access fcderivation (car fcdlst) :pfncnt)
pfncnt))))
(worsethanorequal
(access fcderivation (car fcdlst) :concl)
concl))
(existsfcdworsethanorequal (cdr fcdlst)
concl
fncnt
pfncnt)))))
(defun approvedfcderivationp (fcd cl fcdlst)
; We return t iff we approve fcd as a new fact we will add to fcdlst
; while forward chaining from clause cl. Fcpotlst is the current
; pot list and hence exhibits all the terms in the current problem.
; Our heuristic for approving an fcderivation is that either (a) name
; not have been used before in this derivation or (b) concl is not
; worsethanorequal any concl in the derivation, or (c) the
; triggering term of this fcd is in the current clause.
(declare (ignore fcdlst))
(let ((ttree (access fcderivation fcd :ttree)))
(or (not (fcdrunep (access fcderivation fcd :rune) ttree))
(not (fcdworsethanorequal (access fcderivation fcd :concl)
(access fcderivation fcd :fncnt)
(access fcderivation fcd :pfncnt)
ttree))
(dumboccurlst (access fcderivation fcd :insttrigger) cl))))
(defun approvefcderivations (newfcdlst cl approved fcdlst)
; We have just derived the fcderivations in newfcdlst, from the
; negations of the literals in cl and the fcderivations in fcdlst. We
; wish to filter out those new fcderivations that we do not wish to
; pursue. We return two values, the approved new fcderivations and a
; modified version of fcdlst to which the approved new fcderivations
; have been added. The reason we do the apparently extraneous job of
; adding the approved ones to the existing ones is so that the
; determination of whether we approve of a given new one can be made in
; the context of all those we've already approved.
(cond ((null newfcdlst) (mv approved fcdlst))
((approvedfcderivationp (car newfcdlst) cl fcdlst)
(approvefcderivations (cdr newfcdlst)
cl
(cons (car newfcdlst) approved)
(cons (car newfcdlst) fcdlst)))
(t (approvefcderivations (cdr newfcdlst)
cl
approved
fcdlst))))
; So we are now almost ready to put it all together.
(mutualrecursion
(defun maxlevelno (term wrld)
; Each defun'd function, except the ones being defund at the moment,
; has a 'levelno property, which is a nonnegative integer. The ACL2
; primitives have no levelno property, which we treat as though it were
; 0. This function computes the maximum stored levelno of the functions
; appearing in term. Any fn appearing without a levelno is treated
; as though it had level 0, i.e., it is ignored.
(cond ((variablep term) 0)
((fquotep term) 0)
(t (max (getlevelno (ffnsymb term) wrld)
(maxlevelnolst (fargs term)
wrld)))))
(defun maxlevelnolst (args wrld)
(cond ((null args) 0)
(t (max (maxlevelno (car args) wrld)
(maxlevelnolst (cdr args) wrld)))))
(defun getlevelno (fn wrld)
; Fn is either a lambda expression or a function symbol. We return
; its level number.
(cond ((flambdap fn) (maxlevelno (lambdabody fn) wrld))
((getprop fn 'levelno nil
'currentacl2world wrld))
(t 0)))
)
(mutualrecursion
(defun sortapproved1rating1 (term wrld fc vc)
(cond ((variablep term) (mv fc (1+ vc)))
((fquotep term) (mv fc vc))
((flambdaapplicationp term)
(mvlet (fc vc)
(sortapproved1rating1 (lambdabody term) wrld fc vc)
(sortapproved1rating1lst (fargs term) wrld (1+ fc) vc)))
((or (eq (ffnsymb term) 'not)
(= (getprop (ffnsymb term) 'absoluteeventnumber 0
'currentacl2world wrld)
0))
(sortapproved1rating1lst (fargs term) wrld fc vc))
(t (sortapproved1rating1lst (fargs term) wrld
(+ 1
(getlevelno (ffnsymb term) wrld)
fc)
vc))))
(defun sortapproved1rating1lst (lst wrld fc vc)
(cond ((null lst) (mv fc vc))
(t (mvlet (fc vc)
(sortapproved1rating1 (car lst) wrld fc vc)
(sortapproved1rating1lst (cdr lst) wrld fc vc)))))
)
(defun sortapproved1rating (term wrld)
; In forwardchaining we assume all the derived concls. We sort them by the
; ratings computed here, assuming first those terms with the highest rating.
; Therefore, we wish to give high numbers to very typelike terms such as
; (rationalp x) and (not (< x '0)). Actually, all our ratings are nonpositive
; integers, with 0 thus the highest. The terms pictured above have ratings of
; 1 because they contain a single variable and are otherwise completely
; primitive. If you assume no term contains more than 10 variable occurrences
; then the ordering imposed by these ratings is lexicographic, favoring
; low function count and using variable occurrences to break ties. No
; real consideration has been given this measure beyond that it puts
; the terms above before others!
(mvlet (fc vc)
(sortapproved1rating1 term wrld 0 0)
( (+ (* 10 fc) vc))))
(defun sortapproved1 (approved wrld)
(cond ((null approved) nil)
(t (cons
(cons (sortapproved1rating
(access fcderivation (car approved) :concl)
wrld)
(car approved))
(sortapproved1 (cdr approved) wrld)))))
(defun sortapproved (approved wrld)
; Approved is a list of fcderivations which have derived certain :concls.
; We sort that list so that those with the higher rated :concls come first.
(stripcdrs (mergesortcar> (sortapproved1 approved wrld))))
(defun stripfcdconcls (fcdlst)
(cond ((null fcdlst) nil)
(t (cons (access fcderivation (car fcdlst) :concl)
(stripfcdconcls (cdr fcdlst))))))
(defun forwardchain1 (cl fcpotlst typealist forceflg wrld
donotreconsiderp ens oncepoverride state fcdlst)
; We first advance every fcactivation in fcpotlst, obtaining a new
; potlst and some derived fcderivations. We filter the derived
; fcderivations, throwing out any that, on heuristic grounds, we
; don't like. We then assume the approved derived fcderivations,
; updating the typealist. We extend fcpotlst with any new subterms
; and their associated activations, and we loop until either we get a
; contradiction or we stabilize. We repeatedly extend typealist as
; we go, but the extended typealist is of no use outside forward
; chaining because it is full of fcderivations. We return two
; results. The first is a t or nil indicating whether a contradiction
; was found. The second is a ttree if a contradiction was found and
; is the final fcdlst otherwise.
(mvlet (fcpotlst newfcdlst)
(advancefcpotlst fcpotlst typealist ens oncepoverride
forceflg wrld state nil)
(mvlet (approved fcdlst)
(approvefcderivations newfcdlst
cl
nil
fcdlst)
(mvlet (contradictionp x)
(typealistfcdlst
(sortapproved approved wrld)
typealist donotreconsiderp ens wrld)
(cond (contradictionp (mv t x))
((equal x typealist) (mv nil fcdlst))
(t (forwardchain1
cl
(addnewfcpotslstlst
(stripfcdconcls approved)
(makettreesfromfcderivations approved)
forceflg wrld ens fcpotlst)
x forceflg wrld donotreconsiderp ens
oncepoverride state fcdlst)))))))
(defun fcpairlst (fcdlst)
; We convert a list of fcderivations to a list of pairs of the form
; (concl . ttree), where each ttree is expunged of fcderivations. We
; call such a pair an "fcpair." These pairs can be sensibly used
; outside of the forwardchaining module because the ttrees are free
; of fcderivations.
(cond ((null fcdlst) nil)
(t (cons (cons (access fcderivation (car fcdlst) :concl)
(pushlemma
(access fcderivation (car fcdlst) :rune)
(expungefcderivations
(access fcderivation (car fcdlst) :ttree))))
(fcpairlst (cdr fcdlst))))))
(defun fcpairlsttypealist (fcpairlst typealist ens wrld)
; Fcpairlst is a list of pairs of the form (concl . ttree). We extend
; typealist by assuming the truth of every concl, tagging each typealist
; entry with the ttree, which we assume has already been expunged of
; 'fcderivations. Assuming the initial typealist had no 'fcderivations in
; it, the final one doesn't either. We return the resulting typealist unless
; a contradiction arises, in which case we return the resulting ttree.
; At one time we assumed that there was no contradiction, causing a hard error
; if we found one. However, Jared Davis sent the following script that causes
; that hard error, so we changed this function. A relevant comment, from
; before that change, is given below.
#
(defstub appealp (* *) => *)
(defstub appeallistp (* *) => *)
(defstub appealstructurep (*) => *)
(defstub appealstructurelistp (*) => *)
(defstub getsubgoals (*) => *)
(defstub appealprovisionallyokp (* * *) => *)
(defstub proofp (* * *) => *)
(defstub prooflistp (* * *) => *)
(defaxiom appealstructurelistpforwardtoappealstructurepofcar
(implies (appealstructurelistp x)
(equal (appealstructurep (car x))
(if x t nil)))
:ruleclasses :forwardchaining)
(defaxiom appealplistpforwardtoappealpofcar
(implies (appeallistp x aritytable)
(equal (appealp (car x) aritytable)
(if x t nil)))
:ruleclasses :forwardchaining)
(defaxiom appealpforwardtoappealstructurep
(implies (appealp x aritytable)
(appealstructurep x))
:ruleclasses :forwardchaining)
(defaxiom appealstructurelistpforwardtoappealstructurelistpofcdr
(implies (appealstructurelistp x)
(appealstructurelistp (cdr x)))
:ruleclasses :forwardchaining)
(defaxiom appeallistpforwardtoappeallistpofcdr
(implies (appeallistp x aritytable)
(appeallistp (cdr x) aritytable))
:ruleclasses :forwardchaining)
(defaxiom appeallistpforwardtoappealstructurelistp
(implies (appeallistp x aritytable)
(appealstructurelistp x))
:ruleclasses :forwardchaining)
(defaxiom appealstructurelistpforwardtotruelistp
(implies (appealstructurelistp x)
(truelistp x))
:ruleclasses :forwardchaining)
(defaxiom appeallistpwhenproofp
(implies (prooflistp x database aritytable)
(appeallistp x aritytable))
:ruleclasses :forwardchaining)
(defaxiom appealpwhenproofp
(implies (proofp x database aritytable)
(appealp x aritytable))
:ruleclasses :forwardchaining)
(defthm harderrorinfcpairlsttypealist
(implies (and (prooflistp xs database aritytable)
(not (consp xs)))
(equal (proofp (car xs) database aritytable)
nil)))
#
; Historical Comment:
; Note on the Hard Error below: How might this error arise? The intuitive
; argument that it doesn't goes like this: This function is called in
; forwardchain, on something produced by by forwardchain1. But inspection of
; forwardchain1 shows that it uses typealistfcdlst to check that approved
; fc derivations are not contradictory. What can go wrong? Well, one thing
; that has gone wrong is that typealistfcdlst looks at the derivations in a
; different order than they are looked at by this function. Hence, the old
; familiar typealistclause bugaboo (order of the literals) comes into play.
; We have seen an example where forwardchain1 checked ((< 0 x) (< x 1)
; (integerp x)) and found no contradiction but then passed the reversed list to
; this function which found the contradiction and caused the hard error for the
; first time ever. Our response to that was to put a reconsidertypealist
; into typealistfcdlst. But our "proof" that this hard error never arises
; is now suspect.
(cond ((null fcpairlst) (mv nil typealist))
(t (mvlet
(mbt mbf tta fta ttree)
(assumetruefalse (car (car fcpairlst))
(cdr (car fcpairlst))
t nil typealist nil ens wrld
nil nil :fta)
(declare (ignore fta))
(cond (mbf (mv t ttree))
(mbt (fcpairlsttypealist (cdr fcpairlst)
typealist
ens wrld))
(t (fcpairlsttypealist (cdr fcpairlst)
tta
ens wrld)))))))
(defun forwardchain (cl pts forceflg donotreconsiderp wrld ens
oncepoverride state)
; We forward chain in all possible ways from clause cl. We return
; three results. The first is either t or nil indicating whether a
; contradiction was found. If so, the second result is nil and the
; third is a ttree that encodes the 'lemmas and literals used (via 'pt
; tags). If no contradiction is found, the second result is a
; typealist obtained by assuming false all of the literals of cl
; (this typealist is fully tagged with 'pt tags) plus all of the
; conclusions derived from forward chaining; the third is a list of
; fcpairs, each of the form (concl . ttree), where concl is a truth
; derived from some subset of the negations of literals of cl and
; ttree tags the :FORWARDCHAINING 'lemmas used and all parents (via
; 'pt tags).
; Note: The typealist returned assumes the falsity of every literal
; in the clause and thus is not suitable for use by rewrite. We
; return it strictly for the use of setupsimplifyclausepotlst
; and bddclause.
(mvlet
(contradictionp typealist ttree)
(typealistclause cl (ptstottreelst pts) nil nil ens wrld
nil nil)
(cond (contradictionp (mv t nil ttree))
(t (mvlet (contradictionp x)
(forwardchain1 cl
(addnewfcpotslstlst
cl nil forceflg wrld ens nil)
typealist forceflg wrld
donotreconsiderp ens oncepoverride state
nil)
(cond (contradictionp
; If a contradiction was found by forward chaining, x is the ttree that
; derives it. We need to expunge the fcderivations in x before letting
; it out of the forwardchaining module.
(mv t nil (expungefcderivations x)))
(t
; If no contradiction was found, x is an fcdlst. We need to convert it
; to a list of pairs of the form (concl . ttree), where each ttree is
; expunged of fcderivations.
(let ((fcpairlst (fcpairlst x)))
(mvlet
(contradictionp typealist)
(fcpairlsttypealist
fcpairlst typealist ens wrld)
(cond
(contradictionp
(mv t nil typealist)) ; typealist is a ttree
(t
(mvlet
(contradictionp typealist ttree)
(typealistequalityloop
typealist ens wrld
*typealistequalityloopmaxdepth*)
(cond
(contradictionp
(mv t nil ttree))
(t
(mv nil typealist
fcpairlst)))))))))))))))
; When forwardchain has done its job and produced an fcpair list,
; we will pass that list to rewriteclause. Rewriteclause rewrites
; each literal in turn, under a typealist constructed from the remaining
; literals (some of which will have been rewritten since forwardchain
; constructed the typealist returned above) and from the fcpair list.
; Here is how we construct the typealist:
(defun selectforwardchainedconclsandttrees (fcpairlst pt lits ttreelst)
; Fcpairlst is a list of pairs of the form (concl . ttree). Each ttree
; contains 'pt tags indicating the parents of concl. Pt is a parent tree.
; Consider those elements of fcpairlst, say fcpairlst', whose parents are
; disjoint from pt. While working on the literals in pt we are permitted to
; assume the truth of every concl in fcpairlst'. This function computes
; fcpairlst' and destructures it into two lists which we return in the form
; of (mv lits ttreelst). Lits and ttreelst are in 1:1 correspondence. Each
; lit is the negation of a concl in fcpairlst' and the corresponding ttree is
; the ttree for concl in fcpairlst'. Thus, lits can be thought of as a
; clause segment that can be appended to the other literals we get to assume
; false while working on pt. The ttrees in ttreelst may have 'assumption tags
; because forwarding chaining may FORCE or CASESPLIT.
(cond ((null fcpairlst) (mv lits ttreelst))
((tobeignoredp (cdr (car fcpairlst)) pt)
(selectforwardchainedconclsandttrees (cdr fcpairlst)
pt lits ttreelst))
(t (selectforwardchainedconclsandttrees
(cdr fcpairlst)
pt
(cons (dumbnegatelit (car (car fcpairlst)))
lits)
(cons (cdr (car fcpairlst))
ttreelst)))))
(defun rewriteclausetypealist (tail newclause fcpairlst rcnst wrld
potlst pt)
; We construct a type alist in which we assume (a) the falsity of every literal
; in tail except the first, (b) the falsity of every literal in newclause, and
; (c) the truth of every concl in fcpairlst that is not dependent upon
; any literal noted in the parent tree (:pt) of rcnst.
; We do this by constructing a clause containing the literals in question
; (negating the concls in fcpairlst) and calling our general purpose
; typealistclause. As of v28, we also pass in the simplifyclausepotlst
; to aid in the endeavor since typeset and assumetruefalse can now
; (weakly) use linear arithmetic.
; We return a triple, (mv contradictionp typealist ttree), where
; contradictionp is t or nil and indicates whether we derived a contradiction.
; Typealist is the constructed typealist (or nil if we got a contradiction).
; Ttree is a ttree explaining the contradiction (or nil if got no
; contradiction).
; Note: The typealist returned may contain 'assumption tags. In addition, the
; typealist may contain some 'pt tags  the conclusions derived by forward
; chaining will have their respective ttrees attached to them and these will
; have 'pt tags and could have 'assumptions. We could throw out the 'pt tags
; if we wanted  we are allowed to use everything in this typealist because
; we only put accessible assumptions in it  but we don't. We must record the
; ttrees because of the possible 'assumption tags.
(mvlet
(lits ttreelst)
(selectforwardchainedconclsandttrees fcpairlst
(access rewriteconstant rcnst :pt)
nil nil)
; Observe below that we put the forwardchained concls first. The problem that
; led us to do this was the toy example shown below (extracted from a harder
; failed proof attempt). The thm below fails if you process the literals in
; the order (append newclause (cdr tail) lits).
#
(defstub p (x) t)
(defstub r (x) t)
(defaxiom p>r
(implies (p x)
(r x))
:ruleclasses :forwardchaining)
(defstub myassoc (name l) t)
(defaxiom blob
(implies (r l)
(or (consp (myassoc name l))
(equal (myassoc name l) nil)))
:ruleclasses :typeprescription)
(thm
(implies (p l)
(or (consp (myassoc name l))
(equal (myassoc name l) nil))))
#
; As a clause the theorem is
; (implies (and (p l)
; (not (consp (myassoc name l))))
; (equal (myassoc name l) nil)).
; Consider what happens when we rewrite the conclusion assuming the hyps. We
; have (p l) and (not (consp (myassoc name l))). We do indeed forward chain
; and get (r l) also. But the (not (consp (myassoc name l))) puts the
; following pair on the typealist:
; ((myassoc name l) 1537) ; tscomplement of consp
; Thus, when we go to get the typeset of (myassoc name l) we don't even look
; at the rules about myassoc, we just return 1537.
; Three fixes are possible. First, process lits first so that (r l) is
; available when we do the (consp (myassoc name l)). Second, change typeset
; so that it uses rules about myassoc even if the term (myassoc name l) is
; bound on the typealist. Third, modify typealistclause so that it iterates
; as long as the typealist changes so that it is not important in what order
; the lits are processed. The second alternative seems potentially very slow,
; though we have done no experiments. The third alternative is hard because
; one must ignore known types on the typealist when reprocessing the lits.
; Feb 9, 1995. We are trying a version of the third alternative, with
; reconsidertypealist and the double whammy flag.
(typealistclause
(append lits newclause (cdr tail))
ttreelst ; we could extend this with newclause+(cdr tail) nils
nil ; forceflg
nil ; initial typealist
(access rewriteconstant rcnst :currentenabledstructure)
wrld
potlst pt)))
; Historical Plaque on Forward Chaining
; General purpose forward chaining was not implemented in Nqthm, although
; the linear arithmetic package and :COMPOUNDRECOGNIZER lemmas were (and
; still are) examples of forwardchaining reasoning. The first two
; implementations of general purpose forward chaining in ACL2 occurred
; last week (April 913, 1990). They were both implemented one level
; below where the current forward chaining module sits: we did forward
; chaining just before rewriting each literal of the clause, rather
; than doing all the forward chaining once and tracking dependencies.
; They were both abandoned because of inefficiency. The killer was  we
; think  the repeated duplication of forward chaining derivations. For
; example, if the clause to be rewritten was {~a ~b c1 ... ck} and an
; elaborate forward chaining tree can be built from a and b, then that
; tree was built when we began to rewrite c1 and that tree was built
; again when we began to rewrite c2, etc. In addition, the old forward
; chaining scheme did not include the idea of triggers, it forward
; chained off the first hypothesis of a :FORWARDCHAINING rule. Finally,
; the old scheme used full fledged relievehyps to relieve the other hyps
; of the rules  another potential killer but one that didn't get us
; simply because we had no forward chaining rules with more than one hyp
; in our tests.
; However, in an effort to help software archeologists (not to mention
; the possibility that we might help ourselves avoid repetition of past
; mistakes) we inscribe here an extensive comment written last week:
; The Forward Chaining Essay  Version II (This essay is of at most historic
; interest. For the current version of forward chaining, search for
; Forward Chaining from the top of this file.)
; We are about to start rewriting the current literal under the
; assumption of the negations of the literals in clauseseg. We wish to
; forward chain off of these assumptions to generate a typealist
; suitable for use during the rewriting.
; We return three values: t or nil indicating whether a contradiction was
; found while forward chaining, a new typealist, and a ttree recording
; the forwardchainingrules used.
; The form of a :FORWARDCHAINING rule is:
; (defrec forwardchainingrule
; ((rune . nume) keyhyp otherhyps . concls) nil)
; If a lemma such as
; (implies (and hyp1 hyp2 ... hypn) (and concl1 ... conclk))
; is processed as a :FORWARDCHAINING rule named name we will generate:
; (make forwardchainingrule
; :rune rune
; :nume &
; :keyhyp hyp1
; :otherhyps (hyp2 ... hypn)
; :concls (concl1 ... conclk)
; :matchfree once_or_all)
; which is stored under the 'forwardchainingrules property of the top
; function symbol of hyp1. By "top function symbol" we mean the outer
; most function symbol after stripping away any toplevel NOT.
; When we apply a forwardchainingrule we have a context defined by the
; set of assumptions off of which we are forward chaining (which is
; initially obtained by negating the literals of clauseseg) and a
; typealist encoding those assumptions. Our main result is, of course,
; the final typealist. But the set of assumptions is represented
; explicitly (indeed, somewhat elaborately) to support heuristics
; designed to avoid infinite loops while permitting the desired forward
; chaining.
; The list of assumptions is more properly thought of as the history of
; this forward chaining problem and is held in the variable fchistory.
; More on its structure later.
; Roughly speaking, one applies a :FORWARDCHAINING rule to a term, hyp1',
; as follows: unify :keyhyp with hyp1' and then relievehyps the
; :otherhyps. If those two steps do not succeed, the application fails.
; If they work, then make a heuristic decision about whether the
; resulting instance of :concls is worthwhile. If it is not, the
; application fails. If it is, add concl to the fchistory and
; typealist and say the application succeeded.
; The structure of fchistory sufficient to support our current
; heuristics has evolved from a naive structure that just listed the
; assumptions made so far. Initially, our heuristic decision was simply
; whether the candidate concl was worsethan any existing assumption.
; But imagine that among the initial hypotheses are (ASSOC & &) and
; (STATEP1 S). And imagine that some forward chaining rule lets you
; pump forward from (STATEP1 S) to (P (CDR (ASSOC & &))). Then you
; wouldn't get to use that rule because its conclusion is worse than
; (ASSOC & &). This was the first indication that worsethan alone was
; too restrictive. We fixed this by distinguishing the initial
; assumptions from those produced by forward chaining and we did the
; worsethan check only on the newly added ones.
; However, the next problem was illustrated by having two forward
; chaining rules:
; name1: (statep1 x) > (p (nth 2 state))
; name2: (statep1 x) > (p (nth 3 state)),
; that can get in eachother's way. If the first is used to add its
; conclusion then the second cannot be used because its conclusion is
; worse than that just added.
; So the structure of fchistory is now a list of pairs, each of the form
; (term . hist), where term is one of our assumptions and hist is the
; history of term. If term is among the initial assumptions, then hist
; is nil. If term was produced by the rule named name from some term'
; with history hist', then hist is (name term' . hist').
; Thus, another way to view it is that each entry in fchistory is of the
; form (term namek termk ... name2 term2 name1 term1) and means that term
; was produced by a chain of k forward chaining steps: starting with
; term1 (which is in the initial set of assumptions) use name1 to derive
; term2, use name2 to dervie term3, ..., and use namek to derive term.
; Our heuristic for deciding whether to keep a conclusion, concl, is if
; namek has not been used in this chain, keep concl; otherwise, if namek
; has been used, then concl must be worse than nor equal to no termi in
; its chain.
; It is very inefficient to repeatedly hit all the assumptions with all
; the rules until no change occurs. We have therefore taken steps to
; avoid unnecessary work. First, if a rule has been successfully applied
; to a term then there is no need to apply it again (only to learn that
; its conclusion is rejected). Second, if a conclusion has ever been
; produced before, there is no need to add it again (although technically
; it is probably possible to rederive it in a way that permits further
; chaining not permitted by the original derivation). Third, if a rule
; named name is applied to a term term with derivation d and produces a
; concl that is rejected because of its ancestry, then don't apply name
; to term and d again. To support this heuristic we have to keep track
; of the failed applications, which we do in the variable badappls.
; End of Historical Plaque
; Rockwell Addition: The nurewriter is applied to literals. So
; rewriteatm is changed below. In addition, we optionally lambda
; abstract the result. We also clean up in certain ways. New code
; extends all the way to the defun of rewriteatm.
; Essay on Lambda Abstraction
; We will do some lambda abstraction when we rewrite literals. That
; is implemented here.
; The original idea here was to expand lambdas by ordinary rewriting
; and then to fold them back up, removing duplicate occurrences of
; subterms. Consider
; ((lambda (x y) (foo x (car y) x))
; alpha
; (cons b c))
; This would normally expand to
; (foo alpha b alpha)
; Suppose alpha is very large. Then this is a problem. I will
; fold it back up, to get:
; (let* ((u alpha))
; (foo u b u))
; I have abandoned this idea as far as rewriting goes, though it
; probably still bears a closer look. But I have adopted it as an
; option for prettyprinting clauses.
; The first subproblem is identifying the common subterms (e.g.,
; alpha in (foo alpha b alpha)) to abstract away. I call this the
; multiple subterm problem.
; We say that x is a "multiple subterm" of y if x occurs more than
; once in y. We say x is a "maximal multiple subterm" of y if x is a
; multiple subterm of y and no other multiple subterm of y contains an
; occurrence of x.
; Our interest in maximal subterms is illustrated by (f (g (m x)) (g
; (m x))). (M x) is a multiple subterm. We might abstract this term
; to (let* ((v1 (m x)) (v2 (g v1))) (f v2 v2)). But if (g (m x)) is
; identified as the first multiple subterm, then we get (let ((v1 (g
; (m x)))) (f v1 v1)) and there is only one letbinding, which we
; prefer. So we wish to find a maximal multiple subterm. We will
; eliminate them one at a time. That way we will find smaller
; terms that still appear more than once. For example:
; The term (f (g (m x)) (h (m x)) (g (m x))) may give rise first
; to (let* ((v1 (g (m x)))) (f v1 (h (m x)) v1)), but upon abstracting
; that we get (let* ((v2 (m x)) (v1 (g v2))) (f v1 v2 v1)).
; We are only interested in "nonatomic" multiple subterms, i.e.,
; function applications. Our interest in nonatomic subterms is
; because otherwise we will infinitely recur ``eliminating'' multiple
; occurrences of variable symbols by introducing new variable symbols
; that occur multiple times.
; So to do lambda abstraction on term we will find a nonatomic
; maximal multiple subterm, e1, in term. If successful, we will
; replace all occurrences of e1 in term by some new variable, say v1,
; producing, say, term1. Now consider (f e1 term1), where f is some
; irrelevant madeup symbol. This term has one less nonatomic
; multiple subterm, since e1 occurs only once in it and v1 is atomic.
; Repeat the process on this term until no multiple subterms are
; found. The result is (f ek ... (f e1 termk)), which we can abstract
; to (let ((vk ek) ... (v1 e1)) termk).
; We would like to carry out this process without manufacturing the
; irrelevant function symbol f. So we are really interested in
; multiple occurrences of a term in a list of terms.
(mutualrecursion
(defun maximalmultiple (x termlst winner)
; In this definition, x is a term, but I am using it as though it were
; just the set of all of its subterms. I wish to find a nonatomic
; subterm, e, of x that is a maximal multiple subterm in the list of
; terms termlst. Winner is either nil or the maximal multiple found
; so far.
(cond
((or (variablep x)
(fquotep x))
winner)
((eq (foccurrenceslst x termlst nil) '>)
(cond ((equal winner nil) x)
((eq (foccurrences x winner t) '>) winner)
((eq (foccurrences winner x t) '>) x)
(t winner)))
(t (maximalmultiplelst (fargs x) termlst winner))))
(defun maximalmultiplelst (xlst termlst winner)
(cond ((endp xlst) winner)
(t (maximalmultiplelst (cdr xlst)
termlst
(maximalmultiple (car xlst)
termlst
winner))))))
; So, to find a nonatomic maximal multiple subterm of a single term,
; term, do (maximalmultiple term (list term) nil). More generally,
; to find a nonatomic maximal multiple in a list of terms, lst, do
; (maximalmultiple lst lst nil). If the result is nil, there is no
; such subterm. Otherwise, the result is one.
; To carry out the algorithm sketched above, we must iteratively
; find and replace the maximal multiples by new variable symbols.
(defun maximalmultiples1 (termlst newvars avoidvars pkgwitness)
(let ((e (maximalmultiplelst termlst termlst nil)))
(cond
((equal e nil)
(mv newvars termlst))
(t (let ((var (genvar pkgwitness "V"
(+ 1 (len newvars))
avoidvars)))
(maximalmultiples1
(cons e (substexpr1lst var e termlst))
(cons var newvars)
(cons var avoidvars)
pkgwitness))))))
(defun maximalmultiples (term pkgwitness)
; This function returns (mv vars terms), where terms is one longer
; than vars. Suppose vars is (v3 v2 v1) and terms is (e3 e2 e1
; term3). Then term is equivalent to
; (let* ((v3 e3) (v2 e2) (v1 e1)) term3).
; Observe that if vars is nil there are no multiple subterms and terms
; is the singleton containing term.
(maximalmultiples1 (list term) nil (allvars term) pkgwitness))
(defun lambdaabstract1 (vars terms)
(cond
((endp vars) (car terms))
(t (let* ((body (lambdaabstract1 (cdr vars) (cdr terms)))
(newvars (remove1eq (car vars) (allvars body))))
(consterm (makelambda (cons (car vars) newvars)
body)
(cons (car terms) newvars))))))
(defun lambdaabstract (term pkgwitness)
; Rockwell Addition: Nonequivalent read conditionals!
#acl2looponly ; Rockwell Addition
(cond (*lambdaabstractp*
(mvlet (vars terms)
(maximalmultiples term pkgwitness)
(lambdaabstract1 vars terms)))
(t term))
#+acl2looponly ; Rockwell Addition
(mvlet (vars terms)
(maximalmultiples term pkgwitness)
(lambdaabstract1 vars terms)))
; We also will clean up certain IFexpressions.
(defun mutuallyexclusivetests (a b)
; We return t if terms (and a b) cannot be true. We just recognize
; the case where each is (EQUAL x 'constant) for different constants.
(and (not (variablep a))
(not (fquotep a))
(eq (ffnsymb a) 'equal)
(not (variablep b))
(not (fquotep b))
(eq (ffnsymb b) 'equal)
(or (and (quotep (fargn a 1))
(quotep (fargn b 1))
(not (equal (cadr (fargn a 1)) (cadr (fargn b 1))))
(equal (fargn a 2) (fargn b 2)))
(and (quotep (fargn a 2))
(quotep (fargn b 2))
(not (equal (cadr (fargn a 2)) (cadr (fargn b 2))))
(equal (fargn a 1) (fargn b 1)))
(and (quotep (fargn a 1))
(quotep (fargn b 2))
(not (equal (cadr (fargn a 1)) (cadr (fargn b 2))))
(equal (fargn a 2) (fargn b 1)))
(and (quotep (fargn a 2))
(quotep (fargn b 1))
(not (equal (cadr (fargn a 2)) (cadr (fargn b 1))))
(equal (fargn a 1) (fargn b 2))))))
(defun mutuallyexclusivesubsumptionp (a b c)
; This is a generalized version of (if x y y). Suppose we wish to
; form (if a b c) but that b is c. Then clearly, the result is equal
; to c. Now imagine that c is (if c1 c2 c3) and that a and c1 are
; mutually exclusive. Then we could form (if c1 c2 (if a b c3))
; instead. This would be a win if it turns out that after rippling
; down we find that b is equal to ck: (if a b c) is just c.
(cond
((equal b c) t)
((and (nvariablep c)
(not (fquotep c))
(eq (ffnsymb c) 'IF)
(mutuallyexclusivetests a (fargn c 1)))
(mutuallyexclusivesubsumptionp a b (fargn c 3)))
(t nil)))
(mutualrecursion
(defun cleanupifexpr (x trues falses)
(cond
((variablep x) x)
((fquotep x) x)
((eq (ffnsymb x) 'IF)
(let ((a (cleanupifexpr (fargn x 1) trues falses)))
(cond
((quotep a)
(if (cadr a)
(cleanupifexpr (fargn x 2) trues falses)
(cleanupifexpr (fargn x 3) trues falses)))
((memberequal a trues)
(cleanupifexpr (fargn x 2) trues falses))
((memberequal a falses)
(cleanupifexpr (fargn x 3) trues falses))
(t (let ((b (cleanupifexpr (fargn x 2) (cons a trues) falses))
(c (cleanupifexpr (fargn x 3) trues (cons a falses))))
(cond ((equal b c) b)
((mutuallyexclusivesubsumptionp a b c)
c)
(t (mconsterm* 'if a b c))))))))
(t (mconsterm (ffnsymb x)
(cleanupifexprlst (fargs x) trues falses)))))
(defun cleanupifexprlst (x trues falses)
(cond ((endp x) nil)
(t (cons (cleanupifexpr (car x) trues falses)
(cleanupifexprlst (cdr x) trues falses)))))
)
(defun rewriteatm (atm notflg bkptr gstack typealist
wrld simplifyclausepotlst rcnst state)
; This function rewrites atm with nthupdaterewriter, recursively.
; Then it rewrites the result with rewrite, in the given context,
; maintaining iff.
; It is used to rewrite the atoms of a clause as we sweep across. It
; is just a call of rewrite  indeed, it didn't exist in Nqthm and
; rewrite was called in its place  except for one thing: it first
; gives typeset a chance to decide things. See the note about
; pegatelit in rewriteclause.
(mvlet (knownp nilp ttree)
(knownwhethernil atm typealist
(access rewriteconstant rcnst
:currentenabledstructure)
(oktoforce rcnst)
wrld
nil)
(cond
; Before Version 2.6 we had
; (knownp
; (cond (nilp (mv *nil* ttree))
; (t (mv *t* ttree))))
; but this allowed typeset to remove ``facts'' from a theorem which
; may be needed later. The following transcript illustrates the previous
; behavior:
#
ACL2 !>(defthm foldconstsin+
(implies (and (syntaxp (consp c))
(syntaxp (eq (car c) 'QUOTE))
(syntaxp (consp d))
(syntaxp (eq (car d) 'QUOTE)))
(equal (+ c d x)
(+ (+ c d) x))))
ACL2 !>(defthm helper
(implies (integerp x)
(integerp (+ 1 x))))
ACL2 !>(thm
(implies (integerp (+ 1/2 x))
(integerp (+ 1/2 x)))
:hints (("Goal" :use ((:instance helper
(x (+ 1/2 x)))))))
[Note: A hint was supplied for our processing of the goal above.
Thanks!]
ACL2 Warning [Use] in ( THM ...): It is unusual to :USE an enabled
:REWRITE or :DEFINITION rule, so you may want to consider disabling
(:REWRITE HELPER).
We now augment the goal above by adding the hypothesis indicated by
the :USE hint. The hypothesis can be derived from HELPER via instantiation.
The augmented goal is shown below.
Goal'
(IMPLIES (IMPLIES (INTEGERP (+ 1/2 X))
(INTEGERP (+ 1 1/2 X)))
(IMPLIES (INTEGERP (+ 1/2 X))
(INTEGERP (+ 1/2 X)))).
By case analysis we reduce the conjecture to
Goal''
(IMPLIES (AND (OR (NOT (INTEGERP (+ 1/2 X)))
(INTEGERP (+ 1 1/2 X)))
(INTEGERP (+ 1/2 X)))
(INTEGERP (+ 1/2 X))).
This simplifies, using primitive type reasoning, to
Goal'''
(IMPLIES (INTEGERP (+ 1/2 X))
(INTEGERP (+ 1/2 X))).
Normally we would attempt to prove this formula by induction. However,
we prefer in this instance to focus on the original input conjecture
rather than this simplified special case. We therefore abandon our
previous work on this conjecture and reassign the name *1 to the original
conjecture. (See :DOC otfflg.)
No induction schemes are suggested by *1. Consequently, the proof
attempt has failed.
Summary
Form: ( THM ...)
Rules: ((:DEFINITION IMPLIES)
(:DEFINITION NOT)
(:FAKERUNEFORTYPESET NIL))
Warnings: Use
Time: 0.03 seconds (prove: 0.02, print: 0.01, other: 0.00)
******** FAILED ******** See :DOC failure ******** FAILED ********
ACL2 !>
#
; Note that in the transition from Goal'' to Goal''', the needed
; fact  (INTEGERP (+ 1 1/2 X))  was removed by type reasoning.
; This is not good. We now only use type reasoning at this point if
; it will give us a win.
; One might ask why we only disallow typeset from removing facts here.
; Why not elswhere, and what about rewrite? We do it this way because
; it is only here that the user cannot prevent this removal from
; happening by manipulating the enabled structure.
((and knownp notflg nilp)
; So we have reduced the atm to nil but it occurs negated in the
; clause and so we have reduced the literal to t, proving the clause.
; So we report this reduction.
(mv *nil* ttree))
((and knownp (not notflg) (not nilp))
(mv *t* ttree))
(t
(mvlet
(hitp atm1 ttree1)
; Rockwell Addition
(cond
((eq (nurewritermode wrld) :literals)
(nthupdaterewriter t atm nil
(access rewriteconstant rcnst
:currentenabledstructure)
wrld state))
(t (mv nil nil nil)))
(let ((atm2 (if hitp
(lambdaabstract
(cleanupifexpr atm1 nil nil)
(pkgwitness (currentpackage state)))
atm)))
(mvlet (ans1 ans2)
(rewriteentry
(rewrite atm2
nil
bkptr)
:typealist typealist
:obj '?
:geneqv *geneqviff*
:wrld wrld
:fnstack nil
:ancestors nil
:backchainlimit (backchainlimit wrld)
:simplifyclausepotlst simplifyclausepotlst
:rcnst rcnst
:gstack gstack
:ttree (if hitp ttree1 nil)
:rdepth (rewritestacklimit wrld))
(mv ans1 ans2))))))))
; Now we develop the functions for finding trivial equivalence hypotheses and
; stuffing them into the clause, transforming {(not (equal n '27)) (p n x)},
; for example, into {(p '27 x)} and running p if x is constant too.
(mutualrecursion
(defun everyoccurrenceequivhittablep1
(equiv old geneqv term inhideflg ens wrld)
; This function determines whether every occurrence of old in term is ``equiv
; hittable'' while maintaining geneqv. This is just an optimization of a call
; to substequivexpr followed by an occur check.
; NOTE: We ignore occurrences of old inside arguments to HIDE.
(cond ((equal term old)
; If term is old, then we return nonnil or nil according to whether
; equiv refines geneqv. If it does refine geneqv, this occurrence
; will be hit; if not, this occurrence won't be hit. Actually, if
; we are inside a call of hide then this occurrence won't be hit
; either way.
(and (not inhideflg)
(geneqvrefinementp equiv geneqv wrld)))
((or (variablep term)
(fquotep term))
; If term is different from old and doesn't contain old, e.g., term is a
; variable or a quote, then all occurrences of old in term are equiv
; hittable. Hide is handled below.
t)
(t (everyoccurrenceequivhittablep1listp
equiv
old
(geneqvlst (ffnsymb term)
geneqv
ens
wrld)
(fargs term)
(or inhideflg
(eq (ffnsymb term) 'hide))
ens wrld))))
(defun everyoccurrenceequivhittablep1listp
(equiv old geneqvlst args inhideflg ens wrld)
(cond ((null args) t)
(t (and
(everyoccurrenceequivhittablep1
equiv old
(car geneqvlst)
(car args)
inhideflg
ens wrld)
(everyoccurrenceequivhittablep1listp
equiv old
(cdr geneqvlst)
(cdr args)
inhideflg
ens wrld)))))
)
(defun everyoccurrenceequivhittablep (equiv old geneqv term ens wrld)
; This function determines whether every occurrence of old in term is ``equiv
; hittable'' while maintaining geneqv. This means that (substequivexpr equiv
; new old genequv term ens wrld state ttree) will remove all occurrences of old
; from term (assuming there are no occurrences of old in new and old is a
; variable).
; We here enforce the rule that we don't know how to substitute for explicit
; constants. We also build in the fact that everything is equalhittable
; (i.e., equal refines all equivalence relations).
; NOTE: We ignore occurrences of old inside arguments to HIDE.
(cond
((and (nvariablep old)
(fquotep old))
(substexprerror old))
((eq equiv 'equal) t)
(t (everyoccurrenceequivhittablep1 equiv old geneqv term nil ens wrld))))
(defun everyoccurrenceequivhittablepinclausep (equiv old cl ens wrld)
; This checks that every occurrence of old in cl is equiv hittable
; while maintaining 'iff on each literal. This is just a special case
; in which we are checking everyoccurrenceequivhittablep1listp where
; geneqvlst is a list, as long as cl, of *geneqviff*s. Rather than
; manufacture the suitable geneqvlst we just supply *geneqviff* as
; needed.
(cond ((null cl) t)
(t (and
(everyoccurrenceequivhittablep1
equiv old
*geneqviff*
(car cl)
nil
ens wrld)
(everyoccurrenceequivhittablepinclausep
equiv old (cdr cl) ens wrld)))))
(mutualrecursion
(defun someoccurrenceequivhittablep1 (equiv old geneqv term ens wrld)
; This function determines whether there exists an equivhittable occurrence of
; old in term maintaining geneqv.
(cond ((equal term old)
; If term is old, then we return nonnil or nil according to whether
; equiv refines geneqv. If it does refine geneqv, this occurrence
; will be hit; if not, this occurrence won't be hit.
(geneqvrefinementp equiv geneqv wrld))
((or (variablep term)
(fquotep term)
(eq (ffnsymb term) 'hide))
; If term is different from old and doesn't contain old, e.g., term is
; a variable or a quote, then there is no occurrence of old in term.
; Calls of hide are included, since substitution (substequivexpr)
; does not go inside calls of hide.
nil)
(t (someoccurrenceequivhittablep1listp
equiv
old
(geneqvlst (ffnsymb term)
geneqv
ens
wrld)
(fargs term)
ens wrld))))
(defun someoccurrenceequivhittablep1listp
(equiv old geneqvlst args ens wrld)
(cond ((null args) nil)
(t (or
(someoccurrenceequivhittablep1
equiv old
(car geneqvlst)
(car args)
ens wrld)
(someoccurrenceequivhittablep1listp
equiv old
(cdr geneqvlst)
(cdr args)
ens wrld)))))
)
(defun someoccurrenceequivhittablep (equiv old geneqv term ens wrld)
; This function determines whether some occurrence of old in term is ``equiv
; hittable'' while maintaining geneqv. This means that (substequivexpr equiv
; new old geneqv term ens wrld state ttree) changes term.
; We here enforce the rule that we don't know how to substitute for explicit
; constants.
; NOTE: We ignore occurrences of old inside arguments to HIDE.
(cond
((and (nvariablep old)
(fquotep old))
(substexprerror old))
(t (someoccurrenceequivhittablep1 equiv old geneqv term ens wrld))))
(defun equivhittableinsomeotherlit (equiv term n cl i ens wrld)
; We determine whether term occurs in an equivhittable slot (maintaining iff)
; in some lit of clause cl other than the nth. The number of the first literal
; of cl is i.
(cond ((null cl) nil)
((int= n i)
(equivhittableinsomeotherlit equiv term n (cdr cl) (1+ i) ens wrld))
((someoccurrenceequivhittablep equiv term *geneqviff* (car cl) ens wrld)
t)
(t (equivhittableinsomeotherlit equiv term n (cdr cl) (1+ i) ens wrld))))
(defun findtrivialequivalence1
(notjustquotepflg tail i cl ens wrld avoidlst)
; Cl is a clause. Tail is a tail of cl and i is the position number
; of its first literal, starting from 0 for the first lit in cl. See
; findtrivialequivalence for the rest of the spec.
; It is important to keep in mind that the clause upon which we are working has
; not necessarily been rewritten. Indeed, it is often the product of previous
; substitutions by the driver of this very function. (Aside: once upon a time,
; the driver did not evaluate literals as they got stuffed with constants. At
; the moment it does evaluate enabled fns on constant args. But that may
; change and so this function is written in a way that assumes the worst: there
; may be reducible terms in the clause.) Thus, for example, a clause like
; {(not (equal x 'a)) (not (equal y 'b)) (not (equal x y)) y ...}
; may first produce
; {(not (equal y 'b)) (not (equal 'a y)) y ...}
; and then
; {(not (equal 'a 'b)) 'b ...}
; which contains two unexpected sorts of literals: an equivalence with constant
; args and a constant literal. We must therefore not be surprised by such
; literals. However, we do not expect them to arise often enough to justify
; making our caller cope with the possibility that we've proved the clause. So
; if we find such a literal and can decide the clause, we will just immediately
; report that there are no more usable equivalences and let the simplifier
; rediscover the literal. If we find such a literal and can't decide the
; clause quickly based on equal and iff facts (we are not going to eval
; userdefined equivs) then we will just continue looking for usable
; equivalences. The idea is that if the discovered lit makes the clause true,
; we don't expect to have screwed it up by continuing to substitute; and if the
; discovered lit just drops out, then our continued substitution is what we
; should have done. (Aside: If we persist in our decision to reduce literals
; when they are suffed with constants, then these cases will not arise and all
; of the above is irrelevant.)
; Recall our output spec from findtrivialequivalence. The six results we
; return are the name of the condition detected (disposable or keeper), the
; location i of the literal, equiv, lhs, rhs and the literal itself. Otherwise
; we return 6 nils. (When we succeed, the "lhs" of our result is the term for
; which we are to substitute and "rhs" is the term by which we replace lhs.
; They may in fact come from the opposite sides of the equivalence term.)
(cond ((null tail) (mv nil nil nil nil nil nil))
((memberequal (car tail) avoidlst)
(findtrivialequivalence1
notjustquotepflg (cdr tail) (1+ i) cl ens wrld avoidlst))
; Handle variable V as though it is the literal (not (equal V nil)).
((quotep (car tail))
; If the discovered lit is nil, then we just ignore it because it will drop
; out. If the discovered lit is nonnil, this clause is true. So we signal
; that there are no more usable equivs and let the simplifier get its hands
; on the clause to rediscover that it is true.
(if (equal (car tail) *nil*)
(findtrivialequivalence1
notjustquotepflg (cdr tail) (1+ i) cl ens wrld avoidlst)
(mv nil nil nil nil nil nil)))
((or (variablep (car tail))
(and (eq (ffnsymb (car tail)) 'not)
(or (variablep (fargn (car tail) 1))
(and (not (fquotep (fargn (car tail) 1)))
(equivalencerelationp (ffnsymb (fargn (car tail) 1)) wrld)))))
(let* ((atm
(if (variablep (car tail))
(fconsterm* 'equal (car tail) *nil*)
(fargn (car tail) 1)))
(equiv (if (variablep atm)
'iff
(ffnsymb atm)))
(lhs (if (variablep atm)
atm
(fargn atm 1)))
(rhs (if (variablep atm)
*t*
(fargn atm 2))))
; We have discovered an equiv hyp (not (equiv lhs rhs)) that is not on avoidlst.
(cond ((and (quotep lhs)
(quotep rhs))
; Oh! It has constant args. If equiv is equal we decide which way this lit
; goes and act accordingly, as we did for a quotep lit above. If the equiv is
; not equal then we just assume this lit will eventually drop out (we bet it is
; nil) and go on looking for other usable equivs before giving the result to
; the simplifier to decide.
(cond ((eq equiv 'equal)
(if (equal lhs rhs)
(findtrivialequivalence1
notjustquotepflg
(cdr tail) (1+ i) cl ens wrld avoidlst)
(mv nil nil nil nil nil nil)))
(t (findtrivialequivalence1
notjustquotepflg
(cdr tail) (1+ i) cl ens wrld avoidlst))))
; So below we know that if one side is a quotep then the other side is not (but
; we don't yet know that either side is a quotep). Observe that if one side is
; a quotep we are always safe in answering that we can equiv substitute for the
; other side and it is only a question of whether we have a disposable lit or a
; keeper.
((and notjustquotepflg
(variablep lhs)
(everyoccurrenceequivhittablepinclausep
equiv lhs cl ens wrld)
(not (dumboccur lhs rhs)))
; The 'disposable condition is met: lhs is an everywhere hittable variable not in rhs.
; But it could be that rhs is also an everywhere hittable variable not in lhs.
; If so, we'll substitute the termorder smaller for the bigger just so the
; user knows which way the substitutions will go.
(cond ((and (variablep rhs)
(everyoccurrenceequivhittablepinclausep
equiv rhs cl ens wrld))
(cond
((termorder lhs rhs)
(mv 'disposable i equiv rhs lhs (car tail)))
(t (mv 'disposable i equiv lhs rhs (car tail)))))
(t (mv 'disposable i equiv lhs rhs (car tail)))))
((and notjustquotepflg
(variablep rhs)
(everyoccurrenceequivhittablepinclausep
equiv rhs cl ens wrld)
(not (dumboccur rhs lhs)))
; This is the case symmetric to that above.
(mv 'disposable i equiv rhs lhs (car tail)))
((and (quotep rhs) ; thus lhs is a nonquotep
(equivhittableinsomeotherlit equiv lhs i cl 0 ens wrld))
; The 'keeper conditions are met: lhs is a nonquote with at least one
; equivhittable occurrence in another lit and rhs is a quote. Note that in
; the case that notjustquotepflg is nil, we might be giving the ``wrong''
; first answer, since if lhs is a variable then 'keeper should be 'disposable.
; However, if notjustquotepflg is nil, then we will be ignoring that answer
; anyhow; see the call of substequivandmaybedeletelit in
; removetrivialequivalences.
(mv 'keeper i equiv lhs rhs (car tail)))
((and (quotep lhs) ; thus rhs is a nonquotep
(equivhittableinsomeotherlit equiv rhs i cl 0 ens wrld))
(mv 'keeper i equiv rhs lhs (car tail)))
(t (findtrivialequivalence1
notjustquotepflg
(cdr tail) (1+ i) cl ens wrld avoidlst)))))
(t (findtrivialequivalence1
notjustquotepflg
(cdr tail) (1+ i) cl ens wrld avoidlst))))
(defun findtrivialequivalence (notjustquotepflg cl ens wrld avoidlst)
; We look for a literal of cl of the form (not (equiv lhs rhs)) where
; either of two conditions apply.
; name condition
; disposable: lhs is a variable, all occurrences of lhs in cl
; are equivhittable, and rhs does not contain lhs.
; keeper: lhs is any nonquotep and rhs is a quotep and lhs has
; an equivhittable occurrence in some other literal
; of the clause
; Note that in the keeper case, there may be some nonhittable occurrences of
; lhs in the clause. In addition, we accept commuted version of the equivalence
; and we treat each variablep literal, var, as the trivial equivalence (not
; (equal var 'NIL)).
; If we find such a literal we return 6 values: the name of the condition
; detected, the location i of the literal, equiv, lhs, rhs and the literal
; itself. Otherwise we return 6 nils.
; The driver of this function, removetrivialequivalences, will substitute rhs
; for lhs throughout cl, possibly delete the literal, and then call us again to
; look for the next trivial equivalence. This raises a problem. If the driver
; doesn't delete the literal, then we will return the same one again and loop.
; So the driver supplies us with a list of literals to avoid, avoidlst, and
; will put onto it each of the literals that has been used but not deleted.
; So consider a clause like
; (implies (and (equal (foo b) 'evg) [1]
; (equal a b)) [2]
; (p (foo a) (foo b)))
; The first trivial equivalence is [1]. The driver substitutes 'evg
; for (foo b) but doesn't delete the literal. So we get:
; (implies (and (equal (foo b) 'evg) [1]
; (equal a b)) [2]
; (p (foo a) 'evg))
; and the admotion against using (equal (foo b) 'evg). But now we see
; [2] and the driver substitutes a for b (because a is smaller) and deletes
; [2]. So we get:
; (implies (equal (foo a) 'evg) [1]
; (p (foo a) 'evg))
; and the old admotion against using (equal (foo b) 'evg). Here we find [1]
; ``again'' because it is no longer on the list of things to avoid. Indeed, we
; can even use it to good effect. Of course, once it is used both it and the
; old avoided literal are to be avoided.
; So can this loop? No. Every substitution reduces termorder.
(findtrivialequivalence1 notjustquotepflg cl 0 cl ens wrld avoidlst))
(defun addliteralandpt1 (cltail pt cl ptlst)
; Imagine that lit is a literal with pt as its parent tree. Cl is a clause and
; the parent tree of each literal is given by the corresponding element of
; ptlst. We were about to add lit to cl when we noticed that lit (possibly
; commuted) is already an element of cl, namely the one in the car of cltail,
; which is a tail of cl. Thus, we wish to update ptlst so that the
; corresponding parent tree in the new ptlst includes pt.
(cond
((null cl)
(er hard 'addliteralandpt1 "We failed to find the literal!"))
((equal cltail cl)
(cond ((null (car ptlst)) (cons pt (cdr ptlst)))
(t (cons (cons pt (car ptlst)) (cdr ptlst)))))
(t (cons (car ptlst)
(addliteralandpt1 cltail pt (cdr cl) (cdr ptlst))))))
(defun addliteralandpt (lit pt cl ptlst ttree)
; Very roughly speaking, this is just:
; (mv (addliteral lit cl nil) ; add lit to clause cl
; (cons pt ptlst) ; add lit's parent tnree to ptlst
; ttree) ; and pass up the ttree
; But it is complicated by the fact that the addliteral might not actually
; cons lit onto cl but reduce the clause to {t} or merge the literal with
; another. If that happened and we had actually used the code above, then the
; ptlst returned would no longer be in 1:1 correspondence with the new
; clause.
(cond
((quotep lit)
(cond ((equal lit *nil*) (mv cl ptlst ttree))
(t (mv *trueclause* nil ttree))))
((or (equal cl *trueclause*)
(membercomplementterm lit cl))
(mv *trueclause* nil ttree))
(t (let ((cl0 (memberterm lit cl)))
(cond
((null cl0)
(mv (cons lit cl)
(cons pt ptlst)
ttree))
((null pt)
(mv cl ptlst ttree))
(t (mv cl
(addliteralandpt1 cl0 pt cl ptlst)
ttree)))))))
(defun substequivandmaybedeletelit
(equiv new old n cl i ptlst deleteflg ens wrld state ttree)
; Substitutes new for old (which are equiv) in every literal of cl (maintaining
; iff) except the nth one. The nth literal is deleted if deleteflg is t and
; is skipped but included in the if deleteflg is nil. Ptlst is in 1:1
; correspondence with cl. We return the new clause, a new ptlst and a ttree
; recording the congruence and executable counterpart rules used. It is
; possible that this fn will return a clause dramatically shorter than cl,
; because lits may evaporate upon evaluation or merge with other literals. We
; may also prove the clause.
(cond
((null cl) (mv nil nil ttree))
((int= n i)
(mvlet (cl1 ptlst1 ttree)
(substequivandmaybedeletelit equiv new old n
(cdr cl) (1+ i)
(cdr ptlst)
deleteflg
ens wrld state ttree)
(cond
(deleteflg (mv cl1 ptlst1 ttree))
(t (addliteralandpt (car cl) (car ptlst)
cl1 ptlst1 ttree)))))
((dumboccur old (car cl))
(mvlet (hitp lit ttree)
(substequivexpr equiv new old
*geneqviff*
(car cl)
ens wrld state ttree)
(declare (ignore hitp))
; Hitp may be nil even though old occurs in the lit, because it may not occur
; in an equivhittable place. But we don't really care whether it's t or nil.
(mvlet (cl1 ptlst1 ttree)
(substequivandmaybedeletelit equiv new old n
(cdr cl) (1+ i)
(cdr ptlst)
deleteflg
ens wrld state ttree)
(addliteralandpt lit (car ptlst)
cl1 ptlst1 ttree))))
(t (mvlet (cl1 ptlst1 ttree)
(substequivandmaybedeletelit equiv new old n
(cdr cl) (1+ i)
(cdr ptlst)
deleteflg
ens wrld state ttree)
(addliteralandpt (car cl) (car ptlst)
cl1 ptlst1 ttree)))))
(defun removetrivialequivalences
(cl ptlst removeflg ens wrld state ttree hitp avoidlst)
; This function looks for two kinds of equivalence hypotheses in cl and uses
; them to do substitutions. By "equivalence hypothesis" we mean a literal of
; the form (not (equiv lhs rhs)) that is not on avoidlst. The two kinds are
; called "trivial var equivalences" and "trivial quote equivalences." If we
; find an equation of the first sort we substitute one side for the other and
; delete the equivalence (provided removeflg is t). If we find an equation of
; the second sort, we substitute one side for the other but do not delete the
; equivalence. See findtrivialequivalence for more details, especially
; concerning avoidlst. Hitp is an accumulator that records whether we did
; anything.
; Ptlst is a list of parent trees in 1:1 correspondence with cl. Since we
; return a modified version of cl in which some literals may have been deleted,
; we must also return a modified version of ptlst giving the parent trees for
; the surviving literals.
; The justification for deleting (not (equiv var term)) when var occurs nowhere
; in the clause is (a) it is always sound to throw out a literal, and (b) it is
; heuristically safe here because var is isolated and equiv is reflexive: if
; (implies (equiv var term) p) is a theorem so is p because (equiv term term).
; We return four values: hitp, cl, ptlst and ttree.
; No Change Loser.
; Note: We have briefly considered the question of whether we should do
; anything with hypotheses of the form (equiv var term), where var does not
; occur in term, and some (but not all) occurrences of var are equivhittable.
; Perhaps we should hit those occurrences but not delete the hypothesis? We
; think not. After all, if term is larger than var (as it generally is here),
; why should we replace some occurrences of the small term by the big one?
; They will just be zapped back by rewritesolidify if the hyp is not deleted.
; However, an exception to this rule is if we see a hypothesis of the form
; (equal lhs 'const) where not every occurrence of lhs is equivhittable.
; Such a hyp is not a trivial var equivalence, even if lhs is a variable,
; because of the unhittable occurrence of var. But we do count it as a
; trivial quote equivalence and hit var where we can (but don't delete the
; hypothesis).
(mvlet (condition litposition equiv lhs rhs lit)
(findtrivialequivalence removeflg cl ens wrld avoidlst)
(cond
(litposition
(mvlet (newcl newptlst ttree)
(substequivandmaybedeletelit
equiv rhs lhs litposition cl 0 ptlst
(and removeflg (eq condition 'disposable))
ens wrld state ttree)
(removetrivialequivalences newcl newptlst removeflg
ens wrld state
ttree t
(cons lit avoidlst))))
(t (mv hitp cl ptlst ttree)))))
; In a break with nqthm, we implement a really trivial theorem prover which
; gets the first shot at any conjecture we have to prove. The idea is to build
; into this function whatever is necessary for bootstrap to work. It will
; also speed up the acceptance of commonly used recursive schemas. The idea is
; simply to recognize instances of a small number of known truths, stored in
; clausal form on the world global 'builtinclauses, whose initial value is
; set up below.
; To be predictable, we have to include commutative variants of the
; recognized clauses. In addition, because subsumption works by first
; trying to find (an instance of) the first literal and then trying to
; find the rest, it is faster to put the most unusual literal first in
; each builtin clause.
(defrec builtinclause ((nume . allfnnames) clause . rune) t)
; Note: The :allfnnames field must be set as it would be by
; allfnnamessubsumer. This setting cannot be done automatically because we
; do not know the initial world until we have set up the builtinclauses. But
; we do check, with chkinitialbuiltinclauses which is called and reported
; in checkbuiltinconstants, that the setting below is correct for the actual
; initial world. When adding new records, it is best to use
; (allfnnamessubsumer cl (w state)) to get the :allfnnames field below.
;; RAG  I changed the clauses about e0ord< [v28 and beyond: o<] reducing on
;; complexrationalps to reducing on any complexp.
(defconst *initialbuiltinclauses*
(list
; acl2count is an ordinal.
(make builtinclause
:nume nil
:rune *fakeruneforanonymousenabledrule*
:clause '((op (acl2count x)))
:allfnnames '(op acl2count))
; Car and cdr decrease on consps.
(make builtinclause
:nume nil
:rune *fakeruneforanonymousenabledrule*
:clause '((o< (acl2count (car x))
(acl2count x))
(not (consp x)))
:allfnnames '(acl2count car o< consp not))
(make builtinclause
:nume nil
:rune *fakeruneforanonymousenabledrule*
:clause '((o< (acl2count (cdr x))
(acl2count x))
(not (consp x)))
:allfnnames '(acl2count cdr o< consp not))
; Car and cdr decrease on nonatoms.
(make builtinclause
:nume nil
:rune *fakeruneforanonymousenabledrule*
:clause '((o< (acl2count (car x))
(acl2count x))
(atom x))
:allfnnames '(acl2count car o< atom))
(make builtinclause
:nume nil
:rune *fakeruneforanonymousenabledrule*
:clause '((o< (acl2count (cdr x))
(acl2count x))
(atom x))
:allfnnames '(acl2count cdr o< atom))
; Car and cdr decrease on nonendps.
(make builtinclause
:nume nil
:rune *fakeruneforanonymousenabledrule*
:clause '((o< (acl2count (car x))
(acl2count x))
(endp x))
:allfnnames '(acl2count car o< endp))
(make builtinclause
:nume nil
:rune *fakeruneforanonymousenabledrule*
:clause '((o< (acl2count (cdr x))
(acl2count x))
(endp x))
:allfnnames '(acl2count cdr o< endp))
; 1 decreases on positives and on nonnegatives other than 0. But we
; represent (1 x) three different ways: (1 x), (+ x 1) and (+ 1 x). And to
; say "other than 0" we can use (not (zp x)) or (integerp x) together
; with the negations of any one of (equal x 0), (= x 0) or (= 0 x). The
; symmetry of equal is built into unification, but not so =, so we have
; two versions for each =.
; However, in Version 1.8 we made 1 a macro. Therefore, we have deleted the
; two builtinclauses for 1. If we ever make 1 a function again, we should
; add them again.
(make builtinclause
:nume nil
:rune *fakeruneforanonymousenabledrule*
:clause '((o< (acl2count (binary+ x '1))
(acl2count x))
(zp x))
:allfnnames '(acl2count o< zp))
(make builtinclause
:nume nil
:rune *fakeruneforanonymousenabledrule*
:clause '((o< (acl2count (binary+ '1 x))
(acl2count x))
(zp x))
:allfnnames '(acl2count o< zp))
(make builtinclause
:nume nil
:rune *fakeruneforanonymousenabledrule*
:clause '((o< (acl2count (binary+ x '1))
(acl2count x))
(not (integerp x))
(not (< '0 x)))
:allfnnames '(acl2count o< integerp < not))
(make builtinclause
:nume nil
:rune *fakeruneforanonymousenabledrule*
:clause '((o< (acl2count (binary+ x '1))
(acl2count x))
(not (integerp x))
(< x '0)
(= x '0))
:allfnnames '(acl2count o< integerp not < =))
(make builtinclause
:nume nil
:rune *fakeruneforanonymousenabledrule*
:clause '((o< (acl2count (binary+ x '1))
(acl2count x))
(not (integerp x))
(< x '0)
(= '0 x))
:allfnnames '(acl2count o< integerp not < =))
(make builtinclause
:nume nil
:rune *fakeruneforanonymousenabledrule*
:clause '((o< (acl2count (binary+ x '1))
(acl2count x))
(not (integerp x))
(< x '0)
(equal x '0))
:allfnnames '(acl2count o< integerp not < equal))
(make builtinclause
:nume nil
:rune *fakeruneforanonymousenabledrule*
:clause '((o< (acl2count (binary+ '1 x))
(acl2count x))
(not (integerp x))
(not (< '0 x)))
:allfnnames '(acl2count o< integerp < not))
(make builtinclause
:nume nil
:rune *fakeruneforanonymousenabledrule*
:clause '((o< (acl2count (binary+ '1 x))
(acl2count x))
(not (integerp x))
(< x '0)
(= x '0))
:allfnnames '(acl2count o< integerp not < =))
(make builtinclause
:nume nil
:rune *fakeruneforanonymousenabledrule*
:clause '((o< (acl2count (binary+ '1 x))
(acl2count x))
(not (integerp x))
(< x '0)
(= '0 x))
:allfnnames '(acl2count o< integerp not < =))
(make builtinclause
:nume nil
:rune *fakeruneforanonymousenabledrule*
:clause '((o< (acl2count (binary+ '1 x))
(acl2count x))
(not (integerp x))
(< x '0)
(equal x '0))
:allfnnames '(acl2count o< integerp not < equal))
; Realpart and imagpart decrease on complexps.
#+:nonstandardanalysis
(make builtinclause
:nume nil
:rune *fakeruneforanonymousenabledrule*
:clause '((o< (acl2count (realpart x))
(acl2count x))
(not (complexp x)))
:allfnnames
'(acl2count realpart o< complexp not))
#:nonstandardanalysis
(make builtinclause
:nume nil
:rune *fakeruneforanonymousenabledrule*
:clause '((o< (acl2count (realpart x))
(acl2count x))
(not (complexrationalp x)))
:allfnnames
'(acl2count realpart o< complexrationalp not))
#+:nonstandardanalysis
(make builtinclause
:nume nil
:rune *fakeruneforanonymousenabledrule*
:clause '((o< (acl2count (imagpart x))
(acl2count x))
(not (complexp x)))
:allfnnames
'(acl2count imagpart o< complexp not))
#:nonstandardanalysis
(make builtinclause
:nume nil
:rune *fakeruneforanonymousenabledrule*
:clause '((o< (acl2count (imagpart x))
(acl2count x))
(not (complexrationalp x)))
:allfnnames
'(acl2count imagpart o< complexrationalp not))
; Finally, cdr decreases on nonnil truelistps, but we can say
; "nonnil" as (eq x nil), (eq nil x), (null x) or (equal x nil)
(make builtinclause
:nume nil
:rune *fakeruneforanonymousenabledrule*
:clause '((o< (acl2count (cdr x))
(acl2count x))
(not (truelistp x))
(eq x 'nil))
:allfnnames '(acl2count cdr o< truelistp not eq))
(make builtinclause
:nume nil
:rune *fakeruneforanonymousenabledrule*
:clause '((o< (acl2count (cdr x))
(acl2count x))
(not (truelistp x))
(null x))
:allfnnames '(acl2count cdr o< truelistp not null))
(make builtinclause
:nume nil
:rune *fakeruneforanonymousenabledrule*
:clause '((o< (acl2count (cdr x))
(acl2count x))
(not (truelistp x))
(eq 'nil x))
:allfnnames '(acl2count cdr o< truelistp not eq))
(make builtinclause
:nume nil
:rune *fakeruneforanonymousenabledrule*
:clause '((o< (acl2count (cdr x))
(acl2count x))
(not (truelistp x))
(equal x 'nil))
:allfnnames '(acl2count cdr o< truelistp not equal))))
(defun builtinclausep2 (biclst cl fns ens)
(cond ((null biclst) nil)
((and (enablednumep (access builtinclause (car biclst) :nume)
ens)
(subsetpeq (access builtinclause (car biclst) :allfnnames)
fns)
(eq (subsumes *initsubsumescount*
(access builtinclause (car biclst) :clause)
cl nil)
t))
(access builtinclause (car biclst) :rune))
(t (builtinclausep2 (cdr biclst) cl fns ens))))
(defun builtinclausep1 (bicalist cl fns ens)
; Bicalist is the alist of builtin clauses, organized via top fnname. Cl is
; a clause and fns is the allfnnameslst of cl. This function is akin to
; somemembersubsumes in the sense of some builtin clause subsumes cl. We
; only try subsumption on enabled builtin clauses whose :allfnnames field is
; a subset of fns. We return the rune of the subsuming clause, or nil.
(cond ((null bicalist) nil)
((or (null (caar bicalist))
(membereq (caar bicalist) fns))
; All the builtin clauses in this pot have the same topfnname and that name
; occurs in cl. So these guys are all candidate subsumers. Note: if (car
; bicalist) is null then this is the special pot into which we have put all
; the builtin clauses that have no "function symbols" in them, as computed by
; allfnnamessubsumer. I don't see how this can happen, but if it does we're
; prepared!
(or (builtinclausep2 (cdr (car bicalist)) cl fns ens)
(builtinclausep1 (cdr bicalist) cl fns ens)))
(t (builtinclausep1 (cdr bicalist) cl fns ens))))
(defun possibletrivialclausep (cl)
(if (null cl)
nil
(mvlet (notflg atm)
(stripnot (car cl))
(declare (ignore notflg))
; Keep the following list of function names in sync with those in tautologyp.
; It should be, in fact, just the list in tautologyp plus IF and NOT. Note
; that although tautologyp does not expand NOT, iftautologyp (and hence
; tautologyp) knows about NOT, so we look for it here.
(or (ffnnamesp '(if not
iff
;not
implies eq atom eql = /= null
; If we ever make 1+ and 1 functions again, they should go back on this list.
zerop
plusp minusp listp prog2$ mustbeequal time$
withprovertimelimit force casesplit
doublerewrite)
atm)
(possibletrivialclausep (cdr cl))))))
(defun disjoin2 (t1 t2)
; We return a term IFFequiv (but not EQUAL) to (OR t1 t2). For example,
; if t1 is 'A and t2 is 'T, then we return 'T but (OR t1 t2) is 'A.
(cond ((equal t1 *t*) *t*)
((equal t2 *t*) *t*)
((equal t1 *nil*) t2)
((equal t2 *nil*) t1)
(t (mconsterm* 'if t1 *t* t2))))
(defun disjoin (lst)
(cond ((null lst) *nil*)
((null (cdr lst)) (car lst))
(t (disjoin2 (car lst) (disjoin (cdr lst))))))
(defun trivialclausep (cl wrld)
(or (memberequal *t* cl)
(and (possibletrivialclausep cl)
(tautologyp (disjoin cl) wrld))))
(defun builtinclausep (cl ens matchfreeoverride wrld state)
; We return two results. The first indicates whether cl is a ``built
; in clause,'' i.e., a known truth. The second is the supporting
; ttree (or nil). This ttree is guaranteed to be assumptionfree.
; Once upon a time, this function used forceflg = t in the
; typealistclause call below. Thus, the callers of this function
; anticipate splitting. We have backed off forceflg = t here because
; it seems likely to cause loops due to assuming literals that are
; explicitly denied later in the clause (see the warning in
; typealistclause). But this condition has never been witnessed and
; the change was made without significant testing of the forceflg = t
; case. However, the callers of this function do not now anticipate
; the presence of 'assumption tags in the ttree. Thus, if you make
; this function force or casesplit, you must change its callers!
; Starting with Version_2.7, this function uses forwardchaining. This idea
; arose when changing translatedeclarationtoguard to output calls of
; signedbytep, unsignedbytep, and integerrangep. Suddenly some guards
; proofs needed to be done that formerly were handled by builtinclausep. But
; that problem is reduced or eliminated when we forwardchain and have suitable
; forwardchaining rules from those new predicates.
; When this function is allowed to return t, it is also allowed to return nil.
; In particular, the limit on onewayunify1 calls in the call of subsumes in
; builtinclausep2 can cause this predicate to fail.
(cond ((trivialclausep cl wrld) (mv t nil))
(t (let ((rune (builtinclausep1 (globalval 'builtinclauses wrld)
cl
(allfnnameslst cl)
ens)))
(cond
(rune (mv t (pushlemma rune nil)))
(t (mvlet (contradictionp typealist ttree)
(forwardchain cl
nil ; pts
nil ; oktoforce
nil ; donotreconsiderp
wrld
ens
matchfreeoverride
state)
(declare (ignore typealist))
(cond ((not contradictionp)
(mv nil nil))
((taggedobject 'assumption ttree)
(mv (er hard 'builtinclausep
"It was thought that the forwardchain ~
call in this function could not ~
produce an 'assumption but it did! ~
Try running forwardchain on ~x0. ~
The ens and wrld used here must be ~
recovered by other means if (ens ~
state) and (w state) don't work."
(kwote cl))
nil))
(t (mv t ttree))))))))))
(defun crunchclausesegments1 (seg1 pts1 cl pts)
; This function reverses seg1 and appends it to cl, and does the analogous
; thing to pts1 and pts. However, if a literal in seg1 already occurs in
; cl, it is merged into that literal and its pt is consed onto the
; pt of the literal in cl.
; Note: It is a mystery how the opportunity for this merging should arise. It
; appears to be impossible because seg1 was rewritten under the assumption of
; the falsity of the literals in cl and hence any such literal of seg1 would
; have evaporated. Nevertheless, in the days before we used pts this function
; had been modified from the revappend approach to a careful use of
; memberequal and hence duplicate literals do, apparently, arise.
; Note: In normal use, the first literal in cl at the beginning will be the
; marker literal dealt with by crunchclausesegments2 and
; crunchclausesegments. Observe that the pts of literals occurring after
; that marker in cl are completely irrelevant to the behavior of
; crunchclausesegment, even though we are here careful to move pts from pts1
; into that section of pts when merging occurs. They are irrelevant because
; crunchclausesegments2 just collects the pts up to the marker. It might
; still be important for us to catch merges, since it is possible that two
; literals within seg1 itself will merge and thus we will create a consp pt for
; that literal and that consp pt will be collected by crunchclausesegments2
; and find its way into the main computation. Stranger things have happened in
; this code!
(cond ((null seg1) (mv cl pts))
(t (mvlet (cl pts ttree)
(addliteralandpt (car seg1) (car pts1) cl pts nil)
; Addliteralandpt just passes its last argument through as the ttree and we
; simply ignore the resulting nil. This is just an easy way to cons the first
; literal of seg1 onto cl and the first pt of pts1 onto pts  provided the
; literal doesn't already occur in cl  and to merge the pt into the
; appropriate element of pts if it does.
(declare (ignore ttree))
(crunchclausesegments1 (cdr seg1) (cdr pts1) cl pts)))))
(defun crunchclausesegments2 (cl pts seg1 pts1)
; See crunchclausesegments.
(cond ((null cl) (mv seg1 pts1 nil))
((and (consp (car cl))
(eq (ffnsymb (car cl)) 'car)
(eq (fargn (car cl) 1) :crunchclausesegmentsmarker))
(mv seg1 pts1 (cdr cl)))
(t (crunchclausesegments2 (cdr cl)
(cdr pts)
(cons (car cl) seg1)
(cons (car pts) pts1)))))
(defun crunchclausesegments (seg1 pts1 seg2 ens wrld state ttree)
; This function is a special purpose subroutine of rewriteclause. Seg1 and
; seg2 are just lists of literals. Pts1 is in weak 1:1 correspondence with
; seg1 and enumerates the parent trees of the corresponding literals of seg1.
; Consider the clause obtained by appending these two segments.
; {lit4 ... lit7 lit1' ... lit2' lit3a ... lit3z} ; cl
;  < seg1 >  < seg2 > 
; unrewritten  rewritten
; Context: The rewriter is sweeping through this clause, rewriting each literal
; and assembling a new clause. It has rewritten none of the seg1 literals and
; all of the seg2 literals. It has just rewritten some literal called lit3.
; After clausifying the result (and getting in this case lit3a ... lit3z) it is
; about to start rewriting the first literal of seg1, lit4. It has already
; rewritten lit1'...lit2'. The rewriter actually keeps the unrewritten part of
; the clause (seg1) separate from the rewritten part (seg2) so that it knows
; when it is done. In the old days, it would just proceed to rewrite the first
; literal of seg1.
; But we are trying something new. Suppose lit3 was something like (not
; (member x '(...))). Then we will get lots of segs, each of the form (equal x
; '...). We are trying to optimize our handling of this by actually stuffing
; the constant into the clause and running any terms we can. We do this in
; what we think is a very elegant way: We actually create cl and call
; removetrivialequivalences on it. Then we recover the two parts,
; unrewritten and rewritten. The trick is how we figure out which is which.
; We put a marker literal into the clause, after seg1 and before
; seg2. Removetrivialequivalences may do a lot of literal evaluation
; and deletion. But then we find the marker literal and consider everything to
; its left unrewritten and everything else rewritten.
; We return three values: The unrewritten part of cl, the rewritten part of cl,
; and an extension of ttree.
(let ((marker '(car :crunchclausesegmentsmarker)))
(mvlet (cl pts)
(crunchclausesegments1 seg1 pts1 (cons marker seg2) nil)
(mvlet (hitp cl pts ttree)
(removetrivialequivalences cl pts nil ;;; see Note
ens wrld state ttree nil nil)
; Note: In the call of removetrivialequivalences above we use removeflg =
; nil. At one time, we used removeflg = t, thinking that our cl here was the
; entire problem and thus we could delete the literal after using it. However,
; because of the fcpairlst and the simplifyclausepotlst  both of which
; may contain terms that mention the "eliminated" variable and both of which
; may introduce such terms into the clause later  we believe it best to keep
; the equality until we are at the top of the waterfall again.
(cond
((null hitp)
(mv seg1 pts1 seg2 ttree))
(t (mvlet (seg1 pts1 seg2)
(crunchclausesegments2 cl pts nil nil)
(mv seg1 pts1 seg2 ttree))))))))
; We now develop code to deal with the unrewritten assumptions generated by
; rewriting a literal of a clause. We would like to implement the illusion
; that all 'assumptions produced while rewriting a literal have actually been
; rewritten. We achieve that by stripping such assumptions out of the returned
; ttree, rewriting them, and putting them back. See
; resumesuspendedassumptionrewriting1, below, for the details.
(defun stripnonrewrittenpassumptions (ttree ans)
; Copy ttree and strip out all 'assumption records that have :rewrittenp nil.
; Accumulate those unrewritten records onto ans. Return (mv ttree' ans').
; Picky Note: Some of the conses below are used in place of the official tag
; tree constructors, e.g., (addtotagtree 'assumption & &) and
; (constagtrees & &). See the picky note in setclidsinassumptions.
(cond
((null ttree) (mv nil ans))
((symbolp (caar ttree))
(cond
((eq (caar ttree) 'assumption)
(cond
((not (access assumption (cdar ttree) :rewrittenp))
(stripnonrewrittenpassumptions (cdr ttree)
(cons (cdar ttree) ans)))
((taggedobject 'assumption (cdr ttree))
(mvlet (ttree2 ans)
(stripnonrewrittenpassumptions (cdr ttree) ans)
(mv (cons (car ttree) ttree2) ans)))
(t (mv ttree ans))))
((taggedobject 'assumption (cdr ttree))
(mvlet (ttree2 ans)
(stripnonrewrittenpassumptions (cdr ttree) ans)
(mv (cons (car ttree) ttree2) ans)))
(t (mv ttree ans))))
((taggedobject 'assumption ttree)
(mvlet (ttree1 ans)
(stripnonrewrittenpassumptions (car ttree) ans)
(mvlet (ttree2 ans)
(stripnonrewrittenpassumptions (cdr ttree) ans)
(mv (constagtrees ttree1 ttree2) ans))))
(t (mv ttree ans))))
(defun assumnotelisttotokenlist (assumnotelist)
(if (null assumnotelist)
nil
(cons (access assumnote (car assumnotelist) :rune)
(assumnotelisttotokenlist (cdr assumnotelist)))))
(defun resumesuspendedassumptionrewriting1
(assumptions ancestors gstack simplifyclausepotlst rcnst wrld state
ttree)
; A simple view of this function then is that it rewrites each assumption in
; assumptions and puts the rewritten version into ttree, reporting the first
; false assumption if finds.
; Assumptions is a list of unrewritten assumptions that were generated while
; rewriting with the rewrite arguments given to this function. We return two
; results, (mv badass ttree), where badass is either nil or an assumption
; whose :term can be rewritten to false in the current context and ttree is a
; ttree extending the input tree, justifying all the rewriting done (including
; that to false, if badass), containing 'assumption tags for all the
; assumptions in assumptions, and containing no unrewritten assumptions
; (assuming the initial ttree contained no unrewritten assumptions).
; The complication is that rewriting an assumption generates assumptions which
; we must also rewrite. The process could in principle loop if rewriting an
; assumption can regenerate the assumption. We break this potential loop via
; the use of ancestors. We imagine we are just backchaining.
; It is perhaps worth reminding the reader that these assumptions cannot be
; rewritten before they are forced because they come from typeset, which is
; defined before the rewriter is defined. Thus, we are really implementing a
; kind of delayed mutual recursion: typeset is reporting some assumptions it
; would like rewritten and we are doing it.
(cond
((null assumptions) (mv nil ttree))
(t (let* ((assn (car assumptions))
(term (access assumption assn :term)))
(mvlet
(onancestorsp assumedtrue)
(ancestorscheck term ancestors
(assumnotelisttotokenlist
(access assumption assn :assumnotes)))
(cond
(onancestorsp
; If the assumption's term is assumed true, we may omit it from the answer. If
; it is not assumedtrue, we don't know that it is false: it might merely be
; worse than some ancestor. We therefore just move the now rewritten
; assumption into the ttree and go on. Once upon a time we considered
; aborting, reporting assn as a badass. Observe that if the complement of
; term is on ancestors, then term is being assumed nil (because (not term) is
; assumed true). Doesn't that mean we coul rewrite term to nil? No. All we
; really know is that term is impossible to prove by rewriting using whatever
; lemmas we did this time. Term might be proveable. Consider the fact that
; the user could have proved (implies term term) for any term, even a proveable
; one. Then in trying to prove term we'd assume it false by putting (not term)
; on ancestors and backchain to term, which would lead us here, with the
; complement of term on ancestors. That doesn't mean term can't be proved!
(resumesuspendedassumptionrewriting1
(cdr assumptions)
ancestors gstack simplifyclausepotlst rcnst
wrld state
(if assumedtrue
ttree
(cons (cons 'assumption
(change assumption assn
:rewrittenp term))
ttree))))
(t
; We are about to rewrite term, just as in relievehyp, and so we add its
; negation to ancestors. This is equivalent to assuming term false.
(let ((newancestors
(pushancestor (dumbnegatelit term)
(assumnotelisttotokenlist
(access assumption assn :assumnotes))
ancestors)))
(mvlet
(notflg atm)
(stripnot term)
(mvlet
(val ttree1)
(rewriteentry (rewrite atm nil 'forcedassumption)
:typealist (access assumption assn :typealist)
:obj '?
:geneqv *geneqviff*
:wrld wrld
:fnstack nil
:ancestors newancestors
:backchainlimit (backchainlimit wrld)
:simplifyclausepotlst simplifyclausepotlst
:rcnst rcnst
:gstack gstack
:ttree nil
:rdepth (rewritestacklimit wrld))
(let ((val (if notflg (dumbnegatelit val) val)))
(cond
((equal val *nil*)
; If term rewrote to nil, we return assn as a bad assumption. We
; assume the proof attempt is doomed. We accumulate into ttree the
; ttree supporting the final rewrite to nil. This is a little odd.
; The badass returned is the unrewritten assumption generated by
; (force term) or (casesplit term). But the ttree returned may
; contain work done on other forces as well as the work done to show
; that term reduces to nil, even though we are returning term, not
; nil.
(mv assn (constagtrees ttree1 ttree)))
(t
; If term rewrote to nonnil, we must process the unrewritten assumptions in
; the ttree, ttree1, produced by rewriting term. We do that with a separate
; recursive call of this function, because we must pass in the newancestors so
; that we don't loop. Think of us as having assumed term false, rewritten it
; while making certain assumptions, and now  still in that context of having
; assumed it false  we will work on those assumptions.
(mvlet
(ttree1 assumptions1)
(stripnonrewrittenpassumptions ttree1 nil)
; Observe that if ttree1 contains any assumptions, they are of the rewrittenp t
; variety. We accumulate ttree1 into our answer ttree. Unless term rewrote to
; t, we accumulate the rewritten version of assn into our answer. Note that
; since the :geneqv used above is iff, we can rely on the fact that if val is
; known not to be nil then it is actually t. Finally, we rewrite all of the
; unrewritten assumptions (assumptions1) generated by rewriting term to val
; accumulate them into our answer as well.
(mvlet
(badass ttree)
(resumesuspendedassumptionrewriting1
assumptions1
newancestors ; the critical difference
gstack simplifyclausepotlst rcnst
wrld state
(constagtrees
ttree1
(if (equal val *t*)
ttree
(addtotagtree 'assumption
(change assumption assn
:term val
:rewrittenp term)
ttree))))
(cond
(badass (mv badass ttree))
(t
; Having taken care of assn and all the unrewritten assumptions generated when
; we rewrote it, we now do the rest of assumptions.
(resumesuspendedassumptionrewriting1
(cdr assumptions)
ancestors gstack simplifyclausepotlst rcnst
wrld state
ttree))))))))))))))))))
(defun resumesuspendedassumptionrewriting
(ttree ancestors gstack simplifyclausepotlst rcnst wrld state)
; We copy ttree and rewrite all the nonrewrittenp assumptions in it, deleting
; any thus established. We return (mv badass ttree'), where badass is either
; nil or an assumption in ttree whose :term can be rewritten to nil. Ttree' is
; an extension of the result of removing all nonrewrittenp assumptions from
; ttree and then replacing them by their rewritten versions plus the ttrees
; produced by that rewriting. There are no nonrewrittenp assumptions in
; ttree'.
(mvlet (ttree assumptions)
(stripnonrewrittenpassumptions ttree nil)
(resumesuspendedassumptionrewriting1
assumptions
ancestors gstack simplifyclausepotlst rcnst wrld state
ttree)))
(defun consintottree (ttree1 ttree2)
(cond
((null ttree1) ttree2)
((symbolp (caar ttree1))
(if (tagtreeoccur (caar ttree1) (cdar ttree1) ttree2)
(consintottree (cdr ttree1)
ttree2)
(consintottree (cdr ttree1)
(cons (car ttree1) ttree2))))
(t (consintottree (cdr ttree1)
(consintottree (car ttree1) ttree2)))))
; Essay on Case Limit
; The caselimit component in the casesplitlimitations is a number
; used by rewriteclause to shut down case splitting after a certain
; point is reached.
; The informal heuristic implemented here is ``don't continue to
; rewrite literals once the estimated number of output clauses exceeds
; some limit.'' We call the limit the ``caselimit.'' There are many
; interpretations of this heuristic. We discuss them here. In this
; discussion we abstract away from the particulars of given call of
; rewriteclause and instead consider all the calls of that function
; on the Common Lisp control stack. Each of those calls can be
; characterized by a picture like this {h1 ... hk ! lit1 ... litn}
; where the hi are alreadyrewritten terms generated by splitting on
; the literals that we've already rewritten, the ! signifies where we
; are in this case, and the liti are the unrewritten literals from the
; tail of the original clause. Suppose there are now more than
; caselimit of these cases; we will handle each with the same
; approach. Here are the approaches that come to mind. We have
; chosen to implement (1) after some experimentation with (3).
; (0) Stop now and process no further literals. Return the clause
; {h1 ... hk lit1 ... litn}.
; The advantage to (0) is that it is the cheapest thing we could do.
; But it dooms us to revisit each of the hi with the rewriter before
; we even look at their combination or their effects on the liti. The
; other interpretations below all do some work on the liti in hopes
; that we will have less work to do later.
; (1) It is possible that h1 ... hk is contradictory, or that h1
; ... hk together with lit2, ..., litn, are contradictory.
; Such contradictions will be found by typeset when we try to
; assume all of them false in order to rewrite lit1. So we could
; proceed to do the typealist work to set up the ``rewrite'' of
; each liti, detect the contradiction if it happens, but
; shortcircuit the rewrite at the last minute if no contradiction
; arises. In the shortcircuit we would just have the rewriteatm
; call return liti (i.e., each liti would rewrite to itself).
; This is actually the simplest change to the code.
; As noted above, if we find a typeset contradiction in (1), we won't
; have to rewrite the hi again for this case. Otherwise, we will.
; This kind of observation applies to the other ideas below.
; (2) Build the typealist and actually rewrite each liti while we have
; all this context in our hands. If rewriting liti generates an IFfree
; term (e.g., T or no change or simple normalization), just proceed.
; But if it generates an IF, pretend we did nothing and rewrite it
; to itself.
; (3) As (2) above, but if it generates an IF, use the IF without clausifying
; it. This has the effect of possibly stripping out of liti all the
; cases that are precluded by the hi, without generating any more cases.
; We will eventually see the IFs in this literal again and split them
; out.
; Once upon a time we implemented a ``creep up to the limit''
; heuristic here: If we have not yet exceeded the case limit but the
; current literal's clausification does exceed the limit, then we left
; that literal in IF form and went on. We are afraid that when the
; limit is exceeded it is exceeded by some hideous amount, e.g., 2^32
; clauses are produced. We call such a literal a ``big splitter.''
; The IF form probably tells the user more about what opened than the
; clauses do. Furthermore, little splitters further on down the
; clause might be allowed to open and may ultimately allow us to
; simplify the big splitter. This heuristic had to be implemented in
; such a way that the big splitter was eventually split out. (The
; user might have set the case limit rather low and might be using it
; to introduce cases slowly.) Our idea was just to allow the split
; when it is the first literal to split. It eventually will be. We
; abandoned this creepy idea because it put unsplit bigsplitters on
; the typealist, where they were essentially useless, and then all
; the downstream literals simplified in the empty context, introducing
; many bogus case splits.
(defun helpfullittleecntmsg (caselimit ecnt)
(cond
((and (null caselimit)
(> ecnt 1000))
(prog2$
(cw "~%~%Helpful Little Message: The simplifier is now expected ~
to produce approximately ~n0 subgoals. ~
See :DOC casesplitlimitations.~%~%"
ecnt)
ecnt))
(t ecnt)))
(mutualrecursion
(defun rewriteclause (tail pts bkptr gstack newclause fcpairlst wrld
simplifyclausepotlst
rcnst flg ecnt ans ttree state)
; In nqthm this function was called SIMPLIFYCLAUSE1.
; We are to rewrite the literals of the clause cl formed by appending
; tail to newclause. We assume rcnst has the correct topclause and
; pt and the currentclause is the correct clause. We assume the
; simplifyclausepotlst is set up for the currentclause. We assume
; fcpairlst is a list of pairs of the form (concl . ttree) of
; conclusions derived by forward chaining from negations of literals
; in currentclause. The ttrees indicate dependence on parents (via
; 'pt tags) and we may use any concl not dependent upon the literals
; contained in the :pt of rcnst (to which we add the current literal's
; pt). Ecnt is the estimated number of output clauses. We refine it
; as we go and it is ultimately returned and is the length of of ans.
; We return 4 values: a flag indicating whether anything was done, the
; final ecnt, a set, ans, of clauses whose conjunction implies cl
; under our assumptions, and a ttree that describes what we did. Our
; answers are accumulated onto flg, ecnt, ans, and ttree as we recur
; through the literals of tail.
(cond
((null tail)
(let ((rune
(builtinclausep1 (globalval 'builtinclauses wrld)
newclause
(allfnnameslst newclause)
(access rewriteconstant rcnst
:currentenabledstructure))))
(cond
(rune
(mv t ( ecnt 1) ans (pushlemma rune ttree)))
(t (mv flg ecnt (cons newclause ans) ttree)))))
(t
(mvlet
(notflg atm)
(stripnot (car tail))
(let* ((newpts (cons (car pts)
(access rewriteconstant rcnst :pt)))
(localrcnst
(change rewriteconstant rcnst
:pt
newpts
:currentliteral
(make currentliteral
:notflg notflg
:atm atm)))
(caselimit (caselimit wrld)))
; Note that in localrcnst we declared inactive the polys descending
; from the current lit.
; The use of simplifyclausepotlst below is new to Version_2.8. This
; is in support of typeset using linear arithmetic  we use the
; simplifyclausepotlst when building the typealist. Note that we
; also pass in a parenttree to declare inactive the polys descending
; from the current lit.
(mvlet
(contradictionp typealist ttree0)
(rewriteclausetypealist tail
newclause
fcpairlst
localrcnst
wrld
simplifyclausepotlst
newpts)
; Ttree0 is relevant only if we got a contradiction.
(cond
(contradictionp
(mv t
( ecnt 1)
ans
(constagtrees ttree0 ttree)))
(t
(mvlet
(val ttree1)
; Note: Nqthm used a call of (rewrite atm ...) here, while we now look on the
; typealist for atm and then rewrite. See the Nqthm note below.
; Note: Here is our ``short circuit'' implementation of case limit
; interpretation (2). We just bail out if we have exceeded the case
; limit.
(if (and caselimit
(> ecnt caselimit))
(mv atm
(addtotagtree 'caselimit t nil))
(pstk
(rewriteatm atm notflg bkptr gstack typealist wrld
simplifyclausepotlst localrcnst state)))
(let* ((val (if notflg
(dumbnegatelit val)
val))
(branches (pstk
(clausify val
(convertclausetoassumptions
(cdr tail)
(convertclausetoassumptions
newclause nil))
nil
wrld)))
(ttree1 (if (and (srlimit wrld)
(> (length branches)
(srlimit wrld)))
(addtotagtree 'srlimit
t
ttree1)
ttree1))
(action (rewriteclauseaction (car tail) branches))
(segs
; Perhaps we can simply use branches below. But that requires some thought,
; because the form below handles true clauses (including *trueclause*) with
; special care. This issue arose as we removed oldstyleforcing from the
; code.
(disjoinclausesegmenttoclauseset nil branches))
(nsegs (length segs)))
(mvlet
(badass ttree1)
(resumesuspendedassumptionrewriting
ttree1
nil ;ancestors  the fact that this isn't what it was when
;we pushed the assumption could let rewriting go deeper
gstack
simplifyclausepotlst
localrcnst
wrld
state)
(cond
(badass
; When we rewote the current literal of the clause we made an assumption
; that we now know to be false. We must abandon that rewrite. We
; act just as though the literal rewrote to itself: we pretend we have just
; done the rewriteatm above and obtained atm instead of val. We just
; reproduce the code, except we don't worry about assumptions.
(let* ((val (if notflg (dumbnegatelit atm) atm))
(branches (pstk
(clausify val
(convertclausetoassumptions
(cdr tail)
(convertclausetoassumptions
newclause nil))
nil
wrld)))
(ttree2 (if (and (srlimit wrld)
(> (length branches)
(srlimit wrld)))
(addtotagtree 'srlimit
t
ttree)
ttree))
(action (rewriteclauseaction (car tail) branches))
(segs branches)
(nsegs (length segs)))
; For an explanation of the following call of rewriteclauselst, see
; the standard call below. This is just like it, except we are ignoring
; ttree1. Note that ttree2 is an extension of ttree.
(rewriteclauselst segs
(1+ bkptr)
gstack
(cdr tail)
(cdr pts)
newclause
fcpairlst
wrld
simplifyclausepotlst
(if (eq action 'shownfalse)
localrcnst
rcnst)
(or flg (not (eq action 'nochange)))
(helpfullittleecntmsg
caselimit
(+ ecnt 1 nsegs))
ans
ttree2
state)))
; Here, once upon a time, we implemented the ``creep up on the limit''
; twist of case limit interpretation (3). Instead of shortcircuiting
; above we rewrote the atm. We either clausified the result or just
; turned it into a singleton clause possibly containing IFs, depending
; on whether we were already above the caselimit. We had to handle
; ttree1 appropriately to record the case limit restriction. We then
; continued on to here.
; The following test determines that we're about to exceed the
; caselimit.
; (and caselimit
; (<= ecnt caselimit)
; (< caselimit (+ ecnt 1 nsegs))
; (< 1 ecnt))
; It says we are currently at or below the case limit but the segs
; generated for this literal would push us over it. Furthermore, this
; is not the very first literal to produce segs (ecnt exceeds 1). In
; this case, we ignored segs. That is, we just put the unclausified
; val in as a single literal. We hold ecnt the fixed and show the
; user this rewritten goal in IF form. Eventually this IF would
; become the first literal that produces segs and the (< 1 ecnt) would
; fail, so we would split it out then.
; But as we've abandoned the whole idea of rewriting after the limit
; has been exceeded, we no longer implement this creepy idea.
; Instead, we just blast past the limit and then shut 'er down.
(t
; In the case that there is no bad assumption, then ttree1 is a ttree in which
; all assumptions have been rewritten.
(rewriteclauselst segs
(1+ bkptr)
gstack
(cdr tail)
(cdr pts)
newclause
fcpairlst
wrld
simplifyclausepotlst
; If the current lit rewrote to false, or even if it rewrote at all
; (since critical information may be lost), then we should continue to
; ignore polys and forwardchaining facts that descend from it. We
; therefore pass to lower level calls the localrcnst, which has the
; current literal's index in its :pt. The currentliteral in that
; localrcnst will be reset and the :pt will be extended locally
; there. If the current lit did not change upon rewrite, then we want
; to restore :pt to what it was at entry, so we pass the original
; rcnst. One could consider this as (change rewriteconstant rcnst
; :pt ...) to add to the old rcnst the pt of the literal just
; rewritten. Before v29, we only used localrcnst when action is
; 'shownfalse, which resulted in dropping important information, as
; shown in the following example derived from one provided by Art
; Flatau. Before the change, the goal ("Goal'") produced was
; (IMPLIES (AND (< 30 N) (<= 30 N)) (FOO N)); after the change, the
; (INTEGERP N) hypothesis was preserved.
#
(defstub foo (n) t)
(defthm natpfc2
(implies (natp x) (integerp x))
:ruleclasses :forwardchaining)
(thm (implies (and (not (or (not (natp n)) (<= n 30)))
(integerp n)
(<= 30 n))
(foo n)))
#
(if (eq action 'nochange)
rcnst
localrcnst)
(or flg (not (eq action 'nochange)))
; Prior to this literal, we estimated the number of output clauses to
; be ecnt. This literal of this clause rewrote to nsegs segments. So
; now we have ecnt1+nsegs clauses. This will be correct if no other
; literal (anywhere on the call stack) splits.
; We could estimate differently. We could suppose that this literal
; will split nsegs ways every time it occurs in the call stack.
; Essentially we would let the new ecnt be (* ecnt (max 1 nsegs)).
; (Note that if nsegs is 0, we keep ecnt fixed; the lit rewrote to
; nil.) That estimate will grow faster and probably is an upper bound
; on the actual number that would be created (e.g., some would almost
; certainly be tautologies). If we used such a method, we would start
; to cut off case splitting earlier, we would get more literals with
; IFs in them, and fewer overall clauses because the estimate would be
; too large and kick in even though some of the previous splitting was
; tautologous.
(helpfullittleecntmsg
caselimit
(+ ecnt 1 nsegs))
ans
(if (eq action 'nochange)
ttree
(consintottree ttree1 ttree))
state))))))))))))))
(defun rewriteclauselst (segs bkptr gstack cdrtail cdrpts newclause fcpairlst
wrld simplifyclausepotlst
rcnst flg ecnt ans ttree state)
(cond ((null segs)
(mv flg ecnt ans ttree))
(t
(mvlet (flg1 ecnt1 ans1 ttree1)
(rewriteclauselst (cdr segs)
bkptr
gstack
cdrtail
cdrpts
newclause
fcpairlst
wrld
simplifyclausepotlst
rcnst
flg
ecnt
ans
ttree
state)
(mvlet (unrewritten unwrittenpts rewritten ttree2)
(crunchclausesegments
cdrtail
cdrpts
(append newclause
(setdifferenceequal (car segs)
newclause))
(access rewriteconstant rcnst
:currentenabledstructure)
wrld state ttree1)
(rewriteclause unrewritten
unwrittenpts
bkptr
gstack
rewritten
fcpairlst
wrld
simplifyclausepotlst
rcnst
flg1
ecnt1
ans1
ttree2
state))))))
)
; After removing trivial equations, simplifyclause must set up
; the context in which the rewriting of the clause is done. This
; mainly means setting up the simplifyclausepotlst.
(defun setupsimplifyclausepotlst1 (cl ttrees typealist rcnst wrld state)
(mvlet (contradictionp simplifyclausepotlst)
(rewriteentry
(addtermsandlemmas cl ;termlst to assume
ttrees ;corresponding tag trees
nil ;positivep (terms assumed false)
)
:typealist typealist
:obj nil
:geneqv nil
:wrld wrld
:fnstack nil
:ancestors nil
:backchainlimit (backchainlimit wrld)
:simplifyclausepotlst nil
:potlstterms nil
:rcnst rcnst
:gstack (initialgstack 'setupsimplifyclausepotlst
nil cl)
:ttree nil
:rdepth (rewritestacklimit wrld))
(cond
(contradictionp (mv contradictionp nil))
(t (mv nil simplifyclausepotlst)))))
(defun setupsimplifyclausepotlst (cl ttrees fcpairlst
typealist rcnst wrld state)
; We construct the initial value of the simplifyclausepotlst in
; preparation for rewriting clause cl. We assume rcnst contains the
; user's hint settings, the correct topclause and current clause, and a
; null :pt.
; We return two values. If the first is nonnil it indicates that we
; have proved cl and the other value is irrelevant. In the case that we
; prove clause the first result is a poly, meaning it was proved by
; linear arithmetic. The assumptions in the ttree of that poly must be
; considered before cl is declared proved. When the first answer is nil
; the second is the constructed simplifyclausepotlst.
; As of Version_2.8, we start by adding the (negations of) any
; forwardchaining conclusions to the head of cl and the corresponding
; ttrees to ttrees. We then call the original
; setupsimplifyclausepotlst on the resultant expanded clause.
; This will allow us to use forwardchaining conclusions in linear
; arithmetic.
; Here is one example of why we might want to do this:
#
(defun bytep (n)
(and (integerp n)
(<= 128 n)
(< n 128)))
(defthm bytepthm
(implies (and (integerp n)
(<= 128 n)
(< n 128))
(bytep n)))
(defthm bytepfcthm
(implies (bytep n)
(and (integerp n)
(<= 128 n)
(< n 128)))
:ruleclasses :forwardchaining)
(intheory (disable bytep))
(defthm tricky
(implies (and (bytep n)
(bytep (+ 7 n)))
(bytep (+ 3 n))))
#
; Before linear arithmetic used the conclusions of forwardchaining
; rules, one would have to reenable the definition of bytep in order
; to prove tricky. But if this appeared in a larger context, in which
; one had proved a bunch of lemmas about bytep, one could find oneself
; in a pickle. By enabling bytep, one loses the ability to use all
; the lemmas about it. Without enabling bytep, tricky is hard to
; prove.
;
; And here is another example:
#
(defun bvecp (x n)
(and (integerp x)
(<= 0 x)
(< x (expt 2 n))))
(defthm bvecp2<4
(implies (bvecp x 2)
(and (integerp x)
(<= 0 x)
(< x 4)))
:ruleclasses :forwardchaining)
(intheory (disable bvecp))
(thm (implies (and (bvecp x 2)
(not (equal x 0))
(not (equal x 1))
(not (equal x 2)))
(equal x 3)))
#
(cond ((null fcpairlst)
(setupsimplifyclausepotlst1 cl ttrees typealist rcnst wrld state))
(t
(setupsimplifyclausepotlst (cons (dumbnegatelit
(caar fcpairlst)) cl)
(cons (cdar fcpairlst) ttrees)
(cdr fcpairlst)
typealist rcnst wrld state))))
(defun sequentialsubstvarterm (alist term)
; Each element of alist is of the form (vari . termi). We replace
; vari by termi in term and then sequentially apply the remaining
; pairs to the result.
(cond ((null alist) term)
(t (sequentialsubstvarterm (cdr alist)
(substvar (cdar alist)
(caar alist)
term)))))
(defun processequationalpolys
(cl hist rcnst typealist wrld potlst flg ttree)
; We deduce from potlst all the interesting equations in it and add
; them to cl unless they have already been generated and recorded in
; hist. The flg and ttree are merely accumulators where we construct
; our answers. In the toplevel call, flg should be nil and ttree
; should be any ttree we want to infect with our answer. Nil would do.
; We return three results, flg, cl and ttree. The first indicates
; whether we did anything. The second is the final value of cl and
; the third is the final ttree. That ttree will record the equations
; we generated and used in this step. It should become part of the
; history of our output cl so that we do not loop.
; We merely scan down potlst. At every pot we find the first
; acceptable equational poly (if any) and change flg, cl and ttree
; appropriately.
; Historical note: Previous to Version_2.7, rather than add certain
; equalities to cl we performed the substitution suggested by that
; equality. This substition forced us to carry along another
; argument, which was the list of all such substitutions made to date.
; That was called vartermsubsts. Here is a Historical Comment that
; deals with the necessity for this now eliminated argument.
; Historical Comment
; The argument vartermsubsts is a list of pairs of the form (var
; . term). These represent some of the equations already found, with
; the first pair on the list representing the earliest such equation.
; (That is, the list is in chronology order, not reverse chronological
; order.) When a new equation is found and that equation relates a
; var to a term (instead of two nonvar terms), we do not really add
; the equation to the clause but rather just substitute the term for
; the var, eliminating that variable. This can raise problems if, for
; example, we find A = B and replace all the B's by A, and then later
; find B = C. Had we actually added (equal A B) in response to the
; first equation, this would not be a problem. But since we didn't
; add that equation but just eliminated all the B's in favor of A, we
; now find B = C unconnected to A. So every time we find a new
; equation from the pot we first apply each of the substitution pairs
; to it, sequentially.
; Here is an example that failed under Version_2.4 (which did not
; have the vartermsubsts argument) but succeeded Version_2.5
; (which introduced the argument to fix such problems).
#
(defstub bar (x) t)
(thm (implies (and (rationalp a)(rationalp b)(rationalp c)
(<= a b) (<= b a)
(<= b c) (<= c b))
(equal (bar a) (bar c))))
#
; End of Historical Comment
; We think we avoid the need for this argument by eliminating all
; substitution from this function and instead producing the literal
; equalities we deduce.
(cond ((null potlst)
(mv flg cl ttree))
(t
(mvlet (ttree1 lhs rhs)
(findequationalpoly (car potlst) hist)
(if (null ttree1) ; no equation was found
(processequationalpolys cl hist rcnst typealist wrld
(cdr potlst) flg ttree)
; From lhs <= rhs and rhs <= lhs we can actually derive the equality
; of their fixes, (fix lhs) = (fix rhs). We could generate that
; equation and let the system split on the numericity of the two sides
; by conventional opening of fix. But we don't do that, partly for
; cosmetic reasons but mainly because it is possible the two sides
; have been assumed numeric in ttree1 and rather than force a
; premature split, we just use the existing mechanism to cause the
; split later on below, and thus avoid an identical split.
; The derivedequation, below, is used for two purposes: It is
; advertised as the :target of the assumnote we generate to force an
; assumption, and it is possibly added to the clause. (We say "possibly"
; because the equality may be manifest in some sense. See hitp below.)
; The :target of an assumnote is used just in reporting the force.
(let ((derivedequation ; orient the equality
(cond ((and (variablep lhs)
(not (dumboccur lhs rhs)))
(consterm 'equal (list lhs rhs)))
((and (variablep rhs)
(not (dumboccur rhs lhs)))
(consterm 'equal (list rhs lhs)))
(t (consterm 'equal (list lhs rhs)))))
(oktoforce (oktoforce rcnst))
(ens (access rewriteconstant rcnst
:currentenabledstructure)))
(mvlet (flag1 ttree2)
(addlinearassumption derivedequation
(mconsterm* 'acl2numberp lhs)
typealist ens
(immediateforcep nil ens)
oktoforce wrld ttree1)
(mvlet
(flag2 ttree3)
(cond
((eq flag1 :failed)
(mv :failed ttree1))
(t (addlinearassumption derivedequation
(mconsterm* 'acl2numberp rhs)
typealist ens
(immediateforcep nil ens) oktoforce wrld
ttree2)))
; Note lhs and rhs below are bogus if flag2 is :failed; they should not be
; used. Also, note that up through Version_2.9.3, lhs was set to 0 even when
; (acl2numberp lhs) was indeterminate with forcing off, but now we do not set
; to 0 in that case (flag1 = :failed); similarly for rhs.
(let* ((lhs (if (eq flag1 :knownfalse) *0* lhs))
(rhs (if (eq flag2 :knownfalse) *0* rhs))
; So at this point, if either side is definitely nonnumeric, it has
; defaulted to 0, just as though we generated (equal (fix lhs) (fix
; rhs)) and then opened the corresponding fix to 0. Furthermore,
; ttree3 contains the assumptions that both are numeric (when those
; assumptions are not trivially true or trivially false). In addition
; ttree3 extends ttree1.
; If hitp, below, is true then we will change the cl we are working on. In
; particular, we will NOT change it if either of our numeric assumptions
; :failed or if both lhs and rhs are trivially 0  e.g., as would happen if
; one was 0 and the other was known nonnumeric.
(hitp (not (or (eq flag2 :failed)
; The following case is new after ACL2_2.9.3. The following example was
; provided by Robert Krug, inspired by an example from Dave Greve. Dave didn't
; want a bogus forcing round in such cases (i.e., cases where we don't know
; that at least one side is numeric).
; (thm (implies (and (equal (foo z) (foo y))
; (equal (foo x) (foo z)))
; (foo (+ x y z))))
(and (eq flag1 :added)
(eq flag2 :added))
(and (equal lhs *0*)
(equal rhs *0*))))))
; Note: Robert Krug found a soundness bug in an earlier version of
; this code. We used derivedequation instead of (mconsterm* 'equal
; lhs rhs) below. But derivedequation has the original lhs and rhs
; in them, not the FIXed versions!
(processequationalpolys
(if hitp
(addliteral (dumbnegatelit
(mconsterm* 'equal lhs rhs))
cl
nil)
cl)
hist rcnst typealist wrld
(cdr potlst)
; We got a hit if either we already had a hit or we hit this time.
(or flg hitp)
(constagtrees (cond
(hitp ttree3)
(t
; If we do not change the clause, we do not record a dependence on the
; typeset information recorded in ttree3. However, we still record
; ttree1 because it contains the note that prevents us from rederiving
; this same inequality. Recall that ttree3 includes ttree1.
ttree1))
ttree)))))))))))
; We are finally ready to begin the final assault on simplifyclause.
(defun enumerateelements (lst i)
(cond ((null lst) nil)
(t (cons i (enumerateelements (cdr lst) (1+ i))))))
(defun alreadyusedbyfertilizeclausep (lit hist getclauseid)
; We determine whether the literal lit, which is presumably of the form (not
; (equiv lhs rhs)), has already been used by fertilization in the history hist
; of the current clause. If not, then we return nil. Otherwise, we return the
; clause id of that previous use if getclauseid is true, else we return t.
(cond ((null hist) nil)
((and (eq (access historyentry (car hist) :processor)
'fertilizeclause)
(tagtreeoccur 'literal lit
(access historyentry (car hist) :ttree)))
(or getclauseid
(cdr (taggedobject 'clauseid (access historyentry (car hist)
:ttree)))))
(t (alreadyusedbyfertilizeclausep lit (cdr hist) getclauseid))))
(defun unhiddenlitinfo (hist clause pos wrld)
(cond
((null clause)
(mv nil nil nil))
(t (let ((lit (car clause)))
(casematch lit
(('not ('hide (equiv & &))) ; (not (hide (equiv x y)))
(cond ((equivalencerelationp equiv wrld)
(let* ((newlit (fconsterm* 'not (fargn (fargn lit 1) 1)))
(clid
(alreadyusedbyfertilizeclausep
newlit
hist nil)))
(cond (clid (mv pos newlit clid))
(t (unhiddenlitinfo hist (cdr clause) (1+ pos)
wrld)))))
(t (unhiddenlitinfo hist (cdr clause) (1+ pos) wrld))))
(& (unhiddenlitinfo hist (cdr clause) (1+ pos) wrld)))))))
(defun tilde@hypphrase (lentail cl)
; This tilde@ phrase describes a literal of the given clause, cl, as a
; hypothesis in the prettyification of cl, where lentail is the length of the
; tail of cl following that literal (but if somehow the literal is in cl, this
; function acts like it is the last element). This phrase will, for example,
; complete the sentence "We now use ~@0." One possible completion is "We now
; use the hypothesis." Another is, "We now use the conclusion." A more common
; one is "We now use the third hypothesis."
; Warning: The function fertilizeclausemsg knows that this function
; either refers to the lit as a "conclusion" or as a "hypothesis" and
; can tell which by asking whether the result here is a consp whose
; cdr is nil! So don't change this function without considering that.
(let* ((len (length cl))
(n ( len lentail)))
(cond
((int= n len)
; See the warning above.
'("the conclusion"))
((and (int= len 2)
(int= n 1))
"the hypothesis")
(t (msg "the ~n0 hypothesis"
(cons n 'th))))))
(defun simplifyclause1 (topclause hist rcnst wrld state)
; In Nqthm, this function was called SIMPLIFYCLAUSE0.
; Topclause is a clause with history hist. We assume that rcnst has
; a null pt and contains whatever hint settings the user
; wants in it, as well as the :forceinfo based on whether there is a
; call of IF in topclause.
; We return 3 values. The first indicates whether we changed topclause and,
; if so, whether we went through the rewriter; it will help determine signal
; returned by simplifyclause (and hence will be used, ultimately, to create
; the 'simplifyclause hist entry). If we did not change topclause, the
; second and third are nil. If we did change topclause, the second is a list
; of new clauses whose conjunction implies topclause and the third is a ttree
; explaining what we did. This ttree will be used to create the
; 'simplifyclause hist entry.
(mvlet (hitp currentclause pts removetrivialequivalencesttree)
(removetrivialequivalences topclause
nil
t
(access rewriteconstant rcnst
:currentenabledstructure)
wrld state nil nil nil)
(declare (ignore pts))
(let ((localrcnst (change rewriteconstant rcnst
:topclause topclause
:currentclause currentclause))
(currentclausepts (enumerateelements currentclause 0)))
(mvlet
(contradictionp typealist fcpairlst)
(pstk
(forwardchain currentclause
currentclausepts
(oktoforce localrcnst)
nil ; donotreconsiderp
wrld
(access rewriteconstant rcnst
:currentenabledstructure)
(access rewriteconstant rcnst
:oncepoverride)
state))
; Either we forward chained to a contradiction, in which case we are
; done, or else we have a typealist assuming the negation of every
; literal in the currentclause and a list of pairs of the form (concl
; . ttree) indicating that each concl can be derived from the parent
; literals indicated by the 'pt tags.
(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 'hit
nil
(constagtrees removetrivialequivalencesttree
fcpairlst)))
(t
; We next construct the initial simplifyclausepotlst.
; The construction might prove currentclause, in which case the
; contradictionp answer is nonnil.
(mvlet
(contradictionp simplifyclausepotlst)
(pstk
(setupsimplifyclausepotlst currentclause
(ptstottreelst
currentclausepts)
fcpairlst
typealist
localrcnst wrld state))
(cond
(contradictionp
; A nonnil contradictionp is a poly meaning linear proved currentclause
; (modulo the assumptions in the tag tree of the poly).
(mv 'hit
nil
(constagtrees
removetrivialequivalencesttree
(pushlemma
*fakeruneforlinear*
(access poly contradictionp :ttree)))))
(t
(mvlet
(flg newcurrentclause ttree)
(pstk
(processequationalpolys
currentclause hist localrcnst typealist wrld
simplifyclausepotlst nil
removetrivialequivalencesttree))
(cond
(flg
; Here is where we now perform the substitutions previously done
; within processequationalpolys. See the historical remarks in that
; function.
(mvlet
(hitp newestcurrentclause pts ttree1)
(pstk
(removetrivialequivalences
newcurrentclause
nil
t
(access rewriteconstant localrcnst
:currentenabledstructure)
wrld state ttree nil nil))
(declare (ignore pts hitp))
(mv 'hit
(list newestcurrentclause)
(pushlemma *fakeruneforlinear*
ttree1))))
(t
; When we call rewriteclause, below, we pass in as the initial value
; of its ``did we change anything?'' accumulator the flg, hitp, that
; indicates whether removetrivialequations changed anything. Thus,
; this call may answer ``yes, something was changed'' when in fact,
; nothing was done by rewriteclause itself. Note that since we are
; calling rewriteclause here, we return 'hitrewrite rather than 'hit
; if we return a nonnil signal; see the comments in simplifyclause.
(mvlet
(flg ecnt ans ttree)
(rewriteclause currentclause
currentclausepts
1
(initialgstack 'simplifyclause
nil currentclause)
nil fcpairlst wrld
simplifyclausepotlst
localrcnst
hitp
1
nil
removetrivialequivalencesttree
state)
(declare (ignore ecnt))
(cond
((null flg)
(mvlet
(pos unhiddenlit oldclid)
(unhiddenlitinfo hist topclause 0 wrld)
(cond (pos (let ((tail (nthcdr (1+ pos) topclause)))
(mv 'hitrewrite
(list (append (take pos topclause)
(cons unhiddenlit
tail)))
(addtotagtree
'hypphrase
(tilde@hypphrase (len tail)
topclause)
(addtotagtree
'clauseid oldclid
(pushlemma (fnrunenume 'hide nil
nil wrld)
nil))))))
(t (mv nil ans ttree)))))
(t (mv 'hitrewrite ans ttree))))))))))))))))
(defun someelementdumboccurlst (lst1 lst2)
(cond ((null lst1) nil)
((dumboccurlst (car lst1) lst2) t)
(t (someelementdumboccurlst (cdr lst1) lst2))))
; The Spec Vars of Prove  pspv
; The theorem prover, prove, uses so many special variables that are rarely
; modified that we bundle them up. Because simplifyclause, below, is a
; clause processor in the waterfall, it is the first function in this
; development that is high enough up in the hierarchy to see prove's
; bundle of variables. So it is time to lay out prove's spec vars:
(defrec provespecvar
((rewriteconstant inductionhypterms . inductionconclterms)
(tagtree . hintsettings)
pool
usersuppliedterm displayedgoal orighints . otfflg)
t)
; The orighints setting is the list of clauseids and hintsettings
; supplied to prove. The hintsettings is the particular hint
; settings for the current clause. The only reason we have the
; orighints field is so that we can compute the hints appropriate for
; the toplevel goal if we have to abandon the initial work and revert
; to the usersupplied term.
(defconst *emptyprovespecvar*
(make provespecvar
:rewriteconstant nil
:inductionhypterms nil
:inductionconclterms nil
:tagtree nil
:hintsettings nil
:orighints nil
:pool nil
:usersuppliedterm *t*
:displayedgoal nil
:otfflg nil))
(defun filterdisabledexpandterms (terms ens wrld)
; We build expand hint strucures, throwing certain terms out of terms.
; Variables and constants are kept (but they should never be there). Lambda
; applications are kept. Function symbol applications are kept provided the
; symbol has a nonnil, enabled defbody. There is no point in keeping on
; :expandlst a term whose function symbol has no defbody, because it
; there that we go when we decide to force an expansion (from other than
; userprovided :expand hints).
; Note: It is good that HIDE has a body because we allow HIDE terms to be put
; on :expandlst and we wouldn't want to throw them off.
(cond
((null terms)
nil)
((or (variablep (car terms))
(fquotep (car terms)))
nil)
(t
(cond ((flambdap (ffnsymb (car terms)))
(cons (make expandhint
:pattern (car terms)
:alist :none
:rune nil
:equiv 'equal
:hyp nil
:lhs (car terms)
:rhs (subcorvar (lambdaformals (ffnsymb (car terms)))
(fargs (car terms))
(lambdabody (ffnsymb (car terms)))))
(filterdisabledexpandterms (cdr terms) ens wrld)))
(t
(let ((defbody (defbody (ffnsymb (car terms)) wrld)))
(cond
((and defbody
(enablednumep (access defbody defbody :nume)
ens))
(cons (make expandhint
:pattern (car terms)
:alist :none
:rune (access defbody defbody :rune)
:equiv 'equal
:hyp (access defbody defbody :hyp)
:lhs (consterm (ffnsymb (car terms))
(access defbody defbody
:formals))
:rhs (access defbody defbody :concl))
(filterdisabledexpandterms (cdr terms) ens wrld)))
(t (filterdisabledexpandterms (cdr terms) ens wrld)))))))))
(defun foundhitrewritehistentry (hist)
; Hist is a list of historyentry records. We search it to find a history
; entry with 'hitrewrite or 'hitrewrite2 signal. Note that if we
; find 'hitrewrite, we know that no previous entry (i.e., later in
; hist when viewed as a list) has signal 'hitrewrite2, due to the way
; we return signals in simplifyclause.
(if (endp hist)
nil
(or (car (membereq (access historyentry (car hist) :signal)
'(hitrewrite hitrewrite2)))
(foundhitrewritehistentry (cdr hist)))))
(defabbrev append? (x y)
(cond ((null y) x)
(t (append x y))))
(defun simplifyclause (cl hist pspv wrld state)
; This is the first "clause processor" of the waterfall. Its input and
; output spec is consistent with that of all such processors. See the
; waterfall for a general discussion.
; Cl is a clause with history hist. We can obtain a rewriteconstant
; from the prove spec var pspv. We assume nothing about the
; rewriteconstant except that it has the user's hint settings in it
; and that the pt is nil. We install our topclause and
; currentclause when necessary.
; We return 4 values. The first is a signal that in general is 'miss,
; 'abort, 'error, or a "hit". In this case, it is always either 'miss
; or one of 'hit, 'hitrewrite, or 'hitrewrite2 (as described further
; below). When the signal is 'miss, the other 3 values are
; irrelevant. When the signal is 'hit, the second result is the list
; of new clauses, the third is a ttree that will become that component
; of the historyentry for this simplification, and the fourth is the
; unmodified pspv. (We return the fourth thing to adhere to the
; convention used by all clause processors in the waterfall (q.v.).)
; If the first result is a "hit" then the conjunction of the new
; clauses returned implies cl. Equivalently, under the assumption
; that cl is false, cl is equivalent to the conjunction of the new
; clauses.
; On Tail Biting by Simplifyclause:
; Tail biting can occur at the simplifyclause level, i.e., we can
; return a set of clauses that is a generalization of the clause cl,
; e.g., a set whose conjunction is false even though cl is not. This
; is because of the way we manage the simplifyclausepotlst and
; pts. We build a single potlst and use parent trees to
; render inactive those polys that we wish to avoid. To arrange to
; bite our own tail, put two slightly different versions of the same
; inequality literal into cl. The poly arising from the second can be
; used to rewrite the first and the poly arising from first can be used
; to rewrite the second. If the first rewrites to false immediately our
; use of parent trees (as arranged by passing localrcnst to the recursive
; call of rewriteclause in rewriteclause) will wisely prevent the use of
; its poly while rewriting the second. But if the first rewrites to some
; nonlinear term (which will be rewritten to false later) then we'll
; permit ourselves to use the first's poly while working on the second
; and we could bite our tail.
; This would not happen if we produced a new linear potlst for each
; literal  a potlst in which the literal to be rewritten was not
; assumed false. Early experiments with that approach led us to
; conclude it was too expensive.
; If the specification of rewrite is correct, then tail biting cannot
; happen except via the involvement of linear arithmetic. To see this,
; consider the assumptions governing the rewriting of each literal in the
; clause and ask whether the literal being rewritten in in rewriteclause
; is assumed false via any of those assumptions. There are five sources
; of assumptions in the specification of rewrite: (a) the typealist
; (which is constructed so as to avoid that literal), (b) the assumptions
; in ancestors (which is initially empty), (c) the assumptions in the
; potlst (which we are excepting), and (d) 'assumptions in ttree
; (which we are excepting). Thus, the only place that assumption might
; be found is simplifyclausepotlst. If linear is eliminated, the only
; assumptions left are free of the literal being worked on.
; This is really an interface function between the rewriter and the rest of
; the prover. It has three jobs.
; The first is to convert from the world of pspv to the world of
; rcnst. That is, from the package of spec vars passed around in the
; waterfall to the package of constants known to the rewriter.
; The second job of this function is to control the expansion of the
; inductionhypterms and inductionconcl terms (preventing the
; expansion of the former and forcing the expansion of the latter) by
; possibly adding them to termstobeignoredbyrewrite and
; expandlst, respectively. This is done as part of the conversion
; from pspv (where induction hyps and concl are found) to rcnst (where
; termstobeignoredbyrewrite and expandlst are found). They are
; so controlled as long as we are in the first simplification stages
; after induction. As soon as the clause has gone through the
; rewriter with some change, with input free of inductionconclterms,
; we stop interfering. The real work horse of clause level
; simplification is simplifyclause1.
; The third job is to convert the simplifyclause1 answers into the
; kind required by a clause processor in the waterfall. The work
; horse doesn't return an pspv and we do.
(prog2$
(initializebrrstack state)
(cond ((assoceq 'settleddownclause hist)
; The clause has settled down under rewriting with the
; inductionhypterms initially ignored and the inductionconclterms
; forcibly expanded. In general, we now want to stop treating those
; terms specially and continue simplifying. However, there is a
; special case that will save a little time. Suppose that the clause
; just settled down  i.e., the most recent hist entry is the one we
; just found. And suppose that none of the specially treated terms
; occurs in the clause we're to simplify. Then we needn't simplify it
; again.
(cond ((and (eq 'settleddownclause
(access historyentry (car hist) :processor))
(not (someelementdumboccurlst
(access provespecvar
pspv
:inductionhypterms)
cl)))
; Since we know the inductionconclterms couldn't occur in the clause
;  they would have been expanded  we are done. (Or at least: if
; they do occur in the clause, then still, removing them from the
; expandlst should not help the rewriter!) This test should speed up
; base cases and preinduction simplification at least.
(mv 'miss nil nil nil))
(t
; We now cease interfering and let the heuristics do their job.
(mvlet (changedp clauses ttree)
(simplifyclause1
cl hist
(change rewriteconstant
(access provespecvar pspv
:rewriteconstant)
:forceinfo
(if (ffnnameplst 'if cl)
'weak
t))
wrld
state)
(cond (changedp
; Note: It is possible that our input, cl, is a memberequal of our
; output, clauses! Such simplifications are said to be "specious."
; But we do not bother to detect that here because we want to report
; the specious simplification as though everything were ok and then
; pretend nothing happened. This gives the user some indication of
; where the loop is. In the old days, we just signalled a 'miss if
; (memberequal cl clauses) and that caused a lot of confusion among
; experienced users, who saw simplifiable clauses being passed on to
; elim, etc. See :DOC specioussimplification.
(mv 'hit clauses ttree pspv))
(t (mv 'miss nil nil nil)))))))
(t
; The clause has not settled down yet. So we arrange to ignore the
; inductionhypterms when appropriate, and to expand the
; inductionconclterms without question. The localrcnst created
; below is not passed out of this function.
(let* ((rcnst (access provespecvar pspv :rewriteconstant))
(newforceinfo (if (ffnnameplst 'if cl)
'weak
t))
(inductionconclterms
(access provespecvar pspv :inductionconclterms))
(histentryhit (foundhitrewritehistentry hist))
(hitrewrite2 (or (eq histentryhit 'hitrewrite2)
(and (eq histentryhit 'hitrewrite)
(not (someelementdumboccurlst
inductionconclterms
cl)))))
; We arrange to expand the inductionconclterms and ignore the
; inductionhypterms unless hitrewrite2 above is set.
(localrcnst
(cond (hitrewrite2
; We have previously passed through the rewriter, and either a
; predecessor goal or this one is free of inductionconclterms. In
; that case we stop meddling with the rewriter by inhibiting rewriting
; of inductionhypterms and forcing expansion of
; inductionconclterms. Before Version_2.8 we waited until
; 'settleddownclause before ceasing our meddling. However, Dave
; Greve and Matt Wilding reported an example in which that heuristic
; slowed down the prover substantially by needlessly delaying the
; rewriting of inductionhypterms. Notice that this heuristic nicely
; matches the induction heuristics: both consider only the goal, not
; the result of rewriting it. (We however ignore rewriting by
; preprocessclause for the present purpose: we want to wait for a
; fullblown rewrite before allowing rewriting of
; inductionhypterms.)
; Initially we attempted to fix the slowdown mentioned above (the one
; reported by Greve and Wilding) by eliminating completely the special
; treatment of inductionhypterms. However, lemma
; psuedotermpbinaryop_tree in books/meta/pseudotermplemmas.lisp
; showed the folly of this attempt. The relevant goal was as follows.
; Subgoal *1/5'
; (IMPLIES (AND (CONSP L)
; (CONSP (CDR L))
; (CONSP (CDDR L))
; (PSEUDOTERMP (BINARYOP_TREE BINARYOPNAME
; CONSTANTNAME FIXNAME (CDR L)))
; (PSEUDOTERMLISTP L)
; (SYMBOLP BINARYOPNAME)
; (SYMBOLP FIXNAME)
; (NOT (EQUAL BINARYOPNAME 'QUOTE))
; (NOT (CONSP CONSTANTNAME)))
; (PSEUDOTERMP (BINARYOP_TREE BINARYOPNAME
; CONSTANTNAME FIXNAME L)))
; In this case inductionhypterms contained the single term
; (binaryop_tree binaryopname constantname fixname (cdr l)).
; Without special treatment of inductionhypterms, the above
; binaryop_tree term was rewritten, and hence so was the pseudotermp
; hypothesis. The result seemed to give permission to the next
; hypothesis, (pseudotermlistp l), to be rewritten much more
; agressively than it was formerly, which bogged down the rewriter
; (perhaps even in an infinite loop).
; A later attempt used the simple algorithm that we stop meddling once
; we have made a pass through the rewriter, even if there are still
; inductionconclterms around. Lemma flipeqsubstcommute in
; books/workshops/1999/ivy/ivyv2/ivysources/flip.lisp showed the
; problem with that approach. Subgoal *1/2' below was produced by
; preprocessclause. It produces goal Subgoal *1/2.16, which has a
; new occurrence in the conclusion of the inductionconclterm
; (SUBSTFREE F X TM):
#
Subgoal *1/2'
(IMPLIES (AND (NOT (WFNOT F))
(CONSP F)
(CONSP (CDR F))
(CONSP (CDDR F))
(NOT (CDDDR F))
(OR (EQUAL (CAR F) 'AND)
(EQUAL (CAR F) 'OR)
(EQUAL (CAR F) 'IMP)
(EQUAL (CAR F) 'IFF))
(EQUAL (SUBSTFREE (FLIPEQ (CADR F) (CDR POS))
X TM)
(FLIPEQ (SUBSTFREE (CADR F) X TM)
(CDR POS)))
(EQUAL (SUBSTFREE (FLIPEQ (CADDR F) (CDR POS))
X TM)
(FLIPEQ (SUBSTFREE (CADDR F) X TM)
(CDR POS))))
(EQUAL (SUBSTFREE (FLIPEQ F POS) X TM)
(FLIPEQ (SUBSTFREE F X TM) POS))).
This simplifies, using the :definitions FLIPEQ, LEN, LIST2P, LIST3P,
SUBSTFREE, TRUELISTP, WFBINARY, WFEQ and WFNOT, the :executable
counterparts of BINARY+, EQUAL, LEN and TRUELISTP, primitive type
reasoning and the :rewrite rules CARCONS and CDRCONS, to the following
16 conjectures.
Subgoal *1/2.16
(IMPLIES (AND (CONSP F)
(CONSP (CDR F))
(CONSP (CDDR F))
(NOT (CDDDR F))
(EQUAL (CAR F) 'AND)
(EQUAL (SUBSTFREE (FLIPEQ (CADR F) (CDR POS))
X TM)
(FLIPEQ (SUBSTFREE (CADR F) X TM)
(CDR POS)))
(EQUAL (SUBSTFREE (FLIPEQ (CADDR F) (CDR POS))
X TM)
(FLIPEQ (SUBSTFREE (CADDR F) X TM)
(CDR POS)))
(NOT (CONSP POS)))
(EQUAL (SUBSTFREE F X TM)
(LIST 'AND
(SUBSTFREE (CADR F) X TM)
(SUBSTFREE (CADDR F) X TM))))
#
; If we stop meddling after Subgoal *1/2', then hypothesis rewriting
; in Subgoal *1/2.16 is so severe that we are subject to
; casesplitlimitations and never reach the conclusion! If memory
; serves, an attempt to turn off casesplitlimitations just led the
; prover off the deep end.
(change rewriteconstant
rcnst
:forceinfo newforceinfo
; We also tried a modification in which we use the same :expandlst as
; below, thus continuing to meddle with inductionconclterms even
; after we are done meddling with inductionhypterms. However, that
; caused problems with, for example, the proof of exponentsadd1 in
; books/arithmetic2/pass1/expthelper.lisp. Apparently the forced
; expansion of (EXPT R J) looped with rule exponentsadd2 (rewriting
; r^(i+j)). At any rate, it seems reasonable enough to keep
; suppression of inductionhypterms rewriting in sync with forced
; expansion of inductionconclterms.
; And we tried one more idea: removing the test on whether the clause had been
; rewritten. We got one failure, on collecttimes3b in v28 in
; books/arithmetic2/meta/commonmeta.lisp.
; What happens in the proof attempt is that the inductionconclterms have been
; eliminated in Subgoal *1/7''. If we check for rewriting, no further meddling
; occurs, and the next subgoal (Subgoal *1/7''') is pushed for proof by
; induction. That's what we want in this case.
; But if we don't check for rewriting then when the inductionconclterm (EXPT
; X J) surprisingly reappears in Subgoal *1/7''', we again expand it. It
; continues to appear in every other goal, causing a loop.
; Now, the suggestion was not to check whether the goal was rewritten, and
; we've given that one interpretation. Another interpretation is to record in
; the history the first time we see a disappearance of inductionconclterms,
; so that we never again try to expand them (or ignore inductionhypterms).
; But it seems that the natural way to record such information still involves
; saving extra information (e.g., the signal) in a history entry. So even
; though it may be redundant, we might as well check that we've done some
; rewriting. That way we don't have to rely on the immediate appearance of
; inductionconclterms, and yet we are still guaranteed at least one pass
; through the rewriter before stopping the "meddling".
))
(t
(change rewriteconstant
rcnst
:forceinfo newforceinfo
:termstobeignoredbyrewrite
(append
(access provespecvar
pspv :inductionhypterms)
(access rewriteconstant
rcnst
:termstobeignoredbyrewrite))
:expandlst
(append? (access rewriteconstant
rcnst :expandlst)
; We give the user's expandlst priority, in case it specifies :with for a term
; that is also an enabled call in inductionconclterms.
(filterdisabledexpandterms
inductionconclterms
(access rewriteconstant
rcnst
:currentenabledstructure)
wrld)))))))
(mvlet (hitp clauses ttree)
(simplifyclause1 cl hist localrcnst wrld state)
(cond
(hitp (mv (if hitrewrite2 'hitrewrite2 hitp)
clauses ttree pspv))
(t (mv 'miss nil nil nil)))))))))
; Inside the waterfall, the following clause processor immediately follows
; simplifyclause.
(defun settleddownclause (clause hist pspv wrld state)
; This is the processor in the waterfall just after simplifyclause.
; Its presence in the waterfall causes us to add a
; 'settleddownclause histentry to the history of the clause when
; simplifyclause finishes with it. The "hit state" of the waterfall
; leads back to the simplifier, where the code above detects this
; settling down and turns off the handling of the induction hyp and
; concl terms. The "miss state" of the waterfall leads to the next
; processor.
; Note: There has been some consideration given to the question
; ``should this function claim a 'hit after SPECIOUS
; simplifyclauses?'' We say ``yes'' in the comment in
; previousprocesswasspeciousp.
(declare (ignore wrld state))
(cond ((assoceq 'settleddownclause hist)
(mv 'miss nil nil nil))
(t (mv 'hit (list clause) nil pspv))))
; We now develop the functions for reporting on the output of simplify.
(defun insertpairbycdr (carval cdrval alist)
; A carcdrsorted alist is an alist whose keys are symbols and whose
; values are alists sorted by cdr, where each value is a cons of
; symbols. Such alists are the type returned by
; extractandclassifylemmas.
(cond ((null alist)
(list (cons carval cdrval)))
((eq cdrval (cdar alist))
(cond
((eq carval (caar alist))
alist)
((symbol< carval (caar alist))
(cons (cons carval cdrval)
alist))
(t
(cons (car alist)
(cons (cons carval cdrval)
(cdr alist))))))
((symbol< cdrval (cdar alist))
(cons (cons carval cdrval) alist))
(t
(cons (car alist)
(insertpairbycdr carval cdrval (cdr alist))))))
(defun extendcarcdrsortedalist (key carval cdrval alist)
(cond ((null alist)
(list (cons key (list (cons carval cdrval)))))
((eq key (caar alist))
(cons (cons key (insertpairbycdr
carval cdrval (cdr (car alist))))
(cdr alist)))
((symbol< key (caar alist))
(cons (cons key (list (cons carval cdrval)))
alist))
(t (cons (car alist)
(extendcarcdrsortedalist
key carval cdrval (cdr alist))))))
(defun extractandclassifylemmas (ttree ignorelst forcedrunes alist)
; We essentially partition the set of runes tagged as 'lemmas in ttree
; into partitions based on the type (i.e., the keyword token) for each
; rune. In addition, we indicate whether the rune is a member of
; forcedrunes. In our partitioning we actually throw away the runes and
; just report the corresponding base symbols.
; In particular, scan ttree for all the 'lemma tags and return an
; alist associating each type of rune used in the ttree with a list of
; pairs. Each pair is of the form (flg . name), where flg is t or nil
; and name is the base symbol of a rune of the given type used in the
; ttree. There is a pair for every rune in the ttree, except those
; whose base symbols are in ignorelst; those runes we ignore. If flg
; is t, the corresponding rune is a member of forcedrunes.
; An example alist returned is
; '((:DEFINITION (NIL . APP) (T . REV))
; (:REWRITE (NIL . LEMMA1) (T . LEMMA2) (NIL . LEMMA3))
; (:TYPEPRESCRIPTION (T . FN1) (T . FN2) (NIL . FN3)))
; indicating that three :REWRITE runes were used, with base symbols
; LEMMA1, LEMMA2 (which was forced), and LEMMA3, etc.
; The alist is sorted by car. Each value is itself an alist that is
; sorted by cdr.
(cond ((null ttree) alist)
((symbolp (caar ttree))
(cond
((eq (caar ttree) 'lemma)
(extractandclassifylemmas
(cdr ttree) ignorelst forcedrunes
(let ((rune (cdar ttree)))
(cond
((membereq (basesymbol rune) ignorelst)
alist)
(t
(extendcarcdrsortedalist
(car rune)
(cond ((memberequal rune forcedrunes) t)
(t nil))
(basesymbol rune)
alist))))))
(t (extractandclassifylemmas (cdr ttree)
ignorelst forcedrunes alist))))
(t (extractandclassifylemmas
(cdr ttree) ignorelst forcedrunes
(extractandclassifylemmas (car ttree)
ignorelst forcedrunes alist)))))
(deflabel Simple
:doc
":DocSection Miscellaneous
~c[:]~ilc[definition] and ~c[:]~ilc[rewrite] rules used in preprocessing~/
~bv[]
Example of simple rewrite rule:
(equal (car (cons x y)) x)
Examples of simple definition:
(defun fileclockp (x) (integerp x))
(defun naturalp (x)
(and (integerp x) (>= x 0)))
~ev[]~/
The theorem prover output sometimes refers to ``simple'' definitions
and rewrite rules. These rules can be used by the preprocessor,
which is one of the theorem prover's ``processes'' understood by the
~c[:donot] hint; ~pl[hints].
The preprocessor expands certain definitions and uses certain
rewrite rules that it considers to be ``fast''. There are two ways
to qualify as fast. One is to be an ``abbreviation'', where a
rewrite rule with no hypotheses or loop stopper is an
``abbreviation'' if the right side contains no more variable
occurrences than the left side, and the right side does not call the
functions ~ilc[if], ~ilc[not] or ~ilc[implies]. Definitions and rewrite rules can
both be abbreviations; the criterion for definitions is similar,
except that the definition must not be recursive. The other way to
qualify applies only to a nonrecursive definition, and applies when
its body is a disjunction or conjunction, according to a perhaps
subtle criterion that is intended to avoid case splits.")
(defun tilde*conjunctionofpossiblyforcednamesphrase1 (lst)
(cond
((null lst) nil)
(t
(cons (msg (if (caar lst)
"~x0 (forced)"
"~x0")
(cdar lst))
(tilde*conjunctionofpossiblyforcednamesphrase1 (cdr lst))))))
(defun tilde*conjunctionofpossiblyforcednamesphrase (lst)
; Lst is a list of pairs of the form (flg . name). We build a tilde* phrase
; that will print a conjoined list of names, with the parenthetical remark "forced"
; occurring just after those with flg t.
; For example, if lst is
; ((NIL . APP) (T . REV) (NIL . LEN) (T . MEM) (T . SQ))
; and the output of this function is bound to the fmt variable
; #\D, then ~*D prints "APP, REV (forced), LEN, MEM (forced) and SQ
; (forced)".
(list "" "~@*" "~@* and " "~@*, "
(tilde*conjunctionofpossiblyforcednamesphrase1 lst)))
(defun tilde*simpphrase1 (alist abbreviationsflg)
(cond
((null alist) (mv nil nil))
((eq (caar alist)
(car *fakeruneforlinear*))
(mvlet (restmsgs restpairs)
(tilde*simpphrase1 (cdr alist) abbreviationsflg)
(mv (cons "linear arithmetic" restmsgs)
restpairs)))
((eq (caar alist)
(car *fakerunefortypeset*))
(mvlet (restmsgs restpairs)
(tilde*simpphrase1 (cdr alist) abbreviationsflg)
(mv (cons "primitive type reasoning" restmsgs)
restpairs)))
((eq (caar alist)
(car *fakerunefornurewriter*))
(mvlet (restmsgs restpairs)
(tilde*simpphrase1 (cdr alist) abbreviationsflg)
(mv (cons "the nurewriter" restmsgs)
restpairs)))
(t
(let ((names
(tilde*conjunctionofpossiblyforcednamesphrase (cdar alist)))
; Note: Names is a tilde* object that will print a conjoined list of names
; (possibly followed by parenthetical "forced" remarks). We must determine
; whether there is more than one name in the list. The names printe are just
; those in (cdar alist), which we know is a nonempty true list of pairs.
; Below we set pluralp to t if two or more names will be printed and to nil if
; exactly one name will be printed.
(pluralp (if (cdr (cdar alist)) t nil)))
(mvlet
(msg pair)
(case (caar alist)
(:DEFINITION
(mv (if abbreviationsflg
(if pluralp
"the simple :definitions ~*D"
"the simple :definition ~*D")
(if pluralp
"the :definitions ~*D"
"the :definition ~*D"))
(cons #\D names)))
(:EXECUTABLECOUNTERPART
(mv (if pluralp
"the :executablecounterparts of ~*X"
"the :executablecounterpart of ~*X")
(cons #\X names)))
(:REWRITE
(mv (if abbreviationsflg
(if pluralp
"the simple :rewrite rules ~*R"
"the simple :rewrite rule ~*R")
(if pluralp
"the :rewrite rules ~*R"
"the :rewrite rule ~*R"))
(cons #\R names)))
(:LINEAR
(mv (if pluralp
"the :linear rules ~*L"
"the :linear rule ~*L")
(cons #\L names)))
(:BUILTINCLAUSE
(mv (if pluralp
"the :builtinclause rules ~*B"
"the :builtinclause rule ~*B")
(cons #\B names)))
(:COMPOUNDRECOGNIZER
(mv (if pluralp
"the :compoundrecognizer rules ~*C"
"the :compoundrecognizer rule ~*C")
(cons #\C names)))
; We do not expect the following three cases to arise in the
; simplifier, but this function finds wider use.
(:ELIM
(mv (if pluralp
"the :elim rules ~*e"
"the :elim rule ~*e")
(cons #\e names)))
(:GENERALIZE
(mv (if pluralp
"the :generalize rules ~*G"
"the :generalize rule ~*G")
(cons #\G names)))
(:INDUCTION
(mv (if pluralp
"the :induction rules ~*I"
"the :induction rule ~*I")
(cons #\I names)))
(:META
(mv (if pluralp
"the :meta rules ~*M"
"the :meta rule ~*M")
(cons #\M names)))
(:FORWARDCHAINING
(mv (if pluralp
"the :forwardchaining rules ~*F"
"the :forwardchaining rule ~*F")
(cons #\F names)))
(:EQUIVALENCE
(mv (if pluralp
"the :equivalence rules ~*E"
"the :equivalence rule ~*E")
(cons #\E names)))
(:REFINEMENT
(mv (if pluralp
"the :refinement rules ~*r"
"the :refinement rule ~*r")
(cons #\r names)))
(:CONGRUENCE
(mv (if pluralp
"the :congruence rules ~*c"
"the :congruence rule ~*c")
(cons #\c names)))
(:TYPEPRESCRIPTION
(mv (if pluralp
"the :typeprescription rules ~*T"
"the :typeprescription rule ~*T")
(cons #\T names)))
(:TYPESETINVERTER
(mv (if pluralp
"the :typesetinverter rules ~*t"
"the :typesetinverter rule ~*t")
(cons #\t names)))
; Note that *fakeruneforanonymousenabledrule* will never arise here,
; because pushlemma is careful not to put it into any tag trees.
(otherwise
(mv (er hard 'tilde*simpphrase1
"We did not expect to see the simplifier report a rune of type ~x0."
(caar alist))
nil)))
(mvlet (restmsgs restpairs)
(tilde*simpphrase1 (cdr alist) abbreviationsflg)
(mv (cons msg restmsgs)
(cons pair restpairs))))))))
(defun recoverforcedrunes (ttree ans)
; Every assumption in ttree has exactly one assumnote. Let the
; ":rune" of the assumption be the :rune field of the car of its
; assumnotes.
; We scan the tag tree ttree for all occurrences of the 'assumption
; tag and collect into ans the :rune of each assumption, when the
; :rune is a rune. We ignore the symbolp :runes because we will be
; searching the resulting list for genuine runes and thus need not
; clutter it with symbols.
(cond
((null ttree) ans)
((symbolp (caar ttree))
(cond
((and (eq (caar ttree) 'assumption)
(not (symbolp
(access assumnote
(car (access assumption (cdar ttree) :assumnotes))
:rune))))
(recoverforcedrunes
(cdr ttree)
(addtosetequal
(access assumnote
(car (access assumption (cdar ttree) :assumnotes))
:rune)
ans)))
(t (recoverforcedrunes (cdr ttree) ans))))
(t (recoverforcedrunes
(car ttree)
(recoverforcedrunes (cdr ttree) ans)))))
(defun tilde*simpphrase (ttree)
; This function determines from ttree whether linear arithmetic and/or
; primitive type reasoning was used and what lemmas and function symbols were
; used. Then it constructs and returns a tuple suitable for giving to the ~*
; fmt directive. I.e., if you fmt the string "The proof depends upon ~*S."
; and #\S is bound to the output of this function, then you will get something
; like:
; v
; The proof depends upon linear arithmetic, the lemma ASSOCOFAPP
; (forced), and the definitions of APP (forced) and REVERSE.
; ^
; Note that the msg actually starts at the v above and stops at the ^.
; I.e., no space will be printed at the beginning, and no space or
; punctuation will be printed at the end.
; Note: Several functions know that if (nth 4 output) is nil, where
; output is the result of this function, then essentially nothing was
; done (i.e., "trivial observations" would be printed).
(let ((forcedrunes (recoverforcedrunes ttree nil)))
(mvlet (messagelst charalist)
(tilde*simpphrase1
(extractandclassifylemmas ttree nil forcedrunes nil)
nil)
(list* "trivial ob~ser~va~tions"
"~@*"
"~@* and "
"~@*, "
messagelst
charalist))))
; CLAUSE IDENTIFICATION
; Before we can write the function that prints a description of
; simplifyclause's output, we must be able to identify clauses. This raises
; some issues that are more understandable later, namely, the notion of the
; pool. See PUSHCLAUSE and The Pool.
; Associated with every clause in the waterfall is a unique object
; called the clause identifier or clauseid. These are printed out
; at the user in a certain form, e.g.,
; [3]Subgoal *2.1/5.7.9.11'''
; but the internal form of these ids is:
(defrec clauseid ((forcinground . poollst) caselst . primes) t)
; where forcinground is a natural number, poollst and caselst are truelists
; of nonzero naturals and primes is a natural. The poollst is indeed a
; poollst. (See the function poollst defined below.) The caselst is
; structurally analogous.
; A useful constant, the first clauseid:
(defconst *initialclauseid*
(make clauseid
:forcinground 0
:poollst nil
:caselst nil
:primes 0))
; Note: If this changes, inspect every use of it. As of this writing there is
; one place where we avoid a make clauseid and use *initialclauseid* instead
; because we know the forcinground is 0 and poollst and caselst fields are
; both nil and the primes field is 0.
(defun tilde@poolnamephrase (forcinground poollst)
; We use this function to create the printed representation from the
; forcinground and poollst. This function actually has two uses. First,
; poolnames are used within a single round to refer to local goals, such as
; when we say "Name the formula above *1." or, more suggestively "Name the
; formula above [2]*1.3.4." In such use, the forcing round is placed just
; before the star, in square brackets. But poolnames also play a role in
; "clause ids" such as [2]Subgoal *1.3.4/1.1'''. Observe that in clause ids
; the poolname is printed here ^^^^^^ but the forcinground is
; not printed in the normal place but before the word "Subgoal." Basically,
; the forcinground is always leading. Thus, we need two versions of this
; function, one that puts the forcinground in and another that does not.
; Confusingly but conveniently, if the forcing round is 0, we do not display it
; and so the two uses of this function  to generate standalone pool names
; and to generate parts of clause ids  appear somewhat hidden. But you will
; find calls of this function where the forcinground supplied is 0 
; signallying that we want a pool name to use within a clause id  even though
; the actual forcinground at the time of call is non0.
(cond
((= forcinground 0)
; Notes:
; 1. This asterisk is the one that appears in the printed name.
; 2. If you wanted trailing punctuation, you could put it before
; this close double gritch.
; 3. These two dots are the ones that separate numbers in the name.
; 1 2 3 3
; ! ! ! !
(cons "*~*0"
(list (cons #\0 (list "" "~x*" "~x*." "~x*." poollst)))))
(t
(cons "[~xr]*~*0"
(list (cons #\r forcinground)
(cons #\0 (list "" "~x*" "~x*." "~x*." poollst)))))))
(defun tilde@poolnamephraselst (forcinground lst)
(cond ((null lst) nil)
(t (cons (tilde@poolnamephrase forcinground (car lst))
(tilde@poolnamephraselst forcinground (cdr lst))))))
(defun tilde@clauseidphrase (id)
; Id is a clauseid. This function builds a tilde@ object that when printed
; will display the clause id in its external form.
; Warning: If this function is changed so as to print differently, change the
; associated parser, parseclauseid. Also change the clone of
; this function, stringfortilde@clauseidphrase.
; For example, if id is
; (make clauseid
; :forcinground 3
; :poollst '(2 1)
; :caselst '(5 7 9 11)
; :primes 3)
; then the result of a tilde@ on the returned object will be:
; [3]Subgoal *2.1/5.7.9.11'''
; The parser noted above will parse "[3]Subgoal *2.1/5.7.9.11'''" into the
; clauseid above. Will wonders never cease? Boyer and Moore wrote a parser?
; If the forcinground is 0, then we do not print the [...] displaying the forcinground.
; The sequence of id's printed as the primes field goes from 0 to 11 is
; Subgoal *2.1/5.7.9.11
; Subgoal *2.1/5.7.9.11'
; Subgoal *2.1/5.7.9.11''
; Subgoal *2.1/5.7.9.11'''
; Subgoal *2.1/5.7.9.11'4'
; Subgoal *2.1/5.7.9.11'5'
; Subgoal *2.1/5.7.9.11'6'
; Subgoal *2.1/5.7.9.11'7'
; Subgoal *2.1/5.7.9.11'8'
; Subgoal *2.1/5.7.9.11'9'
; Subgoal *2.1/5.7.9.11'10'
; Subgoal *2.1/5.7.9.11'11'
; If the poollst is nil (which is not a pool list ever produced by
; poollst but which is used before we have pushed anything into the
; pool), then we print
; Subgoal 5.7.9.11'''
; or
; [3]Subgoal 5.7.9.11'''
; depending on the forcinground.
; And if the poollst is nil and the caselst is nil we print
; Goal'''
; or
; [3]Goal'''
(cons (cond
((= (access clauseid id :forcinground) 0)
(cond ((null (access clauseid id :poollst))
(cond ((null (access clauseid id :caselst))
"Goal~#q~[~/'~/''~/'''~/'~xn'~]")
(t "Subgoal ~@c~#q~[~/'~/''~/'''~/'~xn'~]")))
(t "Subgoal ~@p/~@c~#q~[~/'~/''~/'''~/'~xn'~]")))
(t
(cond ((null (access clauseid id :poollst))
(cond ((null (access clauseid id :caselst))
"[~xr]Goal~#q~[~/'~/''~/'''~/'~xn'~]")
(t "[~xr]Subgoal ~@c~#q~[~/'~/''~/'''~/'~xn'~]")))
(t "[~xr]Subgoal ~@p/~@c~#q~[~/'~/''~/'''~/'~xn'~]"))))
(list
(cons #\r (access clauseid id :forcinground))
(cons #\p
(tilde@poolnamephrase 0 (access clauseid id :poollst)))
(cons #\c
(cons "~*0"
(list (cons #\0 (list "" "~x*" "~x*." "~x*."
(access clauseid id :caselst))))))
(cons #\q
(cond ((> (access clauseid id :primes) 3) 4)
(t (access clauseid id :primes))))
(cons #\n
(access clauseid id :primes)))))
; Because of the way :DONOTINDUCT name hints are implemented, we need to be
; able to produce a literal atom of the form name clauseid where clauseid
; is what tilde@clauseidphrase will print on id. Therefore, we now
; virtually repeat the definition of tilde@clauseidphrase, except this time
; building a string. We could use this to print all clause ids. But that is
; slow because it involves consing up strings. So we suffer the inconvenience
; of duplication. If tilde@clauseidphrase is changed, be sure to change
; the functions below.
(defun stringfortilde@clauseidphrase/periods (lst)
(declare (xargs :guard (truelistp lst)))
(cond
((null lst) nil)
((null (cdr lst)) (explodeatom (car lst) 10))
(t (append (explodeatom (car lst) 10)
(cons #\.
(stringfortilde@clauseidphrase/periods
(cdr lst)))))))
(defun stringfortilde@clauseidphrase/primes (n)
(declare (xargs :guard (and (integerp n) (>= n 0))))
(cond ((= n 0) nil)
((= n 1) '(#\'))
((= n 2) '(#\' #\'))
((= n 3) '(#\' #\' #\'))
(t (cons #\' (append (explodeatom n 10) '(#\'))))))
(defun stringfortilde@clauseidphrase (id)
(coerce
(append
(if (= (access clauseid id :forcinground) 0)
nil
`(#\[ ,@(explodeatom (access clauseid id :forcinground) 10) #\]))
(cond ((null (access clauseid id :poollst))
(cond ((null (access clauseid id :caselst))
(append '(#\G #\o #\a #\l)
(stringfortilde@clauseidphrase/primes
(access clauseid id :primes))))
(t (append '(#\S #\u #\b #\g #\o #\a #\l #\Space)
(stringfortilde@clauseidphrase/periods
(access clauseid id :caselst))
(stringfortilde@clauseidphrase/primes
(access clauseid id :primes))))))
(t (append
'(#\S #\u #\b #\g #\o #\a #\l #\Space #\*)
(stringfortilde@clauseidphrase/periods
(access clauseid id :poollst))
(cons #\/
(append (stringfortilde@clauseidphrase/periods
(access clauseid id :caselst))
(stringfortilde@clauseidphrase/primes
(access clauseid id :primes))))))))
'string))
(defrec bddnote
(clid goalterm mxid errstring fmtalist cst term bddcallstack ttree)
nil)
(defun tilde@bddnotephrase (x)
; Bddnote is either a tagged bddnote pair or nil. This function returns a ~@
; phrase to be used just after "But simplification" or "This simplifies".
(cond ((null x) "")
(t (msg " with BDDs (~x0 nodes)"
(access bddnote (cdr x) :mxid)))))
; Clauseids are typed as strings by the user when he wants to
; identify a clause to which some hint settings are attached. We now
; develop the machinery for parsing the user's strings into clauseid
; records.
(defun parsenatural (str i maximum ans)
; Starting at the ith position of string str we parse a
; natural number. We return the number read (or nil, if
; the first char we see is not a digit) and the position of
; the first nondigit. Ans should be initially nil.
(cond ((>= i maximum) (mv ans maximum))
(t (let* ((c (char str i))
(d (case c
(#\0 0)
(#\1 1)
(#\2 2)
(#\3 3)
(#\4 4)
(#\5 5)
(#\6 6)
(#\7 7)
(#\8 8)
(#\9 9)
(otherwise nil))))
(cond (d (parsenatural str (1+ i) maximum
(cond ((null ans) d)
(t (+ (* 10 ans) d)))))
(t (mv ans i)))))))
(defun parsedottednaturals (str i maximum ans)
; Starting at the ith position of string str we parse a list of
; naturals separated by dots. We return the list of naturals (which
; may be nil) and the position of the first character not parsed.
; Here are some examples. In all cases, assume the initial i is 1.
; "*2.1.3 abc..." => (2 1 3) and 6 (which points to the #\Space)
; " Subgoal..." => nil and 1 (which points to the #\S)
; " 5.7.9" => (5 7 9) and 6 (which is just off the end)
; " 5.7ABC" => (5 7) and 4 (which points to the #\A)
; " 5.7.ABC" => (5 7) and 4 (which points to the #\.)
; The last example bears thinking about.
(cond
((>= i maximum) (mv (reverse ans) maximum))
(t (mvlet (nat j)
(parsenatural str i maximum nil)
(cond ((null nat) (mv (reverse ans) i))
((>= j maximum) (mv (reverse (cons nat ans)) maximum))
((and (eql (char str j) #\.)
(< (1+ j) maximum)
(member
(char str (1+ j))
'(#\0 #\1 #\2 #\3 #\4 #\5 #\6 #\7 #\8 #\9)))
(parsedottednaturals str (1+ j) maximum (cons nat ans)))
(t (mv (reverse (cons nat ans)) j)))))))
(defun parsematch (pat j patmax str i strmax)
; Starting at the ith char of string str we match each against its
; counterpart in pat, starting at j. If we exhaust pat we return the
; position of the first character in str past the match. Otherwise we
; return nil. This matching is caseinsensitive.
(cond ((>= j patmax) i)
((>= i strmax) nil)
((or (eql (char pat j) (char str i))
(eql (chardowncase (char pat j)) (chardowncase (char str i))))
(parsematch pat (1+ j) patmax str (1+ i) strmax))
(t nil)))
(defun parseprimes (str i maximum)
; Starting at the ith char of string str we count the "number of primes."
; ', '', and ''' are 1, 2, and 3, respectively. '4' is 4, '5' is 5, etc.
; We return nil if the string we find is not of this form. We also return
; the index of the first character not parsed.
(cond
((>= i maximum) (mv 0 maximum))
((eql (char str i) #\')
(cond ((= (+ 1 i) maximum) (mv 1 maximum))
((eql (char str (+ 1 i)) #\')
(cond ((= (+ 2 i) maximum) (mv 2 maximum))
((eql (char str (+ 2 i)) #\') (mv 3 (+ 3 i)))
(t (mv 2 (+ 2 i)))))
(t (mvlet
(nat j)
(parsenatural str (+ 1 i) maximum nil)
(cond
((null nat) (mv 1 (+ 1 i)))
((< nat 4) (mv 1 (+ 1 i)))
((= j maximum) (mv 1 (+ 1 i)))
((eql (char str j) #\') (mv nat (+ 1 j)))
(t (mv 1 (+ 1 i))))))))
(t (mv 0 i))))
(defun parseclauseid2 (forcinground poollst str i maximum)
; Assume that poollst is a poollst. Suppose that at position i in
; string str there is a caselst followed by some primes, e.g.,
; "...5.7.9.11'''". We parse them out and check that the string ends
; at the end of the primes. We return a clauseid composed of the
; poollst supplied above and the parsed caselst and primes. If the
; parse fails, we return nil.
(mvlet
(caselst j)
(parsedottednaturals str i maximum nil)
(cond ((member 0 caselst)
nil)
(t
; So we've seen "...5.7.9.11..." where ... may be empty.
; We look for the primes.
(mvlet
(n j)
(parseprimes str j maximum)
(cond ((= j maximum)
(make clauseid
:forcinground forcinground
:poollst poollst
:caselst caselst
:primes n))
(t nil)))))))
(defun parseclauseid1 (forcinground str i maximum)
; This function takes a string, e.g., "...Subgoal *2.1/5.7.9.11'''" and an
; index i into it to indicate the terminal substring of interest. We parse
; that terminal substring into the internal clause id with forcinground as its
; :forcinground. For example, if i points to the S in subgoal above, then the
; result is
; (make clauseid
; :forcinground forcinground
; :poollst '(2 1)
; :caselst '(5 7 9 11)
; :primes 3)
; We return nil if the substring does not parse.
(cond
((< maximum (+ i 4)) nil)
((member (char str i) '(#\G #\g))
; The only thing this string could be is something of the form
; "Goal'...". In particular, we know that the poollst and the
; caselst are both nil and it is merely a question of counting
; primes.
(let ((k (parsematch "Goal" 0 4 str i maximum)))
(cond (k
(mvlet (n j)
(parseprimes str k maximum)
(cond ((= j maximum)
(make clauseid
:forcinground forcinground
:poollst nil
:caselst nil
:primes n))
(t nil))))
(t nil))))
(t
(let ((k (parsematch "Subgoal " 0 8 str i maximum)))
(cond ((null k) nil)
((>= k maximum) nil)
((eql (char str k) #\*)
(mvlet
(poollst j)
(parsedottednaturals str (1+ k) maximum nil)
(cond
((or (null poollst)
(member 0 poollst)
(> (+ 1 j) maximum)
(not (eql (char str j) #\/)))
; So we've seen "Subgoal *junk" and we return nil.
nil)
(t
; So we've seen "Subgoal *2.1/..." where ... is nonempty. We
; look for the caselst now.
(parseclauseid2 forcinground poollst str (+ 1 j) maximum)))))
(t
; So we've seen "Subgoal ..." where ... doesn't begin with #\*. Thus
; it can only be a caselst followed by primes.
(parseclauseid2 forcinground nil str k maximum)))))))
(defun parseclauseid (str)
; This function takes a string, e.g., "[3]Subgoal *2.1/5.7.9.11'''" and either
; parses it into an internal clause id or returns nil. For example, on the
; string above the result is
; (make clauseid
; :forcinground 3
; :poollst '(2 1)
; :caselst '(5 7 9 11)
; :primes 3)
; We are case insensitive, but totally rigid about whitespace. We
; expect that the user will most often obtain these strings by
; grabbing the fmt output of a tilde@clauseidphrase object. Users
; sometimes use Emacs to lowercase whole regions of events and that is
; why we are case insensitive.
; We recognize two special cases of clauseid's that are never printed
; by prove. "Goal" and the symbol T both denote the toplevel
; clauseid.
(cond
((stringp str)
(let* ((maximum (length str)))
(cond
((< maximum 4) nil)
((eql (char str 0) #\[)
(mvlet (forcinground i)
(parsenatural str 1 maximum nil)
(cond
((and forcinground
(eql (char str i) #\]))
(parseclauseid1 forcinground str (1+ i) maximum))
(t nil))))
(t (parseclauseid1 0 str 0 maximum)))))
((eq str t) *initialclauseid*)
(t nil)))
(defun tilde@casesplitlimitationsphrase (srflg caseflg)
(if srflg
(if caseflg
" (By the way, the subsumption/replacement and case ~
limits affected this analysis. See :DOC casesplitlimitations.)"
" (By the way, the subsumption/replacement limit ~
affected this analysis. See :DOC casesplitlimitations.)")
(if caseflg
" (By the way, the case limit affected this analysis. ~
See :DOC casesplitlimitations.)"
"")))
; And now we can define the output routine for simplifyclause, which is also
; used in applytophintsclausemsg1.
(defun simplifyclausemsg1 (signal clid clauses speciousp ttree pspv state)
; The arguments to this function are NOT the standard ones for an
; output function in the waterfall because we are prepared to print a
; message about the simplification being specious and as of this
; writing simplification is the only process that may be specious.
; Exception: OBDD processing also uses this function, and can also
; produce specious simplification. Note that our current treatment of
; OBDDs does not create 'assumptions; however, we check for them
; anyhow here, both in order to share this code between
; simplifyclause and OBDD processing and in order to be robust (in
; case forcing enters the realm of OBDD processing later).
; See the discussion of the waterfall for more details about the
; standard arguments for processors.
(declare (ignore signal pspv))
(cond ((null clauses)
(fms "But ~#0~[~/forced ~]simplification~@b reduces this to T, using ~
~*1.~@c~"
(list (cons #\0 (if (taggedobject 'assumption ttree) 1 0))
(cons #\1 (tilde*simpphrase ttree))
(cons #\b (tilde@bddnotephrase
(taggedobject 'bddnote ttree)))
(cons #\c (tilde@casesplitlimitationsphrase
(taggedobject 'srlimit ttree)
(taggedobject 'caselimit ttree))))
(proofsco state)
state
(termevisctuple nil state)))
(speciousp
(fms "This ~#0~[~/forcibly ~]simplifies~@b, using ~*1, to~#2~[ ~@3 ~
itself!~/ a set of ~n4 conjectures including ~@3 itself!~] ~
Therefore, we ignore this specious simp~li~fi~ca~tion. See ~
:DOC specioussimplification.~@c~"
(list (cons #\0 (if (taggedobject 'assumption ttree) 1 0))
(cons #\1 (tilde*simpphrase ttree))
(cons #\2 clauses)
(cons #\3 (tilde@clauseidphrase clid))
(cons #\4 (length clauses))
(cons #\b (tilde@bddnotephrase
(taggedobject 'bddnote ttree)))
(cons #\c (tilde@casesplitlimitationsphrase
(taggedobject 'srlimit ttree)
(taggedobject 'caselimit ttree))))
(proofsco state)
state
(termevisctuple nil state)))
(t
(let ((hypphrasepair (taggedobject 'hypphrase ttree)))
(cond (hypphrasepair
(fms "We remove HIDE from ~@0, which was used heuristically ~
to transform ~@1 by substituting into the rest of that ~
goal. This produces~"
(list (cons #\0 (cdr hypphrasepair))
(cons #\1 (tilde@clauseidphrase
(cdr (taggedobject 'clauseid ttree)))))
(proofsco state)
state
(termevisctuple nil state)))
(t
(fms "This ~#0~[~/forcibly ~]simplifies~@b, using ~*1, ~
to~#2~[~/ the following ~n3 conjectures.~@c~]~"
(list (cons #\0 (if (taggedobject 'assumption ttree) 1 0))
(cons #\1 (tilde*simpphrase ttree))
(cons #\2 clauses)
(cons #\3 (length clauses))
(cons #\b (tilde@bddnotephrase
(taggedobject 'bddnote ttree)))
(cons #\c (tilde@casesplitlimitationsphrase
(taggedobject 'srlimit ttree)
(taggedobject 'caselimit ttree))))
(proofsco state)
state
(termevisctuple nil state))))))))
(deflabel specioussimplification
:doc
":DocSection Miscellaneous
nonproductive proof steps~/
Occasionally the ACL2 theorem prover reports that the current goal
simplifies to itself or to a set including itself. Such
simplifications are said to be ``specious'' and are ignored in the
sense that the theorem prover acts as though no simplification were
possible and tries the next available proof technique. Specious
simplifications are almost always caused by forcing.~/
The simplification of a formula proceeds primarily by the local
application of ~c[:]~ilc[rewrite], ~c[:]~ilc[typeprescription], and other rules to its
various subterms. If no rewrite rules apply, the formula cannot be
simplified and is passed to the next ACL2 proof technique, which is
generally the elimination of destructors. The experienced ACL2 user
pays special attention to such ``maximally simplified'' formulas;
the presence of unexpected terms in them indicates the need for
additional rules or the presence of some conflict that prevents
existing rules from working harmoniously together.
However, consider the following interesting possibility: local
rewrite rules apply but, when applied, reproduce the goal as one of
its own subgoals. How can rewrite rules apply and reproduce the
goal? Of course, one way is for one rule application to undo the
effect of another, as when commutativity is applied twice in
succession to the same term. Another kind of example is when two rules
conflict and undermine each other. For example, under suitable
hypotheses, ~c[(length x)] might be rewritten to ~c[(+ 1 (length (cdr x)))]
by the ~c[:]~ilc[definition] of ~ilc[length] and then a ~c[:]~ilc[rewrite] rule might be used
to ``fold'' that back to ~c[(length x)]. Generally speaking the
presence of such ``looping'' rewrite rules causes ACL2's simplifier
either to stop gracefully because of heuristics such as that
described in the documentation for ~ilc[loopstopper] or to cause a
stack overflow because of indefinite recursion.
A more insidious kind of loop can be imagined: two rewrites in
different parts of the formula undo each other's effects ``at a
distance,'' that is, without ever being applied to one another's
output. For example, perhaps the first hypothesis of the formula is
simplified to the second, but then the second is simplified to the
first, so that the end result is a formula propositionally
equivalent to the original one but with the two hypotheses commuted.
This is thought to be impossible unless forcing or casesplitting
occurs, but if those features are exploited (~pl[force] and
~pl[casesplit]) it can be made to happen relatively easily.
Here is a simple example. Declare ~c[foo] to be a function of one
argument returning one result:
~bv[]
(defstub p1 (x) t)
~ev[]
Prove the following silly rule:
~bv[]
(defthm bad
(implies (casesplit (p1 x))
(p1 x)))
~ev[]
Now suppose we try the following.
~bv[]
(thm (p1 x))
~ev[]
The ~il[rewrite] rule ~c[bad] will rewrite ~c[(p1 x)] to ~c[t], but it will
be unable to prove the hypothesis ~c[(casesplit (p1 x))]. As a result, the
prover will spawn a new goal, to prove ~c[(p1 x)]. However, since this new
goal is the same as the original goal, ACL2 will recognize the simplification
as ~em[specious] and consider the attempted simplification to have failed.
In other words, despite the rewriting, no progress was made! In more common
cases, the original goal may simplify to a set of subgoals, one of which
includes the original goal.
If ACL2 were to adopt the new set of subgoals, it would loop
indefinitely. Therefore, it checks whether the input goal is a
member of the output subgoals. If so, it announces that the
simplification is ``specious'' and pretends that no simplification
occurred.
``Maximally simplified'' formulas that produce specious
simplifications are maximally simplified in a very technical sense:
were ACL2 to apply every applicable rule to them, no progress would
be made. Since ACL2 can only apply every applicable rule, it cannot
make further progress with the formula. But the informed user can
perhaps identify some rule that should not be applied and make it
inapplicable by disabling it, allowing the simplifier to apply all
the others and thus make progress.
When specious simplifications are a problem it might be helpful to
~il[disable] all forcing (including ~il[casesplit]s) and resubmit
the formula to observe whether forcing is involved in the loop or
not. ~l[force]. The commands
~bv[]
ACL2 !>:disableforcing
and
ACL2 !>:enableforcing
~ev[]
~il[disable] and ~il[enable] the pragmatic effects of both ~c[force]
and ~c[casesplit]. If the loop is broken when forcing is
~il[disable]d, then it is very likely some ~il[force]d hypothesis of
some rule is ``undoing'' a prior simplification. The most common
cause of this is when we ~il[force] a hypothesis that is actually
false but whose falsity is somehow temporarily hidden (more below).
To find the offending rule, compare the specious simplification with
its nonspecious counterpart and look for rules that were speciously
applied that are not applied in the nonspecious case. Most likely
you will find at least one such rule and it will have a ~ilc[force]d
hypothesis. By disabling that rule, at least for the subgoal in
question, you may allow the simplifier to make progress on the
subgoal.")
(defun settleddownclausemsg1 (signal clauses ttree pspv state)
; The arguments to this function are the standard ones for an output
; function in the waterfall. See the discussion of the waterfall.
(declare (ignore signal clauses ttree pspv))
state)
