File: linear-a.lisp

package info (click to toggle)
acl2 3.1-1
  • links: PTS
  • area: main
  • in suites: etch, etch-m68k
  • size: 36,712 kB
  • ctags: 38,396
  • sloc: lisp: 464,023; makefile: 5,470; sh: 86; csh: 47; cpp: 25; ansic: 22
file content (3419 lines) | stat: -rw-r--r-- 141,490 bytes parent folder | download
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
; 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 NOTE-2-0.

; 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 78712-1188 U.S.A.

(in-package "ACL2")

;=================================================================

; This file defines the basics of the linear arithmetic decision
; procedure.  We also include clause histories, parent trees,
; tag trees, and assumptions; all of which are needed by add-poly
; and friends.

;=================================================================

; We begin with some general support functions.  They should
; probably be organized and moved to axioms.lisp.

(defabbrev ts-acl2-numberp (ts)
  (ts-subsetp ts *ts-acl2-number*))

(defabbrev ts-rationalp (ts)
  (ts-subsetp ts *ts-rational*))

(defabbrev ts-integerp (ts)
  (ts-subsetp ts *ts-integer*))

(defun all-quoteps (lst)
  (cond ((null lst) t)
        (t (and (quotep (car lst))
                (all-quoteps (cdr lst))))))

(mutual-recursion

(defun dumb-occur (x y)

; This function determines if term x occurs in term y, but does not
; look for x inside of quotes.  It is thus equivalent to occur if you
; know that x is not a quotep.

  (cond ((equal x y) t)
        ((variablep y) nil)
        ((fquotep y) nil)
        (t (dumb-occur-lst x (fargs y)))))

(defun dumb-occur-lst (x lst)
  (cond ((null lst) nil)
        (t (or (dumb-occur x (car lst))
               (dumb-occur-lst x (cdr lst))))))

)

;=================================================================

; Clause Histories

; Clauses carry with them their histories, which describe which processes
; have produced them.  A clause history is a list of history-entry records.
; A process, such as simplify-clause, might inspect the history of its
; input clause to help decide whether to perform a certain transformation.

(defrec history-entry
  (processor ttree . signal)
  t)

; Important Note: This record is laid out this way so that we can use
; assoc-eq on histories to detect the presence of a history-entry for
; a given processor.  Do not move the processor field out of the caar!

; Processor is a waterfall processor (e.g., 'simplify-clause).  The
; ttree and signal are, respectively, the ttree and signal produced by
; the processor on clause.  Each history-entry is built in the
; waterfall, but we inspect them for the first time in this file.

;=================================================================

; Essay on Parent Trees

; Structurally, a "parent tree" or pt is either nil, a number, or the cons
; of two parent trees.  Parent trees are used to represent sets of
; literals.  In particular, every number in a pt is the position of some
; literal in the current-clause variable of simplify-clause1 and the tree
; may be thought of as representing that set of literals.  Pts are used
; to avoid tail biting.  An earlier implementation of this used "clause-tails."
; We explain everything below.

; "Tail biting" is our name for the insidious phenomenon that occurs when
; one assumes p false while trying to prove p and then, carelessly,
; rewrites the goal p to false on the basis of that assumption.  Observe
; that this is sound but detrimental to success.  One way to prevent
; tail-biting is to not assume p false while trying to prove it, but we
; found that too weak.  The way we avoid tail biting is to keep careful
; track of what we're trying to prove, which literal we are working on,
; and what assumptions have been used to derive what results; we never use
; the assumption that p is false (or anything derived from it) to rewrite
; p to false.  Despite our efforts, tail biting by simplify-clause is
; possible.  See "On Tail Biting by Simplify-clause" for more.

; The easiest to understand use of parent trees in this regard is in
; linear arithmetic.  In simplify-clause1 we setup the
; simplify-clause-pot-lst, by expressing all the arithmetic hypotheses of
; the conjecture as polynomial inequalities.  When new inequalities are
; introduced, as when trying to relieve the hypothesis of some rule, we
; can combine them with the preprocessed "polys" to quickly settle certain
; arithmetic statements.  To avoid duplication of effort, our
; simplify-clause-pot-lst contains polys derived from all possible
; literals of the current clause.  This is because a great deal of work
; may be done (via linear lemmas and rewriting) to derive a poly about a
; given suggestive subterm of a given literal and we do not want to do it
; each time we assume that literal false.  Note the ease with which we
; could bite our tail: the list of inequalities is derived from the
; negations of every literal so we might easily use an inequality to
; falsify the literal from which it was derived.  To avoid this, each poly
; is tagged with one or more parent trees.  Intuitively the poly derived
; from an inequality literal is tagged with that literal.  But other
; literals may have been used, e.g., to establish certain terms rational,
; so one must think of the polys as being tagged with sets of literals.
; Then, when we are rewriting a particular literal we tell ourselves (by
; making a note in the :pt field of the rcnst) to avoid any poly
; descending from the goal literal.  Similar use is made of parent trees
; in the fc-pair-lst -- a list of preprocessed conclusions obtained by
; forward chaining from the current clause.

; The problem is made subtle by the fact that the literals we are
; rewriting change before we get to them and thus cannot be recognized by
; their structure alone.  Consider the clause {lit1 lit2 lit3}.  Now
; suppose we forward chain from ~lit3 and deduce concl.  Then fc-pair-lst
; will contain (concl . ttree) where ttree contains a parent tree
; acknowledging our dependence on lit3.  We may thus use concl when we are
; working on lit1 and lit2.  But suppose that in simplifying lit1 we
; produce the literal (not (equal var 27)).  Then we can substitute 27 for
; var everywhere and will actually do so.  Thus, by the time we get to
; work on the third literal of the clause above it will not be lit3 but
; some reduced instance, lit3', of lit3.  If the parent tree literally
; contained lit3, it would be impossible to recognize that concl was to be
; avoided.

; Therefore, we actually refer to literals by their position in the
; current-clause of simplify-clause1 (from which the preprocessing was
; done) and we keep careful track as we simplify what the original pt for
; each literal was.  As we scan over the literals to simplify we maintain
; a map, an enumeration of pts, giving the pt for each literal.  Thus,
; while we actually go to work on lit3' above, we will actually have in
; our hand the fact that lit3 is its parent.  Keeping track of the parents
; of the literals we are working on is made harder by the fact that
; sometimes literal merge.  For example, in {lit1 lit2 lit3} lit1 may
; simplify to lit3 and thus we may merge them.  The surviving literal is
; given the parent tree that contains both 1 and 3 so we know not to use
; conclusions derived from either.  The rewrite-constant, rcnst, in use
; below simplify-clause1 contains as one of its fields the
; :current-clause.  Thus, given the rewrite-constant and a pt it is
; possible to recover the original parent literals.

; We generally use "pt" to refer to a single parent tree.  "Pts" is a list
; of parent trees, implicitly in "weak 1:1 correspondence" with some list
; of terms.  By "weak" we mean pts may be shorter than the list of terms
; and "excess terms" have the nil pt.  That is, it is ok to cdr pts as you
; cdr down the list of terms and every time you need a pt for a term you
; take the car of pts.  There is no need to store the nil pt in tag trees,
; so we don't.  Thus, a commonly used convention is to supply a pts of nil
; to a function that stores 'pts, causing it to store no pts.

; In the early days we did not use parent trees but "clause-tails" -- the
; tail of clause starting with the parent literal.  This was adopted to
; avoid the confusion caused by duplicate literals.  But it was rendered
; unworkable when we implemented the Satriani hacks and started
; substituting for variables as we went.  It also suffered other problems
; due to sloppy implementation.

(defun pt-occur (n pt)

; Determine whether n occurs in the set denoted by pt.

  (cond ((null pt) nil)
        ((consp pt) (or (pt-occur n (car pt)) (pt-occur n (cdr pt))))
        (t (= n pt))))

(defun pt-intersectp (pt1 pt2)

; Determine whether the intersection of the sets denoted by pt1 and pt2
; is nonempty.

  (cond ((null pt1) nil)
        ((consp pt1)
         (or (pt-intersectp (car pt1) pt2)
             (pt-intersectp (cdr pt1) pt2)))
        (t (pt-occur pt1 pt2))))

;=================================================================

; Essay on Tag Trees

; If you add a new tag, be sure to include it in all-runes-in-ttree!

; Tags in Tag Trees

; The tags in use as of this writing (which can be verified by searching
; for add-to-tag-tree) and their meanings are:

; 'lemma

; The tagged object is either a lemma name (a symbolp) or else is the
; integer 0 indicating the use of linear arithmetic.

; 'pt

; The tagged object is a "parent tree".  See the Essay on Parent Trees.
; The tree identifies a set of literals in the current-clause of
; simplify-clause1 used in the derivation of poly or term with which the
; tree is associated.  We need this information for two reasons.  First,
; in order to avoid tail biting (see below) we do not use any poly that
; descends from the assumption of the falsity of the literal we are trying
; to prove.  Second, in find-equational-poly we seek two polys that can be
; combined to derive an equality, and we use 'pt to identify those that
; themselves descend from equality hypotheses.

; 'assumption

; The tagged object is an assumption record containing, among other things, a
; type-alist and a term which must be true under the type-alist in order to
; assure the validity of the poly or rewrite with which the tree is associated.
; We cannot linearize (- x), for example, without knowing (rationalp x).  If we
; cannot establish it by type set reasoning, we add that 'assumption to the
; poly generated.  If we eventually use the poly in a derivation, the
; 'assumption will infect it and when we get up to the simplify-clause level we
; will split on them.

; 'find-equational-poly

; The tagged object is a pair of polynomials.  During simplify clause
; we try to find two polys that can be combined to form an equation we
; don't have explicitly in the clause.  If we succeed, we add the
; equation to the clause.  However, it may be simplified into
; unrecognizable form and we need a way to avoid re-generation of the
; equation in future calls of simplify.  We do this by infecting the
; tag-tree with this tag and the two polys used.

; Historical Note:

; The invention of tag trees came about during the designing of the
; linear package.  Polynomials have three "arithmetic" fields, the
; constant, alist, and relation.  But they then have many other
; fields, like lemmas, assumptions, and literals.  At the time
; of this writing they have 5 other fields.  All of these fields are
; contaminants in the sense that all of the contaminants of a poly
; contaminate any result formed from that poly.  The same is true with
; the second answer of rewrite.

; If we represented the 5-tuple of the ttree of a poly as full-fledged
; fields in the poly the best we could do is to use a balanced binary
; tree with 8 tips.  In that case the average time to change some
; field (including the time to cons a new element onto any of the 5
; contaminants) is 3.62 conses.  But if we clump all the contaminants
; into a single field represented as a tag tree, the cost of adding a
; single element to any one of them is 2 conses and the average cost
; of changing any of the 4 fields in a poly is 2.5 conses.
; Furthermore, we can effectively union all 5 contaminants of two
; different polys in one cons!

(deflabel ttree
  :doc
  ":Doc-Section Miscellaneous

  tag trees~/

  Many low-level ACL2 functions take and return ``tag trees'' or
  ``ttrees'' (pronounced ``tee-trees'') which contain various useful
  bits of information such as the lemmas used, the linearize
  assumptions made, etc.~/

  Let a ``tagged pair'' be a list whose car is a symbol, called the
  ``tag,'' and whose cdr is an arbitrary object, called the ``tagged
  object.''  A ``tag tree'' is either nil, a tagged pair consed onto a
  tag tree, or a non-nil tag tree consed onto a tag tree.

  Abstractly a tag tree represents a list of sets, each member set
  having a name given by one of the tags occurring in the ttree.  The
  elements of the set named ~c[tag] are all of the objects tagged
  ~c[tag] in the tree.  To cons a tagged pair ~c[(tag . obj)] onto a
  tree is to ~c[add-to-set-equal] ~c[obj] to the set corresponding to
  ~c[tag].  To ~c[cons] two tag trees together is to union-equal the
  corresponding sets.  The concrete representation of the union so
  produced has duplicates in it, but we feel free to ignore or delete
  duplicates.

  The beauty of this definition is that to combine two non-~c[nil] tag
  trees you need do only one ~c[cons].

  The following function accumulates onto ans the set associated with
  a given tag in a ttree:
  ~bv[]
  (defun tagged-objects (tag ttree ans)
   (cond
    ((null ttree) ans)
    ((symbolp (caar ttree))             ; ttree = ((tag . obj) . ttree)
     (tagged-objects tag (cdr ttree)
                     (cond ((eq (caar ttree) tag)
                            (add-to-set-equal (cdar ttree) ans))
                           (t ans))))
    (t                                  ; ttree = (ttree . ttree)
       (tagged-objects tag (cdr ttree)
                           (tagged-objects tag (car ttree) ans)))))
  ~ev[]
  This function is defined as a :~ilc[PROGRAM] mode function in ACL2.

  The rewriter, for example, takes a term and a ttree (among other
  things), and returns a new term, term', and new ttree, ttree'.
  Term' is equivalent to term (under the current assumptions) and the
  ttree' is an extension of ttree.  If we focus just on the set
  associated with the tag ~c[LEMMA] in the ttrees, then the set for
  ttree' is the extension of that for ttree obtained by unioning into
  it all the runes used by the rewrite.  The set associated with
  ~c[LEMMA] can be obtained by ~c[(tagged-objects 'LEMMA ttree nil)].")

; The following function determines whether val with tag tag occurs in
; tree:

(defun tag-tree-occur (tag val tree)
  (cond ((null tree) nil)
        ((symbolp (caar tree))
         (or (and (eq tag (caar tree))
                  (equal val (cdar tree)))
             (tag-tree-occur tag val (cdr tree))))
        (t (or (tag-tree-occur tag val (car tree))
               (tag-tree-occur tag val (cdr tree))))))

; To add a tagged object to a tree we use the following function.  Observe
; that it does nothing if the object is already present.

; Note:
; If you add a new tag, be sure to include it in all-runes-in-ttree!

(defun add-to-tag-tree (tag val tree)
  (cond ((tag-tree-occur tag val tree) tree)
        (t (cons (cons tag val) tree))))

; A Little Foreshadowing:

; We will soon introduce the notion of a "rune" or "rule name."  To
; each rune there corresponds a numeric equivalent, or "nume," which
; is the index into the "enabled structure" for the named rule.  We
; push runes into ttrees under the 'lemma property to record their
; use.

; We have occasion for "fake-runes" which look like runes but are not.
; See the Essay on Fake-Runes below.  One such rune is shown below,
; and is the name of otherwise anonymous rules that are always considered
; enabled.  When this rune is used, its use is not recorded in the
; tag tree.

(defconst *fake-rune-for-anonymous-enabled-rule*
  '(:FAKE-RUNE-FOR-ANONYMOUS-ENABLED-RULE nil))

(defun push-lemma (rune tree)

; This is just (add-to-tag-tree 'lemma rune ttree) and is named in
; honor of the corresponding act in Nqthm.  We do not record uses of
; the fake rune.  Rather than pay the price of recognizing the
; *fake-rune-for-anonymous-enabled-rule* perfectly we exploit the fact
; that no true rune has :FAKE-RUNE-FOR-ANONYMOUS-ENABLED-RULE as its
; token.

  (cond ((eq (car rune) :FAKE-RUNE-FOR-ANONYMOUS-ENABLED-RULE) tree)
        ((tag-tree-occur 'lemma rune tree) tree)
        (t (cons (cons 'lemma rune) tree))))

(defun push-lemmas (runes tree)
  (cond ((null runes) tree)
        (t (push-lemmas (cdr runes) (push-lemma (car runes) tree)))))

; To join two trees we use cons-tag-trees.  Observe that if the first
; tree is nil we return the second (we can't cons a nil tag tree on
; and their union is the second anyway).  Otherwise we cons, possibly
; duplicating elements.

(defun cons-tag-trees (tree1 tree2)
  (cond ((null tree1) tree2)
        ((null tree2) tree1)
        (t (cons tree1 tree2))))

(defun tagged-objects (tag ttree ans)

; We accumulate in reverse order onto ans all the objects with the given tag
; in ttree.  We accumulate with add-to-set-equal.

  (cond
   ((null ttree) ans)
   ((symbolp (caar ttree))
    (tagged-objects tag (cdr ttree)
                    (cond ((eq (caar ttree) tag)
                           (add-to-set-equal (cdar ttree) ans))
                          (t ans))))
   (t (tagged-objects tag (cdr ttree)
                      (tagged-objects tag (car ttree) ans)))))

(defun tagged-object (tag ttree)

; This function returns the first (tag . obj) it finds in ttree or nil
; if there is no object with that tag.  We don't usually think of
; there being an ordering on the subtrees.  Indeed, if the tree was
; constructed entirely via cons-tag-trees and add-to-tag-tree then
; there is not a lot of sense to this notion of "first" because those
; operations don't necessarily change the tree (treating it as a set
; of (tag . obj) pairs).  In particular, it is not a theorem that
; (tagged-object tag (add-to-tag-tree tag obj ttree)) = (cons tag
; obj), because there may be a deep occurrence of (tag . obj) in ttree
; already but it is covered by some (tag . obj').  Therefore, on such
; ttrees we use this function only when we know there is at most one
; occurrence of the tag or when we wish merely to determine if there
; is at least one occurrence but don't care which we find.

  (cond
   ((null ttree) nil)
   ((symbolp (caar ttree))
    (cond ((eq (caar ttree) tag)
           (car ttree))
          (t (tagged-object tag (cdr ttree)))))
   (t (or (tagged-object tag (car ttree))
          (tagged-object tag (cdr ttree))))))

; We accumulate our ttree into the state global 'accumulated-ttree so that if a
; proof attempt is aborted, we can still recover the lemmas used within it.  If
; we know a ttree is going to be part of the ttree returned by a successful
; event, then we want to store it in state.  We are especially concerned about
; storing a ttree if we are about to inform the user, via output, that the
; runes in it have been used.  (That is, we want to make sure that if a proof
; fails after the system has reported using some rune then that rune is tagged
; as a 'lemma in the 'accumulated-ttree of the final state.)  This encourages
; us to cons a new ttree into the accumulator every time we do output.  But
; there is a problem.  It is not unusual to construct a ttree by incrementally
; adding to another one.  But if the initial ttree has already been accumulated
; into state, then if we accumulate the final one too, we have actually
; produced two occurrences of the initial one in state.  We do not want to
; search the state's ttree to see if a ttree is already in it.  To avoid this,
; we engage in the following clever hack.  When we accumulate a ttree into
; state, we will mark the ttree as having been accumulated, by putting an
; 'accumulated-into-state tag with (irrelevant, non-nil) value t at the top of
; the tree, meaning that the rest of the ttree has already been added to state.
; To accumulate a ttree into state we actually explore it and only store those
; subtress that have not already been accumulated.

(defun scons-tag-trees (ttree1 ttree2)

; "Slow" or "Smart" cons-tag-trees.  Unions together the two trees but
; only conses those tagged values in ttree1 that are not already in
; ttree2.

  (cond ((null ttree1) ttree2)
        ((symbolp (caar ttree1))
         (scons-tag-trees (cdr ttree1)
                          (add-to-tag-tree (caar ttree1)
                                           (cdar ttree1)
                                           ttree2)))
        (t (scons-tag-trees (cdr ttree1)
                            (scons-tag-trees (car ttree1) ttree2)))))

(defun move-unmarked-subbtrees (ttree1 ttree2)

; This function i like scons-tag-trees, except that it ignores subtrees of
; ttree1 tagged with 'accumulated-into-state, which presumably are already
; included in ttree2.

  (cond
   ((null ttree1) ttree2)
   ((symbolp (caar ttree1))
    (cond ((eq (caar ttree1) 'accumulated-into-state)
           ttree2)
          (t (move-unmarked-subbtrees (cdr ttree1)
                                      (add-to-tag-tree (caar ttree1)
                                                       (cdar ttree1)
                                                       ttree2)))))
   (t
    (move-unmarked-subbtrees (cdr ttree1)
                             (move-unmarked-subbtrees (car ttree1) ttree2)))))

(defun reverse-marked-tag-tree-to-list (ttree acc)

; We create a list without duplicates, whose elements are the same as those in
; the given tag tree as though 'accumulated-ttree marks had been removed from
; ttree.  Moreover, if x occurs before y in ttree, then y occurs before x in
; the returned list.

  (cond ((null ttree) acc)
        ((symbolp (caar ttree))
         (cond ((eq (caar ttree) 'accumulated-into-state)
                (reverse-marked-tag-tree-to-list (cdr ttree) acc))
               (t
                (reverse-marked-tag-tree-to-list (cdr ttree)
                                                 (add-to-set-equal (car ttree) acc)))))
        (t (reverse-marked-tag-tree-to-list
            (cdr ttree)
            (reverse-marked-tag-tree-to-list (car ttree) acc)))))

(defun accumulate-ttree-into-state (ttree state)

; We add ttree to the 'accumulated-ttree in state and return an error triple
; whose value is equivalent to ttree, but with duplicates removed -- except
; that we mark the returned ttree as having been accumulated.

  (pprogn
   (f-put-global 'accumulated-ttree
                 (move-unmarked-subbtrees ttree
                                          (f-get-global 'accumulated-ttree state))
                 state)
   (value (cons (cons 'accumulated-into-state t)

; Note that in the following tag tree, elements occur in the same order as in
; ttree.  Although in principle tag trees represent (unordered) sets, in
; practice it is useful to preserve the order.  Otherwise, we have seen
; ordered-symbol-alistp-remove-first-pair-test in the :mini-proveall fail,
; probably because the order of elements is relevant to new proof-checker
; subgoals resulting from a call of remove-byes-from-tag-tree.

                (reverse (reverse-marked-tag-tree-to-list ttree nil))))))

(defun pts-to-ttree-lst (pts)
  (cond ((null pts) nil)
        (t (cons (add-to-tag-tree 'pt (car pts) nil)
                 (pts-to-ttree-lst (cdr pts))))))

; Previously, we stored the parents of a poly in the poly's :ttree field
; and used to-be-ignoredp.  However, tests have shown that under certain
; conditions to-be-ignoredp was taking up to 80% of the time spent by
; add-poly.  We now store the poly's parents in a seperate field and
; use ignore-polyp.  The next few functions are used in the implementation
; of this change.

(defun marry-parents (parents1 parents2)

; We return the 'eql union of the two arguments.  When we create a
; new poly from two other polys via cancellation, we need to ensure
; that the new poly depends on all the literals that either of the
; others do.

  (if (null parents1)
      parents2
    (marry-parents (cdr parents1)
                   (add-to-set-eql (car parents1) parents2))))

(defun collect-parents1 (pt ans)
  (cond ((null pt)
         ans)
        ((consp pt)
         (collect-parents1 (car pt)
                           (collect-parents1 (cdr pt) ans)))
        (t
         (add-to-set-eql pt ans))))

(defun collect-parents0 (ttree ans)
  (cond
   ((null ttree) ans)
   ((symbolp (caar ttree))
    (collect-parents0 (cdr ttree)
                      (cond ((eq (caar ttree) 'pt)
                             (collect-parents1 (cdar ttree) ans))
                            (t ans))))
   (t (collect-parents0 (cdr ttree)
                        (collect-parents0 (car ttree) ans)))))

(defun collect-parents (ttree)

; We accumulate in reverse order onto ans all the objects (parents) in
; the pts in the ttree.  When we create a new poly via linearize, we
; extract a list of all its parents from the poly's 'ttree and store
; this list in the poly's 'parents field.  This function does the
; extracting.

; This was copied from tagged-objects and modified.

  (collect-parents0 ttree nil))

(defun ignore-polyp (parents pt)

; Consider the set, P, of all parents mentioned in the list parents.
; Consider the set, B, of all parents mentioned in the parent tree pt.  We
; return t iff P and B have a non-empty intersection.  From a more applied
; perspective, assuming parents is the parents list associated with some
; poly, P is the set of literals upon which the poly depends.  B is
; generally the set of literals we are to avoid dependence upon.  The poly
; should be ignored if it depends on some literal we are to avoid.

  (if (null parents)
      nil
    (or (pt-occur (car parents) pt)
        (ignore-polyp (cdr parents) pt))))

(defun to-be-ignoredp (ttree pt)

; Consider the set, P, of all parents mentioned in the 'pt tags of ttree.
; Consider the set, B, of all parents mentioned in the parent tree pt.  We
; return t iff P and B have a non-empty intersection.  From a more applied
; perspective, assuming ttree is the tree associated with some poly, P is
; the set of literals upon which the poly depends.  B is generally the set
; of literals we are to avoid dependence upon.  The poly should be ignored
; if it depends on some literal we are to avoid.

; This function was originally written to do the job described above.
; But then Robert Krug suggested the efficiency of maintaining the
; parents list and introduced ignore-polyp.  Now this function is only
; used elsewhere, but the above comments still apply mutatis mutandis.

  (cond ((null ttree)
         nil)
        ((symbolp (caar ttree))
         (cond ((eq (caar ttree) 'pt)
                (or (pt-intersectp (cdar ttree) pt)
                    (to-be-ignoredp (cdr ttree) pt)))
               (t (to-be-ignoredp (cdr ttree) pt))))
        (t (or (to-be-ignoredp (car ttree) pt)
               (to-be-ignoredp (cdr ttree) pt)))))


;=================================================================


; Assumptions

; We are prepared to force assumptions of certain terms by adding
; them to the tag tree under the 'assumption tag.  This is always done
; via force-assumption.  All assumptions are embedded in an
; assumption record:

(defrec assumnote (cl-id rune . target) t)

; The cl-id is the clause id (as maintained by the waterfall) of the clause
; currently being worked upon.  Rune is either the rune (or a symbol, as per
; force-assumption) that forced this assumption.  Target is the term to which
; rune was being applied.  Because the :assumnotes field of an assumption is
; always non-nil, there is at least one assumnote in it, but the cl-id field in
; that assumnote might be nil because we do not know the clause id just yet.
; We fill in the :cl-id field later so that we don't have to pass such static
; information all the way down to the places where assumptions are forced.
; When an assumption is generated, it has exactly one assumnote.  But later we
; will "merge" assumptions together (actually, delete some via subsumption) and
; when we do we will union the assumnotes together to keep track of why we are
; dealing with that assumption.

(defrec assumption
  ((type-alist . term) immediatep rewrittenp . assumnotes)
  t)

; An assumption record records the fact that we must prove term under
; the assumption of type-alist.  Immediatep indicates whether it is
; the user's desire to split the main goal on term immediately
; (immediatep = 'case-split), prove the term under alist immediately
; (t) or delay the proof to a forcing round (nil).  

; WARNING: The system can be unsound if immediatep takes on any but
; these three values.  In functions like collect-assumptions we assume
; that collecting all the 'case-splits and then collecting all the t's
; gets all the non-nils!

; Assumnotes is involved with explaining to the user what we are doing.  It is
; a non-empty list of assumnote records.

; We now turn to the question of whether term has been rewritten or not.  If it
; has not been, and we know the context in which rewriting should be tried, it
; is presumably a good idea to try to rewrite term before we try a full-fledged
; proof: a proof requires converting the type-alist and term into a clause and
; then simplifying all the literals of that clause, whereas we expect many
; times that the type-alist will allow term to rewrite to t.  One might ask why
; we don't always rewrite before forcing.  The answer is simple: type-set
; forces and cannot use the rewriter because it is defined well before the
; rewriter.  So type-set forces unrewritten terms often.  The problem with the
; simple idea of trying first to prove those terms by rewriting is that REWRITE
; takes many additional context-specifying arguments, the most complicated
; being the simplify-clause-pot-lst.  Having set the stage for an explanation,
; we now give it:

; Rewrittenp indicates whether we have already tried to rewrite term.  Recall
; that relieve-hyp first rewrites and forces the rewritten term only if
; rewriting fails.  Thus, at least within the rewriter, we will see both
; rewritten and unrewritten assumptions coming back in the ttrees we generate.
; Rewrittenp is either a term or nil.  If it is a term, forced-term, then it is
; the term we were asked to force and term is the result of rewriting
; forced-term.  We use the unrewritten term in a heuristic that sometimes
; throws out supposedly irrelevant hypotheses from the clauses we ultimately
; prove to establish the assumptions.  See the discussion of "disguarding."  If
; rewrittenp is nil, we have not yet tried to rewrite term and term is
; literally what was forced.  The simplifier will collect the unrewritten
; assumptions generated during rewrite and will rewrite them in the
; "appropriate context" as discussed below.

; The view we take is that from within the rewriter, all assumptions are
; rewritten before being forced.  That cannot be implemented directly, so
; we do it cleverly, by rewriting them after the force but not telling
; the user.  It just seems like a good idea for the rewriter, of all the
; processes, to produce only rewritten assumptions.  Now those rewritten
; assumptions aren't maximally rewritten.  For example, an assumption
; might rewrite to an if and normalization etc. might produce a provable
; set of assumptions.  But we do not use normalization or clausification on
; assumptions until it is time to hit them with the full prover.

; The following record definition is decidedly out of place, belonging as it
; does to the code for forward-chaining.  But we must make it now to allow
; us to define contain-assumptionp.  This record is documented in comments
; in the essay entitled:  "Forward Chaining Derivations - fc-derivation - fcd"

(defrec fc-derivation
  ((rune . concl) (fn-cnt . p-fn-cnt) (inst-trigger . ttree))
  t)

; WARNING: If you change fc-derivation, go visit the "virtual" declaration of
; the record in simplify.lisp and update the comments.  See the essay "Forward
; Chaining Derivations - fc-derivation - fcd".

(defun contains-assumptionp (ttree)

; We return t iff ttree contains an assumption "at some level" where we
; know that 'fc-derivations contain ttrees that may contain assumptions.
; See the discussion in force-assumption.

  (cond ((null ttree) nil)
        ((symbolp (caar ttree))
         (cond 
          ((eq (caar ttree) 'assumption) t)
          ((eq (caar ttree) 'fc-derivation)
           (or (contains-assumptionp (access fc-derivation (cdar ttree) :ttree))
               (contains-assumptionp (cdr ttree))))
          (t (contains-assumptionp (cdr ttree)))))
        (t (or (contains-assumptionp (car ttree))
               (contains-assumptionp (cdr ttree))))))

(defun remove-ttrees-from-type-alist (type-alist)

; We delete from type-alist any entry, (term ts . ttree), whose ttree contains
; an assumption.  Then we delete all the ttrees!  Thus, if ttree2 below is the
; only one of the three to contain an assumption, the type-alist
; ((v1 ts1 . ttree1)(v2 ts2 . ttree2)(v3 ts3 . ttree3))
; is transformed into
; ((v1 ts1 . nil) (v3 ts3 . nil)).

; It is always sound to delete a hypothesis.  See the discussion in
; force-assumption.

  (cond
   ((null type-alist) nil)
   ((contains-assumptionp (cddar type-alist))
    (remove-ttrees-from-type-alist (cdr type-alist)))
   (t (cons (list* (caar type-alist)
                   (cadar type-alist)
                   nil)
            (remove-ttrees-from-type-alist (cdr type-alist))))))

(defun force-assumption1
  (rune target term type-alist rewrittenp immediatep ttree)

  (let* ((term (cond ((equal term *nil*)
                      (er hard 'force-assumption
                          "Attempt to force nil!"))
                     ((null rune)
                      (er hard 'force-assumption
                          "Attempt to force the nil rune!"))
                     (t term))))
    (cond ((not (member-eq immediatep '(t nil case-split)))
           (er hard 'force-assumption1
               "The :immediatep of an ASSUMPTION record must be ~
                t, nil, or 'case-split, but we have tried to create ~
                one with ~x0."
               immediatep))
          (t
           (add-to-tag-tree 'assumption
                            (make assumption
                                  :type-alist type-alist
                                  :term term
                                  :rewrittenp rewrittenp
                                  :immediatep immediatep
                                  :assumnotes
                                  (list (make assumnote
                                              :cl-id nil
                                              :rune rune
                                              :target target)))
                            ttree)))))

(defun dumb-occur-in-type-alist (var type-alist)
  (cond
   ((null type-alist)
    nil)
   ((dumb-occur var (caar type-alist))
    t)
   (t
    (dumb-occur-in-type-alist var (cdr type-alist)))))

(defun all-dumb-occur-in-type-alist (vars type-alist)
  (cond
   ((null vars)
    t)
   (t (and (dumb-occur-in-type-alist (car vars) type-alist)
           (all-dumb-occur-in-type-alist (cdr vars) type-alist)))))

(defun force-assumption
  (rune target term type-alist rewrittenp immediatep force-flg ttree)

; Warning:  Rune may not be a rune!  It may be a function symbol.

; This function adds (implies type-alist' term) as an 'assumption to ttree.
; Rewrittenp is either nil, meaning term has not yet been rewritten, or is the
; term that was rewritten to obtain term.  Rune is the name of the rule in
; whose behalf term is being assumed, and rune is being applied to the target
; term target.  If rune is a symbol then it is actually a primitive
; function symbol and this is a split on the guard of that symbol.  There is
; even an exception to that: sometimes rune is the function symbol equal.  But
; the guard of equal is t and so is never forced!  What is going on?  In
; linearize we force term2 to be real if term1 is real and we are
; linearizing (equal term1 term2).

; The type-alist actually stored in the assumption record, type-alist', is not
; type-alist!  We first remove from type-alist all the entries depending upon
; assumptions.  Then we delete all ttrees from the type-alist.  It is
; legitimate to throw away any hypothesis, thus we can delete the entries we
; choose.  Why do we throw out the type-alist entries depending on assumptions?
; The reason is that in the forcing round we actually generate a formula
; representing (implies type-alist' term) and this formula does not encode the
; fact that a given hyp depends upon certain assumptions.

; Because assumptions can be generated during forward chaining, the type-alist
; may contain 'fc-derivations tags among its ttrees.  These records record how
; a given hypothesis was derived and may itself have 'assumptions in its ttree.
; We therefore consider a ttree to "contain assumptions" if it contains an
; fc-derivation that contains assumptions.

; It could be thought that the creation of type-alist' from type-alist is
; merely an efficiency aimed at saving a few conses.  This is not correct.
; This change has a dramatic effect on the size of our ttrees.  Before we did
; this, it was possible for a ttree to contain an assumption which (by virtue
; of the :type-alist) contained a ttree which contained an assumption which
; contained a ttree, etc.  We have seen this sort of thing nested to depth 9.
; Furthermore, it was frequently the case that a ttree contained some proper
; subttree x which occurred also in an assumption contained in the parent
; ttree.  Thus, the ttree x was duplicated.  While the parent ttree was small
; (in the sense that it contained on a few nodes) the tree was very large when
; printed, because of this duplication.  We have seen a ttree that contained 5
; million nodes (when explored in this root-and-branch way through 'assumptions
; and 'fc-derivations) but which actually was composed of only 100 distinct
; (non-equal) subtrees.  Again, one might think this was a problem only if one
; printed out the ttree, but some processes, such as expunge-fc-derivations, do
; root-and-branch exploration.  On the tree in question the system simply hung
; up and appeared to be in an infinite loop.  This fix keeps ttrees small (even
; when viewed in the root-and-branch way) and is crucial to our practice of
; using them.

; Once upon a time, we allowed rune to be nil.  We have since changed that and
; now use the *fake-rune-for-anonymous-enabled-rule* when we don't know a
; better rune.  But we have put a check in here to make sure no one uses the
; nil "rune" anymore.  Wanting a genuine rune here is just a reflection of the
; output routine that explains the origins of each forcing round.

; Force-flg is known to be non-nil; it may be either t or 'weak.  It's tempting
; to allow force-flg = nil and handle that case here (trivially), but the case
; structure in functions like type-set-binary-+ suggests that it's better to
; deal with that case up front, in order to avoid lots of tests that are
; irrelevant (since the same trivial thing happens in all cases when force-flg
; is nil).

; This function is a No-Change Loser, meaning that if it fails and returns nil
; as its first result, it returns the unmodified ttree as its second.  Note
; that either force-flg or nil is returned as the first argument; hence, a
; "successful" force with force-flg = 'weak will result in an unchanged
; force-flg being returned.  If the first value returned is nil, we are to
; pretend that we weren't allowed to force in the first place.

; At the time of this writing we have temporarily abandoned the idea of
; allowing force-flg to be 'weak:  it will always be t or nil.  See the comment
; in ok-to-force.

  (let ((type-alist (remove-ttrees-from-type-alist type-alist)))
    (cond
     ((not force-flg)
      (mv force-flg
          (er hard 'force-assumption
              "Force-assumption called with null force-flg!")))

; We experimented with allowing force-flg to be 'weak.  However, currently
; force-flg is known to be t or nil.  See the comment in ok-to-force.

     #|
     ((or (eq force-flg t)
          (all-dumb-occur-in-type-alist (all-vars term) type-alist))
      (mv force-flg
          (force-assumption1
           rune target term type-alist rewrittenp immediatep ttree)))
     (t
      (mv nil ttree))
     |#
     (t (mv force-flg
            (force-assumption1
             rune target term type-alist rewrittenp immediatep ttree))))))

(defun tag-tree-occur-assumption-nil (ttree)

; This is just (tag-tree-occur 'assumption <*nil*> ttree) where by <*nil*> we 
; mean any assumption record with :term *nil*.

  (cond ((null ttree) nil)
        ((symbolp (caar ttree))
         (or (and (eq (caar ttree) 'assumption)
                  (equal (access assumption (cdar ttree) :term) *nil*))
             (tag-tree-occur-assumption-nil (cdr ttree))))
        (t (or (tag-tree-occur-assumption-nil (car ttree))
               (tag-tree-occur-assumption-nil (cdr ttree))))))

;; Could we just check (not (tagged-object 'assumption ttree)) instead
;; of assumption-free-ttreep in various places?

(defun assumption-free-ttreep (ttree)

; This is a predicate that returns t if ttree contains no 'assumption
; tag.  It also checks for 'fc-derivation tags, since they could hide
; 'assumptions.  An error-causing version of this function is
; chk-assumption-free-ttree.  Keep these two in sync.

  (cond ((tagged-object 'assumption ttree) nil)
        ((tagged-object 'fc-derivation ttree) nil)
        (t t)))

; The following assumption is impossible to satisfy and is used as a marker
; that we sometimes put into a ttree to indicate to our caller that the
; attempted force should be abandoned.

(defconst *impossible-assumption*
  (make assumption
        :type-alist nil
        :term *nil*
        :rewrittenp *nil*
        :immediatep nil ; must be t, nil, or 'case-split
        :assumnotes (list (make assumnote
                                :cl-id nil
                                :rune *fake-rune-for-anonymous-enabled-rule*
                                :target *nil*))))


;=================================================================


; We are about to get into the linear arithmetic stuff quite heavily.
; This code started in Nqthm in 1979 and migrated more or less
; untouched into ACL2, with the exception of the addition of the
; rationals.  However, around 1998, Robert Krug began working on an
; improved arithmetic book and after a year or so realized he wanted
; to make serious changes in the linear arithmetic procedures.
; Robert's hand is now felt all over this code.


; Essay on the Logical Basis for Linear Arithmetic.

; This essay was written for some early version of ACL2.  It still
; applies to the linear arithmetic decision procedure as of Version_2.7,
; although some of the details may need revision.

; We list here the "algebraic laws" we assume.  We point back to this
; list from the places we assume them.  It is crucial to realize that
; by < and + here we do not mean the familiar "guarded" functions of
; Common Lisp and algebra, but rather the "completed" functions of the
; ACL2 logic.  In particular, nonnumeric arguments to + are defaulted
; to 0 and complex numbers may be added to rational ones to yield
; complex ones, etc.  The < relation coerces nonnumeric arguments to 0
; and then compares the resulting numbers lexicographically on the
; real and imaginary parts, using the familiar less-than relation on
; the rationals.

; Let us use << as the "familiar" less-than.  Then
; (< x y) = (let ((x1 (if (acl2-numberp x) x 0))
;                 (y1 (if (acl2-numberp y) y 0)))
;            (or (<< (realpart x1) (realpart y1))
;                (and (= (realpart x1) (realpart y1))
;                     (<< (imagpart x1) (imagpart y1)))))

; The wonderful thing about this definition, is that it enjoys the algebraic
; laws we need to support linear arithmetic.  The "box" below contains the
; complete listing of the algegraic laws supporting linear arithmetic
; ("alsla").

; However, interspersed around them in the box are some events that ACL2's
; completed < and + have the ALSLA properties.  To enable us to use the theorem
; prover, we define some new symbols like < and + and prove that those symbols
; have the desired properties.  This is a bit tricky because the completed <
; and + must be defined in terms of the partial < and + which work on the
; rationals and complexes, respectively, and we do not want to rely on any
; built in properties of those primitive symbols.

; Therefore, we constrain three new symbols, PLUS, TIMES, and LESSP which you
; may think of as being the familiar, partial versions of +, *, and <.
; (Indeed, the witnesses in the constraints are those primitives.  The
; encapsulate below merely exports the properties that we are going to assume.)
; Then we define completed versions of these functions, called CPLUS, CTIMES,
; and CLESSP and we prove the ALSLA properties of those functions.

; Note: This exercise is still suspicious because it involves equality
; goals between arithmetic terms and there is no reason to believe that our
; "untrusted" linear arithmetic isn't contributing to their proof.  Well, a
; search through the output produces no sign of "linear" after the
; encapsulation below, but that could indicate an io bug.  A more convincing
; proof would be to eliminate the use of the arithmetic data types altogether
; but that would be a little nasty, faking rationals and complexes.  A still
; more convincing proof would be to construct the proof formally, as we hope to
; do when we have proof objects.

#|

(progn

; Perhaps this axiom can be proved from given ones, but I haven't taken the
; time to work it out.  I will add it.  I believe it!

(defaxiom *-preserves-<
  (implies (and (rationalp c)
                (rationalp x)
                (rationalp y)
                (< 0 c))
           (equal (< (* c x) (* c y))
                  (< x y))))

(defthm realpart-rational
  (implies (rationalp x) (equal (realpart x) x)))

(defthm imagpart-rational
  (implies (rationalp x) (equal (imagpart x) 0)))

(encapsulate (((plus * *) => *)
              ((times * *) => *)
              ((lessp * *) => *))

; Plus and lessp here are the rational versions of those functions.  They are
; intended to be the believable, intuitive, functions.  You should read the
; properties we export to make sure you believe that the high school plus and
; lessp have those properties.  We prove the properties, but we prove them from
; witnesses of plus and lessp that are ACL2's completed + and < supported by
; ACL2's linear arithmetic and hence, if the soundness of ACL2's arithmetic is
; in doubt, as it is in this exercise, then no assurrance can be drawn from the
; constructive nature of this axiomatization of rational arithmetic.

             (local (defun plus (x y)
                      (declare (xargs :verify-guards nil))
                      (+ x y)))
             (local (defun times (x y)
                      (declare (xargs :verify-guards nil))
                      (* x y)))
             (local (defun lessp (x y)
                      (declare (xargs :verify-guards nil))
                      (< x y)))
             (defthm rationalp-plus
               (implies (and (rationalp x)
                             (rationalp y))
                        (rationalp (plus x y)))
               :rule-classes (:rewrite :type-prescription))
             (defthm plus-0
               (implies (rationalp x)
                        (equal (plus 0 x) x)))
             (defthm plus-commutative-and-associative
               (and (implies (and (rationalp x)
                                  (rationalp y))
                             (equal (plus x y) (plus y x)))
                    (implies (and (rationalp x)
                                  (rationalp y)
                                  (rationalp z))
                             (equal (plus x (plus y z))
                                    (plus y (plus x z))))
                    (implies (and (rationalp x)
                                  (rationalp y)
                                  (rationalp z))
                             (equal (plus (plus x y) z)
                                    (plus x (plus y z))))))
             (defthm rationalp-times
               (implies (and (rationalp x)
                             (rationalp y))
                        (rationalp (times x y))))
             (defthm times-commutative-and-associative
               (and (implies (and (rationalp x)
                                  (rationalp y))
                             (equal (times x y) (times y x)))
                    (implies (and (rationalp x)
                                  (rationalp y)
                                  (rationalp z))
                             (equal (times x (times y z))
                                    (times y (times x z))))
                    (implies (and (rationalp x)
                                  (rationalp y)
                                  (rationalp z))
                             (equal (times (times x y) z)
                                    (times x (times y z)))))
               :hints
               (("Subgoal 2"
                 :use ((:instance associativity-of-*)
                       (:instance commutativity-of-* (x x)(y (* y z)))))))
             (defthm times-distributivity
               (implies (and (rationalp x)
                             (rationalp y)
                             (rationalp z))
                        (equal (times x (plus y z))
                               (plus (times x y) (times x z)))))
             (defthm times-0
               (implies (rationalp x)
                        (equal (times 0 x) 0)))
             (defthm times-1
               (implies (rationalp x)
                        (equal (times 1 x) x)))
             (defthm plus-inverse
               (implies (rationalp x)
                        (equal (plus x (times -1 x)) 0))
               :hints
               (("Goal"
                 :use ((:theorem (implies (rationalp x)
                                          (not (< 0 (+ x (* -1 x))))))
                       (:theorem (implies (rationalp x)
                                          (not (< (+ x (* -1 x)) 0))))))))
             (defthm plus-inverse-unique
               (implies (and (rationalp x)
                             (rationalp y)
                             (equal (plus x (times -1 y)) 0))
                        (equal x y))
               :rule-classes nil)
             (defthm lessp-irreflexivity
               (implies (rationalp x)
                        (not (lessp x x))))
             (defthm lessp-antisymmetry
               (implies (and (rationalp x)
                             (rationalp y)
                             (lessp x y))
                        (not (lessp y x))))
             (defthm lessp-trichotomy
               (implies (and (rationalp x)
                             (rationalp y)
                             (not (equal x y))
                             (not (lessp x y)))
                        (lessp y x)))
             (defthm lessp-plus
               (implies (and (rationalp x)
                             (rationalp y)
                             (rationalp u)
                             (rationalp v)
                             (lessp x y)
                             (not (lessp v u)))
                        (lessp (plus x u) (plus y v))))
             (defthm not-lessp-plus
               (implies (and (rationalp x)
                             (rationalp y)
                             (rationalp u)
                             (rationalp v)
                             (not (lessp y x))
                             (not (lessp v u)))
                        (not (lessp (plus y v) (plus x u)))))
             (defthm 1+trick-for-lessp
               (implies (and (integerp x)
                             (integerp y)
                             (lessp x y))
                        (not (lessp y (plus 1 x)))))
             (defthm times-positive-preserves-lessp
               (implies (and (rationalp c)
                             (rationalp x)
                             (rationalp y)
                             (lessp 0 c))
                        (equal (lessp (times c x) (times c y))
                               (lessp x y)))))

; Now we "complete" +, *, <, and <= to the complex rationals and thence to the
; entire universe.  The results are CPLUS, CTIMES, CLESSP, and CLESSEQP.  You
; should buy into the claim that these functions are what we intended in ACL2's
; completed arithmetic.

; Note: At first sight it seems odd to do it this way.  Why not just assume
; plus, above, is the familiar operation on the complex rationals?  We tried
; it and it didn't work very well, because ACL2 does not reason very well
; about complex arithmetic.  It seemed more direct to make the definition of
; complex addition and multiplication be explicit for the purposes of this
; proof.

(defun cplus (x y)
  (declare (xargs :verify-guards nil))
  (let ((x1 (fix x))
        (y1 (fix y)))
    (complex (plus (realpart x1) (realpart y1))
             (plus (imagpart x1) (imagpart y1)))))

(defun ctimes (x y)
  (declare (xargs :verify-guards nil))
  (let ((x1 (fix x))
        (y1 (fix y)))
    (complex (plus (times (realpart x1) (realpart y1))
                   (times -1 (times (imagpart x1) (imagpart y1))))
             (plus (times (realpart x1) (imagpart y1))
                   (times (imagpart x1) (realpart y1))))))

(defun clessp (x y)
  (declare (xargs :verify-guards nil))
  (let ((x1 (fix x))
        (y1 (fix y)))
    (or (lessp (realpart x1) (realpart y1))
        (and (equal (realpart x1) (realpart y1))
             (lessp (imagpart x1) (imagpart y1))))))

(defun clesseqp (x y)
  (declare (xargs :verify-guards nil))
  (not (clessp y x)))

; A trivial theorem about fix, allowing us hereafter to disable it.

(defthm fix-id (implies (acl2-numberp x) (equal (fix x) x)))

(in-theory (disable fix))

;-----------------------------------------------------------------------------
; The Algebraic Laws Supporting Linear Arithmetic (ALSLA)

; All the operators FIX their arguments
; (equal (+ x y) (+ (fix x) (fix y)))
; (equal (* x y) (* (fix x) (fix y)))
; (equal (< x y) (< (fix x) (fix y)))
; (fix x) = (if (acl2-numberp x) x 0)

(defthm operators-fix-their-arguments
  (and (equal (cplus x y) (cplus (fix x) (fix y)))
       (equal (ctimes x y) (ctimes (fix x) (fix y)))
       (equal (clessp x y) (clessp (fix x) (fix y)))
       (equal (fix x) (if (acl2-numberp x) x 0)))
  :rule-classes nil
  :hints (("Subgoal 1" :in-theory (enable fix))))

; + Associativity, Commutativity, and Zero
; (equal (+ (+ x y) z) (+ x (+ y z)))
; (equal (+ x y) (+ y x))
; (equal (+ 0 y) (fix y))

(defthm cplus-associativity-etc
  (and (equal (cplus (cplus x y) z) (cplus x (cplus y z)))
       (equal (cplus x y) (cplus y x))
       (equal (cplus 0 y) (fix y))))

; * Distributes Over +
; (equal (+ (* c x) (* d x)) (* (+ c d) x))

(defthm ctimes-distributivity
  (equal (cplus (ctimes c x) (ctimes d x)) (ctimes (cplus c d) x)))

; * Associativity, Commutativity, Zero and One
; (equal (* (* x y) z) (* x (* y z)))   ; See note below 
; (equal (* x y) (* y x))
; (equal (* 0 x) 0)
; (equal (* 1 x) (fix x))

(defthm ctimes-associativity-etc
  (and (equal (ctimes (ctimes x y) z) (ctimes x (ctimes y z)))
       (equal (ctimes x y) (ctimes y x))
       (equal (ctimes 0 y) 0)
       (equal (ctimes 1 x) (fix x))))

; + Inverse
; (equal (+ x (* -1 x)) 0)

(defthm cplus-inverse
  (equal (cplus x (ctimes -1 x)) 0))

; Reflexivity of <=
; (<= x x)

(defthm clesseqp-reflexivity
  (clesseqp x x))

; Antisymmetry
; (implies (< x y) (not (< y x)))   ; (implies (< x y) (<= x y))

(defthm clessp-antisymmetry
  (implies (clessp x y)
           (not (clessp y x))))

; Trichotomy
; (implies (and (acl2-numberp x)
;               (acl2-numberp y))
;          (or (< x y)
;              (< y x)
;              (equal x y)))

(defthm clessp-trichotomy
  (implies (and (acl2-numberp x)
                (acl2-numberp y))
           (or (clessp x y)
               (clessp y x)
               (equal x y)))
  :rule-classes nil)

; Additive Properties of < and <=
; (implies (and (<  x y) (<= u v)) (<  (+ x u) (+ y v)))
; (implies (and (<= x y) (<= u v)) (<= (+ x u) (+ y v)))

; We have to prove three lemmas first.  But then we nail these suckers!

 (defthm not-lessp-plus-instance-u=v
   (implies (and (rationalp x)
                 (rationalp y)
                 (rationalp u)
                 (not (lessp y x)))
            (not (lessp (plus y u) (plus x u)))))

 (defthm lessp-plus-commuted1
   (implies (and (rationalp x)
                 (rationalp y)
                 (rationalp u)
                 (rationalp v)
                 (lessp x y)
                 (not (lessp v u)))
            (lessp (plus u x) (plus v y)))
   :hints (("goal" :use (:instance lessp-plus))))

 (defthm irreflexive-revisited-and-commuted
   (implies (and (rationalp x)
                 (rationalp y)
                 (lessp y x))
            (equal (equal x y) nil)))

(defthm clessp-additive-properties
  (and (implies (and (clessp x y)
                     (clesseqp u v))
                (clessp (cplus x u) (cplus y v)))
       (implies (and (clesseqp x y)
                     (clesseqp u v))
                (clesseqp (cplus x u) (cplus y v)))))

; The 1+ Trick
; (implies (and (integerp x)
;               (integerp y)
;               (< x y))
;          (<= (+ 1 x) y))

(defthm cplus-1-trick
  (implies (and (integerp x)
                (integerp y)
                (clessp x y))
           (clesseqp (cplus 1 x) y)))

; Cross-Multiplying Allows Cancellation
; (implies (and (< c1 0)
;               (< 0 c2))
;          (equal (+ (* c1 (abs c2)) (* c2 (abs c1))) 0))

; Three lemmas lead to the result.

 (defthm times--1--1 
   (equal (times -1 -1) 1)
   :hints
   (("goal"
     :use ((:instance plus-inverse-unique (x (times -1 -1)) (y 1))))))

 (defthm times--1-times--1
   (implies (rationalp x)
            (equal (times -1 (times -1 x)) x))
   :hints (("Goal"
            :use (:instance times-commutative-and-associative
                            (x -1)
                            (y -1)
                            (z x)))))
 (defthm reassocate-to-cancel-plus
   (implies (and (rationalp x)
                 (rationalp y))
            (equal (plus x (plus y (plus (times -1 x) (times -1 y))))
                   0))
   :hints
   (("Goal" :use ((:instance plus-commutative-and-associative
                             (x y)
                             (y (times -1 x))
                             (z (times -1 y)))))))

; Multiplication by Positive Preserves Inequality
;(implies (and (rationalp c)     ; see note below
;              (< 0 c))
;         (iff (< x y)
;              (< (* c x) (* c y))))

(defthm multiplication-by-positive-preserves-inequality
  (implies (and (rationalp c)
                (clessp 0 c))
           (iff (clessp x y)
                (clessp (ctimes c x) (ctimes c y)))))

; The Zero Trichotomy Trick
; (implies (and (acl2-numberp x)
;               (not (equal x 0))
;               (not (equal x y)))
;          (or (< x y) (< y x)))

 (defthm complex-equal-0
   (implies (and (rationalp x)
                 (rationalp y))
            (equal (equal (complex x y) 0)
                   (and (equal x 0)
                        (equal y 0)))))

(defthm zero-trichotomy-trick
 (implies (and (acl2-numberp x)
               (not (equal x 0))
               (not (equal x y)))
          (or (clessp x y) (clessp y x)))
 :rule-classes nil :hints (("goal" :in-theory (enable fix))))


; The Find Equational Poly Trick
; (implies (and (<= x y) (<= y x)) (equal (fix x) (fix y)))

(defthm find-equational-poly-trick
  (implies (and (clesseqp x y)
                (clesseqp y x))

           (equal (fix x) (fix y)))
  :hints (("Goal" :in-theory (enable fix))))

)

|#
;-----------------------------------------------------------------------------
; Thus ends the ALSLA.  However, there are, no doubt, a few more that we
; will discover when we implement proof objects!

; Note that in Multiplication by Positive Preserves Inequality we require the
; positive to be rational.  Multiplication by a "positive" complex rational
; does not preserve the inequality.  For example, the following evaluates
; to nil:
; (let ((c #c(1 -10))
;       (x #c(1 1))
;       (y #c(2 -2)))
;  (implies (and ; (rationalp c)          ; omit the rationalp hyp
;                  (< 0 c))
;           (iff (< x y)                  ; t
;                (< (* c x) (* c y)))))   ; nil

; Thus, the coefficients in our polys must be rational.

; End of Essay on the Logical Basis for Linear Arithmetic.

(deflabel linear-arithmetic
  :doc
  ":Doc-Section Miscellaneous

  A description of the linear arithmetic decision procedure~/~/

  We describe the procedure very roughly here.
  Fundamental to the procedure is the notion of a linear polynomial
  inequality.  A ``linear polynomial'' is a sum of terms, each of
  which is the product of a rational constant and an ``unknown.''  The
  ``unknown'' is permitted to be ~c[1] simply to allow a term in the sum
  to be constant.  Thus, an example linear polynomial is
  ~c[3*x + 7*a + 2]; here ~c[x] and ~c[a] are the (interesting) unknowns.
  However, the unknowns need not be variable symbols.  For
  example, ~c[(length x)] might be used as an unknown in a linear
  polynomial.  Thus, another linear polynomial is ~c[3*(length x) + 7*a].
  A ``linear polynomial inequality'' is an inequality 
  (either ~ilc[<] or ~ilc[<=])
  relation between two linear polynomials.  Note that an equality may
  be considered as a pair of inequalities; e.q., ~c[3*x + 7*a + 2 = 0]
  is the same as the conjunction of ~c[3*x + 7*a + 2 <= 0] and
  ~c[0 <= 3*x + 7*a + 2].

  Certain linear polynomial
  inequalities can be combined by cross-multiplication and addition to
  permit the deduction of a third inequality with
  fewer unknowns.  If this deduced inequality is manifestly false, a
  contradiction has been deduced from the assumed inequalities.

  For example, suppose we have two assumptions
  ~bv[]
  p1:       3*x + 7*a <  4 
  p2:               3 <  2*x
  ~ev[]
  and we wish to prove that, given ~c[p1] and ~c[p2], ~c[a < 0].  As
  suggested above, we proceed by assuming the negation of our goal
  ~bv[]
  p3:               0 <= a.
  ~ev[]
  and looking for a contradiction.

  By cross-multiplying and adding the first two inequalities, (that is,
  multiplying ~c[p1] by ~c[2], ~c[p2] by ~c[3] and adding the respective
  sides), we deduce the intermediate result
  ~bv[]
  p4:  6*x + 14*a + 9 < 8 + 6*x
  ~ev[]
  which, after cancellation, is:
  ~bv[]
  p4:        14*a + 1 <  0.
  ~ev[]
  If we then cross-multiply and add ~c[p3] to ~c[p4], we get
  ~bv[]
  p5:               1 <= 0,
  ~ev[]
  a contradiction.  Thus, we have proved that ~c[p1] and ~c[p2] imply the
  negation of ~c[p3].

  All of the unknowns of an inequality must be eliminated by
  cancellation in order to produce a constant inequality.  We can
  choose to eliminate the unknowns in any order, but we eliminate them in
  term-order, largest unknowns first.  (~l[term-order].)  That is, two
  polys are cancelled against each other only when they have the same
  largest unknown.  For instance, in the above example we see that ~c[x]
  is the largest unknown in each of ~c[p1] and ~c[p2], and ~c[a] in
  ~c[p3] and ~c[p4].

  Now suppose that this procedure does not produce a contradiction but
  instead yields a set of nontrivial inequalities.  A contradiction
  might still be deduced if we could add to the set some additional
  inequalities allowing further cancellations.  That is where
  ~c[:linear] lemmas come in.  When the set of inequalities has stabilized
  under cross-multiplication and addition and no contradiction is
  produced, we search the data base of ~c[:]~ilc[linear] rules for rules about
  the unknowns that are candidates for cancellation (i.e., are the
  largest unknowns in their respective inequalities).  ~l[linear]
  for a description of how ~c[:]~ilc[linear] rules are used.

  See also ~ilc[non-linear-arithmetic] for a description of an extension
  to the linear-arithmetic procedure described here.")

;=================================================================

; Arith-term-order

; As of Version_2.6, we now use a different term-order when ordering
; the alist of a poly.  Arith-term-order is almost the same as
; term-order (which was used previously) except that 'UNARY-/ is
; `invisible' when it is directly inside a 'BINARY-*.  The motivation
; for this change lies in an observation that, when reasoning about
; floor and mod, terms such as (< (/ x y) (floor x y)) are common.
; However, when represented within the linear-pot-lst, (BINARY-* X
; (UNARY-/ Y)) was a heavier term than (FLOOR X Y) and so the linear
; rule (<= (floor x y) (/ x y)) never got a chance to fire.  Now,
; (FLOOR X Y) is the heavier term.

; Note that this function is something of a hack in that it works
; because "F" is later in the alphabet than "B".  It might be better
; to allow the user to specify an order; but, if the linear rules
; present in the books distributed with ACL2 are representative this
; is sufficient.  Perhaps this should be reconsidered later.

;; RAG - I thought about adding lines here for real numbers, but since we
;; cannot construct actual real constants, I don't think this is
;; needed here.  Besides, I'm not sure what the right value would be
;; for a real number!

(defun fn-count-evg-rec (evg acc)

; See the comment in var-fn-count for an explanation of how this function
; counts the size of evgs.

  (cond ((atom evg)
         (cond ((rationalp evg)
                (cond ((integerp evg)
                       (cond ((< evg 0)
                              (+ 2 (- evg) acc))
                             (t  (+ 1 evg acc))))
                      (t
                       (fn-count-evg-rec (numerator evg)
                                         (fn-count-evg-rec (denominator evg)
                                                           (1+ acc))))))

               #+:non-standard-analysis
               ((realp evg) (er hard 'fn-count-evg 
                                "Encountered an irrational in fn-count-evg!"))

               ((complex-rationalp evg)
                (fn-count-evg-rec (realpart evg)
                                  (fn-count-evg-rec (imagpart evg)
                                                    (1+ acc))))

               #+:non-standard-analysis
               ((complexp evg) (er hard 'fn-count-evg 
                                   "Encountered a complex irrational in fn-count-evg!"))

               ((symbolp evg)
                (+ 2 (* 2 (length (symbol-name evg))) acc))
               ((stringp evg)
                (+ 1 (* 2 (length evg)) acc))
               (t ; (characterp evg)
                (1+ acc))))
        (t (fn-count-evg-rec (cdr evg)
                             (fn-count-evg-rec (car evg)
                                               (1+ acc))))))

(defmacro fn-count-evg (evg)
  `(fn-count-evg-rec ,evg 0))

(mutual-recursion

(defun arith-fn-var-count (term times-flag)
  (declare (xargs :guard (pseudo-termp term)))
  (cond ((variablep term)
         (mv 0 1))
        ((fquotep term)
         (mv 0 0))
        (t (mv-let (f v)
             (arith-fn-var-count-lst (fargs term)
                                     (eq (ffn-symb term) 'BINARY-*))
             (mv (if (and times-flag
                          (eq (ffn-symb term)
                              'UNARY-/))
                     f
                   (+ 1 f))
                 v)))))

(defun arith-fn-var-count-lst (lst times-flag)
  (declare (xargs :guard (pseudo-term-listp lst)))
  (cond ((null lst)
         (mv 0 0))
        (t (mv-let (f1 v1)
             (arith-fn-var-count (car lst) times-flag)
             (mv-let (f2 v2)
               (arith-fn-var-count-lst (cdr lst) times-flag)
               (mv (+ f1 f2) (+ v1 v2)))))))

)

(defun arith-term-order (term1 term2)
  (mv-let (fn-count1 var-count1)
    (arith-fn-var-count term1 nil)
    (mv-let (fn-count2 var-count2)
      (arith-fn-var-count term2 nil)
      (cond ((< var-count1 var-count2) t)
            ((> var-count1 var-count2) nil)
            ((< fn-count1 fn-count2) t)
            ((> fn-count1 fn-count2) nil)
            (t (lexorder term1 term2))))))


;=================================================================


; Polys

; Historical note: Polys are now 
; (<  0 (+ constant (* k1 t1) ... (* kn tn)))
; rather than
; (<  (+ constant (* k1 t1) ... (* kn tn)) 0)
; as in Version_2.6 and before.

(defrec poly 
    (((alist parents . ttree)
      .
      (constant relation rational-poly-p . derived-from-not-equalityp)))
    t)

; A poly represents an implication hyps -> concl, where hyps is the
; conjunction of the terms in the 'assumptions of the ttree and concl is

; (<  0 (+ constant (* k1 t1) ... (* kn tn))), if relation = '<
; (<= 0 (+ constant (* k1 t1) ... (* kn tn))), otherwise.

; Constant is an ACL2 numberp, possibly complex-rationalp but usually
; rationalp.  Alist is an alist of pairs of the form (ti . ki) where ti is a
; term and ki is a rationalp.  The alist is kept ordered by arith-term-order
; on the ti.  The largest ti is at the front.  Relation is either '< or '<=.

; The ttree in a poly is a tag tree.
; There are three tags we use here:  lemma, assumption, and pt.
; The lemma tag indicates a lemma name used to produce the poly.
; The assumption tag indicates a term assumed true to produce the poly.
; For example, an assumption might be (rationalp (foo a b)).
; The pt tag indicates literals of current-clause used in the production
; of the poly.

; The parents field is a list of parents and is set-eql to the union
; over all 'pt tags in ttree of the tips of the pts.  It is used in
; the code that ignores polynomials descended from the current
; literal.  (This used to be done by to-be-ignoredp, which used to
; take up to 80% of the time spent by add-poly.)  See collect-parents
; and marry-parents for how we establish and maintain this
; relationship, and ignore-polyp for its use.

; Rational-poly-p is a booolean flag used in non-linear arithmetic.  When it
; is true, then the right-hand side of the inequality (the polynomial) is
; rational.  The flag is needed because of the presence of complex numbers in
; ACL2's logic.  Note that sums and products of rational polys are rational.
; When rational-poly-p is true we know that the product of two positive polys
; is also positive.

; Derived-from-not-equalityp keeps track of whether the poly in
; question was derived directly from a top-level negated equality.
; This field is new to v2_8 --- previously its value was calculated
; as needed.  In the rest of this comment, we address two issues ---
; (1) What derived-from-not-equalityp is used for.
; (2) Differences with earlier behavior.

; (1) What derived-from-not-equalityp is used for: In
; process-equational-polys, we scan through the
; simplify-clause-pot-lst and look for complementary pairs of
; inequalities from which we can derive an equality.  Example: from
; (<= x y) and (<= y x) we can derive (equal x y).  However, the two
; inequalities could have themselves been derived from the very
; equality we are about to generate, and this could lead to looping.
; Thus, we tag those inequalities which stem directly from the
; linearization of a (negated) equality with
; :derived-from-not-equalityp = t.  This field is then examined in
; process-equational-polys (or rather its sub-functions), and the
; result is used to prune the list of candidate inequalities.

; (2) Differences with earlier behavior:
; Previously, the function descends-from-not-equalityp played the role
; of the new field :derived-from-not-equalityp.  This function was
; much more conservative in its judgement and threw out any poly which
; descended from an inequality in any way, rather than only those
; which were derived directly from a (negated) equality.  Matt
; Kaufmann noticed difference and provoked an email exchange with
; Robert Krug, who did the research and initial coding leading to this
; version of linear).  Here is Robert's reply.

#|
Matt is right, I did inadvertantly change ACL2's meaning for
descends-from-not-equalityp.  Perhaps this change is also responsible
for some of the patches required for the regression suite.  However,
this change was inadvertant only because I did not properly understand
the old behaviour which seems odd to me.  I believe that the new
behaviour is the ``correct'' one.  Let us look at an example:

Input:

x = y       (1)
a + y >= b  (2)
a + x <= b  (3)

After cancellation:

y: x <= y      (1a)
   b <= y + a  (2)

   y <= x      (1b)

x: x + a <= b  (3)

   b <= x + a  (4) = (1b + 2)

I think that some form of x + a = b should be generated and added to
the clause.  Under the new order, (3) and (4) would be allowed to
combine, because neither of them descended \emph{directly} from an
inequality.  This seems like the kind of fact that I, as a user, would
expect ACL2 to know and use.  Under the old regime however, since (1b) 
was used in the derivation of (4), this was not allowed.

This raises the qestion of whether the new test is too liberal.  For
example, from

input:
x = y
a + x = b + y

We would now generate the equality a = b.  I do not see any harm in
this.  Perhaps another example will convince me that we need to
tighten the heuristic up.
|#

; Note: In Nqthm, we thought of polynomials being inequalities in a different
; logic, or at least, in an extension of the Nqthm logic that included the
; rationals.  In ACL2, we think of a poly as simply being an alternative
; represention of a term, in which we have normalized by the use of certain
; algebraic laws governing the ACL2 function symbols <, <=, +, and *.  We
; noted these above (see ALSLA).  In addition, we think of the operations
; performed upon polys being just ordinary inferences within the logic,
; justified by still other algebraic laws, such as that allowing the addition
; of inequalities.  The basic idea behind the linear arithmetic procedure is
; to convert the (arithmetic) assumptions in a problem (including the
; negation of the conclusion) to their normal forms, make a bunch of ordinary
; forward-chaining-like inferences from those assumptions guided by certain
; principles, and if a contradiction is found, deduce that the original
; assumptions imply the original conclusion.  The point is that linear
; arithmetic is not some model-theoretic step appealing to the correspondence
; of theorems in two different theories but rather an entirely
; proof-theoretic step.

(defabbrev first-var (p) (caar (access poly p :alist)))

(defabbrev first-coefficient (p) (cdar (access poly p :alist)))

; We expect polys to meet the following invariant implied in the discussion
; above:
; 1. The leading coefficient is +/-1
; 2. The leading unknown:
;    a. Is not a quoted constant --- Not much of an unknown/variable
;    b. Is not itself a sum --- A poly represents a sum of terms
;    c. Is not of the form (* c x), where c is a rational constant ---
;       The c should have been ``pulled out''.
;    d. Is not of the form (- c), (* c d), or (+ c d) where c and d are 
;       rational constants --- These terms should be evaluated and added 
;       onto the constant, not used as an unknown.
;    Some of these are implied by others, but we check them each
;    independently.

; The following three functions (weakly) capture this notion.

; Note: These invariants are referred to elsewhere by number, e.g.,
; ``2.a'' If you change the above, search for occurrences of
; ``good-polyp''.  If you refer to these invariants, be sure to
; include the string ``good-polyp'' somewhere nearby.

(defun good-coefficient (c)
  (equal (abs c) 1))

(defun good-pot-varp (x)
  (and (not (quotep x))
       (not (equal (fn-symb x) 'BINARY-+))
       (not (and (equal (fn-symb x) 'BINARY-*)
                 (quotep (fargn x 1))
                 (real/rationalp (unquote (fargn x 1)))))
       (not (and (equal (fn-symb x) 'UNARY--)
                 (quotep (fargn x 1))
                 (real/rationalp (unquote (fargn x 1)))))))

(defun good-polyp (p)
  (and (good-coefficient (first-coefficient p))
       (good-pot-varp (first-var p))))

; We need to define executable versions of the logical functions for <, <=,
; and abs.  We know, however, that we will only apply them to acl2-numberps
; so we do not need to consider fixing the arguments.

;; RAG - I changed rational to real in the test to use < as the comparator.

(defun logical-< (x y)
  (declare (xargs :guard (and (acl2-numberp x) (acl2-numberp y))))
  (cond ((and (real/rationalp x)
              (real/rationalp y))
         (< x y))
        ((< (realpart x) (realpart y))
         t)
        (t (and (= (realpart x) (realpart y))
                (< (imagpart x) (imagpart y))))))

;; RAG - Another change of rational to real in the test to use <= as the
;; comparator.

(defun logical-<= (x y)
  (declare (xargs :guard (and (acl2-numberp x) (acl2-numberp y))))
  (cond ((and (real/rationalp x)
              (real/rationalp y))
         (<= x y))
        ((< (realpart x) (realpart y))
         t)
        (t (and (= (realpart x) (realpart y))
                (<= (imagpart x) (imagpart y))))))

(defun evaluate-ground-poly (p)

; We assume the :alist of poly p is nil and thus p is a ground poly.
; We compute its truth value.

  (if (eq (access poly p :relation) '<)
      (logical-< 0 (access poly p :constant))
      (logical-<= 0 (access poly p :constant))))

(defun impossible-polyp (p)
  (and (null (access poly p :alist))
       (eq (evaluate-ground-poly p) nil)))

(defun true-polyp (p)
  (and (null (access poly p :alist))
       (evaluate-ground-poly p)))

(defun silly-polyp (poly)

; For want of a better name, we say a poly is "silly" if it contains
; the *nil* assumption among its 'assumptions.

  (tag-tree-occur-assumption-nil (access poly poly :ttree)))

(defun impossible-poly (ttree)
  (make poly
        :alist nil
        :parents (collect-parents ttree)
        :rational-poly-p t
        :derived-from-not-equalityp nil
        :ttree ttree
        :constant -1
        :relation '<))

(defun base-poly0 (ttree parents relation rational-poly-p derived-from-not-equalityp)

; Warning: Keep this in sync with base-poly.

  (make poly
        :alist nil
        :parents parents
        :rational-poly-p rational-poly-p
        :derived-from-not-equalityp derived-from-not-equalityp
        :ttree ttree
        :constant 0
        :relation relation))

(defun base-poly (ttree relation rational-poly-p derived-from-not-equalityp)

; Warning: Keep this in sync with base-poly0.

  (make poly
        :alist nil
        :parents (collect-parents ttree)
        :rational-poly-p rational-poly-p
        :derived-from-not-equalityp derived-from-not-equalityp
        :ttree ttree
        :constant 0
        :relation relation))

(defun poly-alist-equal (alist1 alist2)

; This function is essentially EQUAL for two alists, but is faster
; (at least with poly alists).

  (cond ((null alist1)
         (null alist2))
        ((null alist2)
         nil)
        (t
         (and (eql (cdar alist1) (cdar alist2))
              (equal (caar alist1) (caar alist2))
              (poly-alist-equal (cdr alist1) (cdr alist2))))))

(defun poly-equal (poly1 poly2)

; This function is essentially EQUAL for two polys, but is faster.

  (and (eql (access poly poly1 :constant)
            (access poly poly2 :constant))
       (eql (access poly poly1 :relation)
            (access poly poly2 :relation))
       (poly-alist-equal (access poly poly1 :alist)
                         (access poly poly2 :alist))))

(defun poly-weakerp (poly1 poly2)

; We return t if poly1 is ``weaker'' than poly2. 

; Pseudo-examples:
; (<= 3 (* x y)) is weaker than both (< 3 (* x y)) and (<= 17/5 (* x y));
; but is not weaker than (< 17 (+ w (* x y))), (< 17 (* 5 x y)),
; or (< 17 (* y x)).

  (and (or (logical-< (access poly poly2 :constant)
                      (access poly poly1 :constant))

; The above inequality test always confuses me.  In the comments,
; it is said that (<= 3 (* x y)) is weaker than (<= 17/5 (* x y)).
; Recall that the polys are stored in a format suggested by:
; (<  (+ constant (* k1 t1) ... (* kn tn)) 0).  Thus, the two constants
; would be stored as a -3 and a -17/5, and the above test is correct.
; -17/5 < -3.       

           (and (eql (access poly poly1 :constant)
                     (access poly poly2 :constant))
                (or (eq (access poly poly1 :relation) '<=)
                    (eq (access poly poly2 :relation) '<))))
       (poly-alist-equal (access poly poly1 :alist)
                         (access poly poly2 :alist))))

(defun poly-member (p lst)

; P is a poly and lst is a list of polys.  This function used to return t if p
; was in lst (ignoring tag trees).  Now, it returns t if p is weaker than
; some poly in lst.

; This change was motivated by an observation that after several linear rules
; have fired and a couple of rounds of cancellation have occurred, one will
; occasionally see the linear pot fill up with weak polys.  In most cases
; this idea makes no real performance difference; but Robert Krug has seen
; examples where it makes a tremendous difference.

  (and (consp lst)
       (or (poly-weakerp p (car lst))
           (poly-member p (cdr lst)))))

(defun new-and-ugly-linear-varsp (lst flag term)

; Lst is a list of polys, term is the linear var which triggered the
; addition of the polys in lst, and flag is a boolean indicating
; whether we have maxed out the the loop-stopper-value associated
; with term.  If flag is true, we check whether any of the polys are
; arith-term-order worse than term.

; Historical Note: Once upon a time, in Version_2.5 and earlier, this
; function actually insured that term wasn't in lst, i.e., that term was
; "new".  But in Version_2.6, we changed the meaning of the function without
; changing its name.  The word "new" in the name is now a mere artifact.

; This is intended to catch certain loops that can arise from linear
; lemmas.  See the "Mini-essay on looping and linear arithmetic" below.


  (cond ((not flag)
         nil)
        ((null lst) 
         nil)
        ((arith-term-order term
                           (first-var (car lst)))
         t)
        (t (new-and-ugly-linear-varsp (cdr lst) flag term))))

(defun filter-polys (lst ans)

; We scan the list of polys lst.  If we find an impossible one, we
; return it as our first result.  If we find a true one we skip it.
; If we find a poly that is ``weaker'' (see poly-member and poly-weakerp)
; than one of those already filtered, we skip it.
; Otherwise we just accumulate them into ans.  We return two values:
; the standard indication of contradiction and, otherwise in the
; second, the filtered list.  This list in the reverse order from that
; produced by nqthm.

  (cond ((null lst) 
         (mv nil ans))
        ((impossible-polyp (car lst))
         (mv (car lst) nil))
        ((true-polyp (car lst))
         (filter-polys (cdr lst) ans))
        ((poly-member (car lst) ans)
         (filter-polys (cdr lst) ans))
        (t 
         (filter-polys (cdr lst) (cons (car lst) ans)))))


;=================================================================

; Here we define some functions for constructing polys.

(defun add-linear-variable1 (n var alist)

; N is a rational constant and var is an arbitrary term -- a linear "variable".
; Alist is a polynomial alist and we are to add the new pair (var . n) to it.
; We keep the alist sorted on term-order on the terms with the largest var
; first.  Furthermore, if there is already an entry for var we merely add n to
; it.  If the resulting coefficient is 0 we delete the pair.

; We assume n is not 0 to begin with.

  (cond ((null alist)
         (cons (cons var n) nil))
        ((arith-term-order var (caar alist))
         (cond ((equal var (caar alist))
                (let ((k (+ (cdar alist)
                            n)))
                  (cond ((= k 0) (cdr alist))
                        (t (cons (cons var k) (cdr alist))))))
               (t (cons (car alist)
                        (add-linear-variable1 n var
                                              (cdr alist))))))
        (t (cons (cons var n)
                 alist))))

(defun zero-factor-p (term)

; The following code recognizes terms of the form (* a1 ... 0 ... ak)
; so that we can treat them as though they were 0.  Two sources of these
; 0-factor terms are: the original clause for which we are
; constructing a pot-lst, and a term introduced by forward chaining,
; which doesn't use rewrite.  (The latter might commonly occur via an
; fc rule like (implies (and (< 0 x) (< y y+)) (< (* x y) (* x y+)))
; triggered by (* x y+).  The free var y might be chosen to be 0, as
; would happen if (< 0 y+) were available.  The result would be the
; term (* 0 y).)

  (cond ((variablep term) nil)
        ((fquotep term)
         (equal term *0*))
        ((eq (ffn-symb term) 'BINARY-*)
         (or (zero-factor-p (fargn term 1))
             (zero-factor-p (fargn term 2))))
        (t
         nil)))

(defun get-coefficient (term acc)

; We are about to add term onto a poly.  We want to enforce the
; poly invariant 2.c. (Described shortly before the definition of
; good-polyp.)  We therefore accumulate onto acc any leading constant
; coefficients.  We return the (possibly) stripped term and its
; coefficient.

  (if (and (eq (fn-symb term) 'BINARY-*)
           (quotep (fargn term 1))
           (real/rationalp (unquote (fargn term 1))))
      (get-coefficient (fargn term 2) (* (unquote (fargn term 1)) acc))
    (mv acc term)))

(defun add-linear-variable (term side p)
  (mv-let (n term)
    (cond ((zero-factor-p term)
           (mv 0 nil))
          ((and (eq (fn-symb term) 'BINARY-*)
                (quotep (fargn term 1))
                (real/rationalp (unquote (fargn term 1))))
           (mv-let (coeff new-term)
             (get-coefficient term 1)
             (if (eq side 'lhs)
                 (mv (- coeff) new-term)
               (mv coeff new-term))))
          ((eq side 'lhs)
           (mv -1 term))
          (t
           (mv 1 term)))
    (if (= n 0)
        p
      (change poly p
              :alist
              (add-linear-variable1 n term (access poly p :alist))))))

(defun dumb-eval-yields-quotep (term)

; We are about to add term onto a poly.  We want to enforce the poly invariant
; 2.d. (Described shortly before the definition of good-polyp.)   Here, we
; check whether we should evaluate term.  If so, we do the evaluation in 
; dumb-eval immediately below.

  (cond ((variablep term)
         nil)
        ((fquotep term)
         t)
        ((equal (ffn-symb term) 'BINARY-*)
         (and (dumb-eval-yields-quotep (fargn term 1))
              (dumb-eval-yields-quotep (fargn term 2))))
        ((equal (ffn-symb term) 'BINARY-+)
         (and (dumb-eval-yields-quotep (fargn term 1))
              (dumb-eval-yields-quotep (fargn term 2))))
        ((equal (ffn-symb term) 'UNARY--)
         (dumb-eval-yields-quotep (fargn term 1)))
        (t
         nil)))

(defun dumb-eval (term)

; See dumb-eval-yields-quotep, above.  This function evaluates (fix
; ,term) and produces the corresponding evg, not a term.  Thus,
; (binary-+ '1 '2) dumb-evals to 3 not '3, and (quote abc) dumb-evals
; to 0.

  (cond ((variablep term)
         (er hard 'dumb-eval
             "Bad term. We were expecting a constant, but encountered
              the variable ~x."
             term))
        ((fquotep term)
         (if (acl2-numberp (unquote term))
             (unquote term)
           0))
        ((equal (ffn-symb term) 'BINARY-*)
         (* (dumb-eval (fargn term 1))
            (dumb-eval (fargn term 2))))
        ((equal (ffn-symb term) 'BINARY-+)
         (+ (dumb-eval (fargn term 1))
            (dumb-eval (fargn term 2))))
        ((equal (ffn-symb term) 'UNARY--)
         (- (dumb-eval (fargn term 1))))
        (t
         (er hard 'dumb-eval
             "Bad term. The term ~x was not as expected by dumb-eval."
             term))))

(defun add-linear-term (term side p)

; Side is either 'rhs or 'lhs.  This function adds term to the
; indicated side of the poly p.  It is the main way we construct a
; poly.  See linearize.

  (cond
   ((variablep term)
    (add-linear-variable term side p))

; We enforce poly invariant 2.d.   (Described shortly before the 
; definition of good-polyp.)

   ((dumb-eval-yields-quotep term)
    (let ((temp (dumb-eval term)))
      (if (eq side 'lhs)
          (change poly p
                  :constant
                  (+ (access poly p :constant) (- temp)))
        (change poly p
                :constant
                (+ (access poly p :constant) temp)))))

   (t
    (let ((fn1 (ffn-symb term)))
      (case fn1
            (binary-+
             (add-linear-term (fargn term 1) side
                              (add-linear-term (fargn term 2) side p)))
            (unary--
             (add-linear-term (fargn term 1) 
                              (if (eq side 'lhs) 'rhs 'lhs)
                              p))
            (binary-*

; We enforce the poly invariants 2.b. and 2.c.  (Described shortly
; before the definition of good-polyp.)

             (cond
              ((and (quotep (fargn term 1))
                    (real/rationalp (unquote (fargn term 1)))
                    (equal (fn-symb (fargn term 2)) 'BINARY-+))
               (add-linear-term
                (mcons-term* 'BINARY-+
                             (mcons-term* 'BINARY-*
                                          (fargn term 1)
                                          (fargn (fargn term 2) 1))
                             (mcons-term* 'BINARY-*
                                          (fargn term 1)
                                          (fargn (fargn term 2) 2)))
                side
                p))
              ((and (quotep (fargn term 1))
                    (real/rationalp (unquote (fargn term 1)))
                    (equal (fn-symb (fargn term 2)) 'BINARY-*)
                    (quotep (fargn (fargn term 2) 1))
                    (real/rationalp (unquote (fargn (fargn term 2) 1))))
               (add-linear-term
                (mcons-term* 'BINARY-*
                             (kwote (* (unquote (fargn term 1))
                                       (unquote (fargn (fargn term 2) 1))))
                             (fargn (fargn term 2) 2))
                side
                p))
              (t
               (add-linear-variable term side p))))

            (otherwise
             (add-linear-variable term side p)))))))

(defun add-linear-terms-fn (rst)
  (cond ((null (cdr rst))
         (car rst))
        ((eq (car rst) :lhs)
         `(add-linear-term ,(cadr rst) 'lhs
                           ,(add-linear-terms-fn (cddr rst))))
        ((eq (car rst) :rhs)
         `(add-linear-term ,(cadr rst) 'rhs
                           ,(add-linear-terms-fn (cddr rst))))
        (t
         (er hard 'add-linear-terms-fn
             "Bad term ~x0"
             rst))))

(defmacro add-linear-terms (&rest rst)

; There are a couple of spots where we wish to add several pieces at
; a time to a poly.  This macro and its associated function enable us
; to circumvent ACL2's requirement that all functions take a fixed
; number of arguments.

; Example usage:
; (add-linear-terms :lhs term1
;                   :lhs ''1
;                   :rhs term2
;                   (base-poly ts-ttree
;                             '<=
;                             t
;                             nil))

  (add-linear-terms-fn rst))

(defun normalize-poly1 (coeff alist)
  (cond ((null alist)
         nil)
        (t
         (acons (caar alist) (/ (cdar alist) coeff)
                (normalize-poly1 coeff (cdr alist))))))

(defun normalize-poly (p)

; P is a poly.  We normalize it, so that the leading coefficient
; is +/-1.

  (if (access poly p :alist)
      (let ((c (abs (first-coefficient p))))
        (cond 
         ((eql c 1)
          p)
         (t
          (change poly p
                  :alist (normalize-poly1 c (access poly p :alist))
                  :constant (/ (access poly p :constant) c)))))
    p))

(defun normalize-poly-lst (poly-lst)
  (cond ((null poly-lst)
         nil)
        (t
         (cons (normalize-poly (car poly-lst))
               (normalize-poly-lst (cdr poly-lst))))))


;=================================================================


; Linear Pots

(defrec linear-pot ((loop-stopper-value . negatives) . (var . positives)) t)

; Var is a "linear variable", i.e., any term.  Positives and negatives are
; lists of polys with the properties that var is the first (heaviest) linear
; variable in each poly in each list and var occurs positively in the one and
; negatively in the other.  Loop-stopper-value is a natural number counter that
; is used to avoid looping, starting at 0 and incremented, using
; *max-linear-pot-loop-stopper-value* as a bound.

(defun modify-linear-pot (pot pos neg)

; We do the equivalent of:

; (change linear-pot pot :positives pos :negatives neg)

; except that we avoid unnecessary consing.

  (if (equal neg (access linear-pot pot :negatives))
      (if (equal pos (access linear-pot pot :positives))
          pot
        (change linear-pot pot :positives pos))
    (if (equal pos (access linear-pot pot :positives))
        (change linear-pot pot :negatives neg)
      (change linear-pot pot
              :positives pos
              :negatives neg))))

; Mini-essay on looping and linear arithmetic

; Robert Krug has written code to solve a problem with infinite loops related
; to linear arithmetic.  The following example produces the loop in ACL2
; Versions 2.4 and earlier.

#|
 (defaxiom *-strongly-monotonic
   (implies (and (< a b))
            (< (* a c) (* b c)))
   :rule-classes :linear)

 (defaxiom commutativity-2-of-*
   (equal (* x y z)
          (* y x z)))

 (defstub foo (x) t)

 (thm
  (implies (and (< a (* a c))
                (< 0 evil))
           (foo x)))
|#

; The defconst below stops the loop.  We may want to increase it in the
; future, but it appears to be sufficient for certifying ACL2 books in the
; current distribution.  It is used together with the field loop-stopper-value
; of the record linear-pot.  When a linear-pot is first created, its
; loop-stopper-value is 0 (see add-poly).  See add-linear-lemma for how
; loop-stopper-value is used to detect loops.

; Robert has provided the following trace, in which one can still see the first
; few iterations of the loop before it is caught by the loop-stopping mechanism
; now added.  He suggests tracing new-and-ugly-linear-varp and worse-than to
; get some idea as to why this loop was not caught before due to the presence
; of the inequality (< 0 evil).

#|
(trace (add-linear-lemma
        :entry (list (list 'term (nth 0 si::arglist))
                     (list 'lemma (access linear-lemma 
                                          (nth 1 si::arglist)
                                          :rune))
                     (list 'max-term (access linear-lemma 
                                             (nth 1 si::arglist)
                                             :max-term))
                     (list 'conclusion (access linear-lemma 
                                               (nth 1 si::arglist)
                                               :concl))
                     (list 'type-alist (show-type-alist 
                                        (nth 2 si::arglist))))
        :exit (if (equal (nth 9 si::arglist)
                         (mv-ref 1))
                  '(no change)
                  (list (list 'old-pot-list 
                              (show-pot-lst (nth 9 si::arglist)))
                        (list 'new-potlist 
                              (show-pot-lst (mv-ref 1)))))))
|#

(defconst *max-linear-pot-loop-stopper-value* 3)

(defun loop-stopper-value-of-var (var pot-lst)

; We return the value of loop-stopper-value associated with var in the
; pot-lst.  If var does not appear we return 0.

  (cond ((null pot-lst) 0)
        ((equal var (access linear-pot (car pot-lst) :var))
         (access linear-pot (car pot-lst) :loop-stopper-value))
        (t
         (loop-stopper-value-of-var var (cdr pot-lst)))))

(defun set-loop-stopper-values (new-vars new-pot-lst term value)

; New-vars is a list of new variables in new-pot-lst.  Term is the trigger-term
; which caused the new pots to be added, and value is the loop-stopper-value
; associated with it.  If a new-var is term-order greater than term, we set its
; loop-stopper-value to value + 1.  Otherwise, we set it to value.

; Note that new-vars is in the same order as the vars of new-pot-lst.

  (cond ((null new-vars) new-pot-lst)
        ((equal (car new-vars) (access linear-pot (car new-pot-lst) :var))
           (cond ((arith-term-order term (car new-vars))
                    (cons (change linear-pot (car new-pot-lst)
                                  :loop-stopper-value (1+ value))
                          (set-loop-stopper-values (cdr new-vars)
                                                   (cdr new-pot-lst)
                                                   term
                                                   value)))
                 (t
                    (cons (change linear-pot (car new-pot-lst)
                                  :loop-stopper-value value)
                          (set-loop-stopper-values (cdr new-vars)
                                                   (cdr new-pot-lst)
                                                   term
                                                   value)))))
        (t
           (cons (car new-pot-lst)
                 (set-loop-stopper-values new-vars
                                          (cdr new-pot-lst)
                                          term
                                          value)))))

(defun var-in-pot-lst-p (var pot-lst)

; Test whether var is the label of any of the pots in pot-lst.

  (cond ((null pot-lst) nil)
        ((equal var (access linear-pot (car pot-lst) :var))
         t)
        (t
         (var-in-pot-lst-p var (cdr pot-lst)))))

(defun bounds-polys-with-var1 (poly-lst pt)

; We cdr down poly-lst, looking for a bounds poly.  Poly-lst 
; is either the :positives or :negatives from a pot.  We know that
; the first bounds poly we find is, in fact, the strongest one present
; in poly-lst because we filter out any ones that are weaker than
; one already present with poly-member before adding it.

  (cond ((null poly-lst)
         nil)
        ((and (null (cdr (access poly (car poly-lst) :alist)))
              (rationalp (access poly (car poly-lst) :constant))
              (not (ignore-polyp (access poly (car poly-lst) :parents) pt)))
         (list (car poly-lst)))
        (t
         (bounds-polys-with-var1 (cdr poly-lst) pt))))

(defun bounds-polys-with-var (var pot-lst pt)

; A bounds poly is one in which the there is only one var in the
; alist.  Such a poly can be regarded as "bounding" said var.

; Pseudo-examples:
; 3 < x is a bounds poly.
; 3 < x + y is not.
; #(1,1) < x is not.

; We insist that the constant c be rational.

; We return a list of the strongest bounds polys in the pot labeled
; with var.  If there are no such polys, we return nil.

  (cond ((null pot-lst) nil)
        ((equal var (access linear-pot (car pot-lst) :var))
         (append (bounds-polys-with-var1
                  (access linear-pot (car pot-lst) :negatives) pt)
                 (bounds-polys-with-var1
                  (access linear-pot (car pot-lst) :positives) pt)))
        (t (bounds-polys-with-var var (cdr pot-lst) pt))))

(defun polys-with-var1 (var pot-lst)
  (cond ((null pot-lst) nil)
        ((equal var (access linear-pot (car pot-lst) :var))
         (append (access linear-pot (car pot-lst) :negatives)
                 (access linear-pot (car pot-lst) :positives)))
        (t (polys-with-var1 var (cdr pot-lst)))))

(defun polys-with-var (var pot-lst)

; We return a list of all the polys in the pot labeled with var.
; If there is no pot in pot-lst labeled with var, we return nil.
; We may occasionally be calling this function with an improper
; var.  We catch this early, rather than stepping through the whole
; pot (see add-inverse-polys and add-inverse-polys1).

  (if (eq (fn-symb var) 'BINARY-+)
      nil
    (polys-with-var1 var pot-lst)))

(defun new-vars-in-pot-lst (new-pot-lst old-pot-lst)

; We return all the new vars of new-pot-lst.  A "var" of a pot-lst is
; the :var component of a linear-pot in the pot-lst.  A var is
; considered "new" if it is not a variablep (i.e., is a function
; application) and the var is not a var of the old-pot-lst.

; New-pot-lst is an extension of old-pot-lst, obtained by successive
; calls of add-poly.  Every variable of old-pot-lst is in the new, but
; not vice versa.  Since both lists are ordered by the vars we can
; recur down both the new and the old pot lists simultaneously.

  (cond ((null new-pot-lst)
         nil)

; This function used to be wrong!  We incorrectly optimized the case
; for a pot with a variablep :var.  Consider an old-pot-lst with one
; pot, (foo x), and a new-pot-lst with two pots, x and (foo x).
; Previously, since (variablep (access linear-pot (car new-pot-lst)
; :var)) would be true, we would recur on the cdr of both pots and
; then determine that (foo x) was new.  I suspect that the variablep
; test was added to the function after the rest had been written.
; Here is the old code.  This bug was discovered by Robert Krug.

#|      ((and (not (variablep (access linear-pot (car new-pot-lst) :var)))
              (or all-new-flg
                  (null old-pot-lst)
                  (not (equal (access linear-pot (car new-pot-lst) :var)
                              (access linear-pot (car old-pot-lst) :var)))))
         (cons (access linear-pot (car new-pot-lst) :var)
               (new-vars-in-pot-lst (cdr new-pot-lst)
                                    old-pot-lst all-new-flg)))
|#

        ((or (null old-pot-lst)
             (not (equal (access linear-pot (car new-pot-lst) :var)
                         (access linear-pot (car old-pot-lst) :var))))
         (if (not (variablep (access linear-pot (car new-pot-lst) :var)))
             (cons (access linear-pot (car new-pot-lst) :var)
                   (new-vars-in-pot-lst (cdr new-pot-lst) old-pot-lst))
           (new-vars-in-pot-lst (cdr new-pot-lst) old-pot-lst)))
        (t (new-vars-in-pot-lst (cdr new-pot-lst)
                                (cdr old-pot-lst)))))

(defun changed-pot-vars (new-pot-lst old-pot-lst to-be-ignored-lst)

; New-pot-lst is an extension of old-pot-lst. To-be-ignored-lst is a
; list of pots which we are to ignore.  We return the list of pot
; labels (i.e., vars) of the pots which are changed with respect to
; old-pot-lst (a new pot is considered changed) which are not in
; to-be-ignored-lst.

  (cond ((null new-pot-lst)
         nil)
        ((equal (access linear-pot (car new-pot-lst) :var)
                (access linear-pot (car old-pot-lst) :var))
         (if (or (equal (car new-pot-lst)
                        (car old-pot-lst))
                 (member-equal (access linear-pot (car new-pot-lst) :var)
                               to-be-ignored-lst))
             (changed-pot-vars (cdr new-pot-lst) (cdr old-pot-lst) 
                               to-be-ignored-lst)
           (cons (access linear-pot (car new-pot-lst) :var)
                 (changed-pot-vars (cdr new-pot-lst) (cdr old-pot-lst) 
                                   to-be-ignored-lst))))
        (t
         (cons (access linear-pot (car new-pot-lst) :var)
               (changed-pot-vars (cdr new-pot-lst) old-pot-lst 
                                 to-be-ignored-lst)))))

(defun infect-polys (lst ttree parents)

; We extend the :ttree of every poly in lst with ttree.  We similarly
; expand :parents with parents.

  (cond ((null lst) nil)
        (t (cons (change poly (car lst)
                         :ttree
                         (cons-tag-trees ttree
                                         (access poly (car lst) :ttree))
                         :parents (marry-parents
                                   parents
                                   (access poly (car lst) :parents)))
                 (infect-polys (cdr lst) ttree parents)))))

(defun infect-first-n-polys (lst n ttree parents)

; We assume that parents is always (collect-parents ttree) when this is called.
; See infect-new-polys.

  (cond ((int= n 0) lst)
        (t (cons (change poly (car lst)
                         :ttree
                         (cons-tag-trees ttree
                                         (access poly (car lst) :ttree))
                         :parents (marry-parents
                                   parents
                                   (access poly (car lst) :parents)))
                 (infect-first-n-polys (cdr lst) (1- n) ttree parents)))))

(defun infect-new-polys (new-pot-lst old-pot-lst ttree)

; We must infect with ttree every poly in new-pot-lst that is not in
; old-pot-lst.  By "infect" we mean cons ttree onto the ttree of the
; poly.  However, we know that new-pot-lst is an extension of
; old-pot-lst via add-poly.  For every linear-pot in old-pot-lst there
; is a pot in the new pot-lst with the same var.  Furthermore, the
; linear pots are ordered so that by cdring down both new and old
; simultaneously when they have equal vars we keep them in step.
; Finally, every list of polys in new is an extension of its
; corresponding list in old.  I.e., the positives of some pot in new
; with the same var as a pot in old is an extension of the positives
; of that pot in old.  Hence, to visit every new poly in that list it
; suffices to visit just the first n, where n is the difference in the
; lengths of the new and old positives.

; See add-disjunct-polys-and-lemmas.

  (cond ((null new-pot-lst) nil)
        ((or (null old-pot-lst)
             (not (equal (access linear-pot (car new-pot-lst) :var)
                         (access linear-pot (car old-pot-lst) :var))))
         (let ((new-new-pot-lst
                (infect-new-polys (cdr new-pot-lst)
                                  old-pot-lst
                                  ttree)))
           (cons (modify-linear-pot
                  (car new-pot-lst)
                  (infect-polys (access linear-pot (car new-pot-lst) 
                                        :positives)
                                ttree
                                (collect-parents ttree))
                  (infect-polys (access linear-pot (car new-pot-lst) 
                                        :negatives)
                                ttree
                                (collect-parents ttree)))
                 new-new-pot-lst)))
        (t
         (let ((new-new-pot-lst
                (infect-new-polys (cdr new-pot-lst)
                                  (cdr old-pot-lst)
                                  ttree)))
           (cons (modify-linear-pot
                  (car new-pot-lst)
                  (infect-first-n-polys
                   (access linear-pot (car new-pot-lst) :positives)
                   (- (length (access linear-pot (car new-pot-lst)
                                      :positives))
                      (length (access linear-pot (car old-pot-lst)
                                      :positives)))
                   ttree
                   (collect-parents ttree))
                  (infect-first-n-polys
                   (access linear-pot (car new-pot-lst) :negatives)
                   (- (length (access linear-pot (car new-pot-lst)
                                      :negatives))
                      (length (access linear-pot (car old-pot-lst)
                                      :negatives)))
                   ttree
                   (collect-parents ttree)))
                 new-new-pot-lst)))))

;=================================================================


; Process-equational-polys

; Having set up the simplify-clause-pot-lst simplify clause we take
; advantage of it to find derived equalities that can help simplify
; the clause.  In this section we develop process-equational-polys.

(defun fcomplementary-multiplep1 (alist1 alist2)

; Both alists are polynomial alists, e.g., the car of each pair is a
; term and the cdr of each pair is a rational.  We determine whether
; negating each cdr in alist2 yields alist1.

  (cond ((null alist1) (null alist2))
        ((null alist2) nil)
        ((and (equal (caar alist1) (caar alist2))
              (= (cdar alist1) (- (cdar alist2))))
         (fcomplementary-multiplep1 (cdr alist1) (cdr alist2)))
        (t nil)))

(defun fcomplementary-multiplep (poly1 poly2)

; We determine whether multiplying poly2 by some negative rational
; produces poly1.  We assume that both polys have the same relation,
; e.g., <=, and the same first-var.

; Since we now normalize polys so that their first coefficient is
; +/-1.  That makes this function simpler.  In particular, we now need
; only check whether poly2 is the (arithmetic) negation of poly1.

    (and (= (access poly poly1 :constant)
            (- (access poly poly2 :constant)))
         (fcomplementary-multiplep1 (cdr (access poly poly1 :alist))
                                    (cdr (access poly poly2 :alist)))))

(defun already-used-by-find-equational-polyp1 (poly1 ttree)

; See already-used-by-find-equational-polyp.

  (cond
   ((null ttree) nil)
   ((symbolp (caar ttree))
    (cond
     ((eq (caar ttree) 'find-equational-poly)
      (or (poly-equal (car (cdar ttree)) poly1)
          (already-used-by-find-equational-polyp1 poly1 (cdr ttree))))
     (t (already-used-by-find-equational-polyp1 poly1 (cdr ttree)))))
   (t (or (already-used-by-find-equational-polyp1 poly1 (car ttree))
          (already-used-by-find-equational-polyp1 poly1 (cdr ttree))))))

(defun already-used-by-find-equational-polyp (poly1 hist)

; Poly1 is a positive poly.  Let poly2 be its negative version.  We are
; considering using them to create an equation as part of
; find-equational-poly.  We wish to know whether they have ever been
; so used before.  The answer is found by looking into the history of
; the clause being worked on, hist, for every 'simplify-clause entry.
; Each such entry is of the form (simplify-clause clause ttree).  We
; search ttree for (poly1 . poly2) tagged with 'find-equational-poly.

; Historical Note: Once upon a time, polys were not normalized in the
; sense that the leading coefficient is 1.  Thus, 2x <= 6 and 3 <= x
; were complementary.  To discover whether a poly had been used
; before, we had to know both the positive and the negative form
; involved.  But now polys are normalized and the only complement to 3
; <= x is x <= 3.  Thus, we could change the tag value to be a single
; positive poly instead of both.  You will note that we never actually
; need poly2.

  (cond ((null hist) nil)
        ((and (eq (access history-entry (car hist) :processor)
                  'simplify-clause)
              (already-used-by-find-equational-polyp1 poly1
                                                      (access history-entry
                                                              (car hist)
                                                              :ttree)))
         t)
        (t (already-used-by-find-equational-polyp poly1 (cdr hist)))))

(defun cons-term-binary-+-constant (x term)

; x is an acl2-numberp, possibly complex, term is a rational type term.  We
; make a term equivalent to (binary-+ 'x term).

  (cond ((= x 0) term)
        ((quotep term) (kwote (+ x (cadr term))))
        (t (fcons-term* 'binary-+ (kwote x) term))))

(defun cons-term-unary-- (term)
  (cond ((variablep term) (fcons-term* 'unary-- term))
        ((fquotep term) (kwote (- (cadr term))))
        ((eq (ffn-symb term) 'unary--) (fargn term 1))
        (t (fcons-term* 'unary-- term))))

(defun cons-term-binary-*-constant (x term)

; x is a number (possibly complex), term is a rational type term.  We make a
; term equivalent to (binary-* 'x term).

  (cond ((= x 0) (kwote 0))
        ((= x 1) term)
        ((= x -1) (cons-term-unary-- term))
        ((quotep term) (kwote (* x (cadr term))))
        (t (fcons-term* 'binary-* (kwote x) term))))

(defun find-equational-poly-rhs1 (alist)

; See find-equational-poly-rhs.

  (cond ((null alist) *0*)
        ((null (cdr alist))
         (cons-term-binary-*-constant (- (cdar alist))
                                      (caar alist)))
        (t (cons-term 'binary-+
                      (list
                       (cons-term-binary-*-constant (- (cdar alist))
                                                    (caar alist))
                       (find-equational-poly-rhs1 (cdr alist)))))))

(defun find-equational-poly-rhs (poly1)

; Suppose poly1 and poly2 are complementary multiple <= polys, as
; described in find-equational-poly.  We wish to form the rhs term
; returned by that function.  We know the two polys have the form

; poly1:   k0 + k1*t1 + k2*t2 ... <= 0,      k1 positive
; poly2    j0 + j1*t1 + j2*t2 ... <= 0,      j1 negative

; and if q = k1/j1 then q is negative and ji*q = -ki for each i.

; Thus, k0 + k1*t1 + k2*t2 ... = 0.

; The equation created by find-equational-poly will be lhs = rhs, where lhs
; is t1.  We are to create rhs.  That is:

; rhs = -k0/k1 - k2/k1*t2 ...

; which, if we let c be -1/k1

; rhs = (+ c*k0 (+ c*k2*t2 ...))

; which is what we return.

; However now that we normalize polys, k1 = 1 and j1 = -1, so that q =
; -1 and c = -1.  Hence we now negate, rather than multiplying by c.

  (cons-term-binary-+-constant (- (access poly poly1 :constant))
                               (find-equational-poly-rhs1
                                (cdr (access poly poly1 :alist)))))

(defun find-equational-poly3 (poly1 poly2 hist)

; See find-equational-poly.  This is the function that actually builds
; the affirmative answer returned by that function.  Between this function
; and that one are two others whose only job is to iterate across all the
; potentially acceptable positives and negatives and give to this function
; a potentially appropriate poly1 and poly2.

; We know that poly1 is a positive <= poly that does not descend from
; a (not (equal & &)).  We know that poly2 is a negative <= poly that
; does not descend from a (not (equal & &)).  We know they have the same
; first-var.

; We first determine whether they are complementary multiples of eachother
; and have not been used by find-equational-poly already.  If so, we
; return a ttree and two terms, as described by find-equational-poly.

  (cond ((and (fcomplementary-multiplep poly1 poly2)
              (not (already-used-by-find-equational-polyp poly1 hist)))
         (mv (add-to-tag-tree
              'find-equational-poly
              (cons poly1 poly2)
              (cons-tag-trees (access poly poly1 :ttree)
                              (access poly poly2 :ttree)))
             (first-var poly1)
             (find-equational-poly-rhs poly1)))
        (t (mv nil nil nil))))

(defun find-equational-poly2 (poly1 negatives hist)

; See find-equational-poly.  Poly1 is a positive <= poly with the same
; first var as all the members of negatives.  We scan negatives looking
; for a poly2 that is acceptable.

  (cond
   ((null negatives)
    (mv nil nil nil))
   ((or (not (eq (access poly (car negatives) :relation) '<=))
        (access poly (car negatives) :derived-from-not-equalityp))
    (find-equational-poly2 poly1 (cdr negatives) hist))
   (t
    (mv-let (msg lhs rhs)
      (find-equational-poly3 poly1 (car negatives) hist)
      (cond
       (msg (mv msg lhs rhs))
       (t (find-equational-poly2 poly1 (cdr negatives) 
                                 hist)))))))

(defun find-equational-poly1 (positives negatives hist)

; See find-equational-poly.  Positives and negatives are the
; appropriate fields of the same linear pot.  All the first-vars are
; equal.  We scan the positives and for each <= poly there we look for
; an acceptable member of the negatives.

  (cond
   ((null positives)
    (mv nil nil nil))
   ((or (not (eq (access poly (car positives) :relation) '<=))
        (access poly (car positives) :derived-from-not-equalityp))
    (find-equational-poly1 (cdr positives) negatives hist))
   (t
    (mv-let (msg lhs rhs)
      (find-equational-poly2 (car positives) negatives hist)
      (cond
       (msg (mv msg lhs rhs))
       (t (find-equational-poly1 (cdr positives) negatives hist)))))))

(defun find-equational-poly (pot hist)

; Look for an equation to be derived from this pot.  We look for a
; weak inequality in positives whose negation is a member of
; negatives, which was not the result of linearizing a (not (equal lhs
; rhs)), and which has never been found (and recorded in hist) before.
; The message we look for is our business (we generate and recognize
; them) but they must be in the tag tree stored in the 'simplify-clause
; entries of hist.

; We return three values.  If we find no acceptable poly, we return
; three nils.  Otherwise we return a non-nil ttree and two terms, lhs
; and rhs.  In this case, it is a truth (assuming pot and the
; 'assumptions in the ttree) that lhs = rhs.  As a matter of fact, lhs
; will be the var of the linear-pot pot and rhs will be a +-tree of
; lighter vars.  Of course, the equation can be rearranged and used
; arbitrarily by the caller.

; If the equation is used in the current simplification, the ttree we
; return must find its way into the hist entry for that
; simplify-clause.

; Historical note: The affect of the newly (v2_8) introduced field, 
; :derived-from-not-equalityp, is different from that of the
; earlier function descends-from-not-equalityp.  We are now more
; liberal about the polys we can generate here.  See the discussion
; accompanying the definition of a poly.  (Search for ``(defrec poly''.))

  (find-equational-poly1 (access linear-pot pot :positives)
                         (access linear-pot pot :negatives)
                         hist))

;=================================================================


; Add-polys

(defun get-coeff-for-cancel1 (alist1 alist2)

; Alist1 and alist2 are the alists from two polys which we are about
; to cancel.  We calculate the absolute value of what would be the
; leading coefficient if we added the two alists.  This is in support
; of cancel, which see.

  (cond ((null alist1)
         (if (null alist2)
             1
           (abs (cdar alist2))))
        ((null alist2)
         (abs (cdar alist1)))
        ((not (arith-term-order (caar alist1) (caar alist2)))
         (abs (cdar alist1)))
        ((equal (caar alist1) (caar alist2))
         (let ((temp (+ (cdar alist1)
                        (cdar alist2))))
           (if (eql temp 0)
               (get-coeff-for-cancel1 (cdr alist1) (cdr alist2))
             (abs temp))))
        (t
         (abs (cdar alist2)))))

(defun cancel2 (alist coeff)
  (cond ((null alist)
         nil)
        (t
         (cons (cons (caar alist)
                     (/ (cdar alist) coeff))
               (cancel2 (cdr alist) coeff)))))

(defun cancel1 (alist1 alist2 coeff)

; Alist1 and alist2 are the alists from two polys which we are about
; to cancel.  We create a new alist by adding alist1 and alist2, using
; coeff to normalize the result.  

  (cond ((null alist1)
         (cancel2 alist2 coeff))
        ((null alist2)
         (cancel2 alist1 coeff))
        ((not (arith-term-order (caar alist1) (caar alist2)))
         (cons (cons (caar alist1)
                     (/ (cdar alist1) coeff))
               (cancel1 (cdr alist1) alist2 coeff)))
        ((equal (caar alist1) (caar alist2))
         (let ((temp (/ (+ (cdar alist1)
                           (cdar alist2))
                        coeff)))
           (cond ((= temp 0)
                  (cancel1 (cdr alist1) (cdr alist2) coeff))
                 (t (cons (cons (caar alist1) temp)
                          (cancel1 (cdr alist1) (cdr alist2) coeff))))))
        (t (cons (cons (caar alist2)
                       (/ (cdar alist2) coeff))
                 (cancel1 alist1 (cdr alist2) coeff)))))

(defun cancel (p1 p2)

; P1 and p2 are polynomials with the same first var and opposite
; signs.  We construct the poly obtained by cross-multiplying and
; adding p1 and p2 so as to cancel out the first var.

; Polys are now normalized such that the leading coefficients are
; +/-1.  Hence we no longer need to cross-multiply before adding
; p1 and p2.  (The variables co1 and co2 in the original version
; are now guaranteed to be 1.)  We do add a twist to the naive
; implementation though.  Rather than adding the two alists, and
; then normalizing the result, we calculate what would have been
; the leading coeficient and normalize as we go (dividing by its
; absolute value).

; We return two values.  The first indicates whether we have
; discovered a contradiction.  If the first result is non-nil then it
; is the impossible poly formed by cancelling p1 and p2.  The ttree of
; that poly will be interesting to our callers because it contains
; such things as the assumptions made and the lemmas used to get the
; contradiction.  When we return a contradiction, the second result is
; always nil.  Otherwise, the second result is either nil (meaning that
; the cancellation yeilded a trivially true poly) or is the newly
; formed poly.

; Historical note: The affect of the newly (v2_8) introduced field, 
; :derived-from-not-equalityp, is different from that of the
; earlier function descends-from-not-equalityp.  See the discussion
; accompanying the definition of a poly.  (Search for ``(defrec poly''.))

; Note:  It is sometimes convenient to trace this function with
#|
  (trace (cancel
          :entry (list (show-poly (car si::arglist))
                       (show-poly (cadr si::arglist)))
          :exit (let ((flg (car values))
                      (val (car (mv-refs 1)))) 
                  (cond (flg (append values (mv-refs 1)))
                        (val (list nil (show-poly val)))
                        (t (list nil nil))))))
|#

; Since we now normalize polys, the cars of the two alists will
; cancel each other out and all we have to concern ourselves with
; are their cdrs.

  (let* ((alist1 (cdr (access poly p1 :alist)))
         (alist2 (cdr (access poly p2 :alist)))
         (coeff (get-coeff-for-cancel1 alist1 alist2))
         (p (make poly
                  :constant (/ (+ (access poly p1 :constant)
                                  (access poly p2 :constant))
                               coeff)
                  :alist (cancel1 alist1
                                  alist2
                                  coeff)
                  :relation  (if (or (eq (access poly p1 :relation) '<)
                                     (eq (access poly p2 :relation) '<))
                                 '<
                               '<=)
                  :ttree (cons-tag-trees (access poly p1 :ttree)
                                         (access poly p2 :ttree))
                  :rational-poly-p (and (access poly p1 :rational-poly-p)
                                        (access poly p2 :rational-poly-p))
                  :parents (marry-parents (access poly p1 :parents)
                                          (access poly p2 :parents))
                  :derived-from-not-equalityp nil)))
    (cond ((impossible-polyp p) (mv p nil))
          ((true-polyp p) (mv nil nil))
          (t (mv nil p)))))

(defun cancel-poly-against-all-polys (p polys pt ans)

; P is a poly, polys is a list of polys, the first var of p is the same
; as the first of every poly in polys and has opposite sign.  We are to
; cancel p against each member of polys, getting in each case a
; contradiction, a true poly (which we discard) or a new shorter poly.
; Pt is a parent tree indicating literals we are to avoid.

; We return two answers.  The first is either nil or the first
; contradiction we find.  When the first is a contradiction, the
; second is nil.  Otherwise, the second is the list of all newly
; produced polys.

; Ans is supposed to be nil initially and is the site at which we
; accumulate the new polys.  This is a No-Change Loser.

  (cond ((null polys)
         (mv nil ans))
        ((ignore-polyp (access poly (car polys) :parents) pt)
         (cancel-poly-against-all-polys p (cdr polys)
                                        pt ans))
        (t (mv-let (contradictionp new-p)
             (cancel p (car polys))
             (cond (contradictionp 
                    (mv contradictionp nil))
                   (t 
                    (cancel-poly-against-all-polys
                     p
                     (cdr polys) 
                     pt

; We discard polys which are ``weaker'' (see poly-member and
; poly-weakerp) than one already accumulated into ans.

                     (if (and new-p
                              (not (poly-member new-p ans)))
                         (cons new-p ans)
                       ans))))))))

; Historical note:

; The following functions --- add-polys0 and its callees --- have been
; substantially rewritten.  Previous to Version_2.8 the following
; two comments were in add-poly and add-poly1 (which no longer exists)
; respectively:

; Add-poly historical comment
#|
; This is the fundamental function for changing a pot-lst.  It adds a
; single poly p to pot-lst.  All the other functions which construct
; pot lists do it, ultimately, via calls to add-poly.

; In nqthm this function was called add-equation but since its argument
; is a poly we renamed it.

; This function adds a poly p to the pot-lst.  Since the pot-lst is
; ordered by term-order on the vars, we recurse down the pot-lst just
; far enough to find where p fits.  There are three cases: p goes
; before the current pot, p goes in the current pot, or p goes after
; the current pot.  The first is simplest: make a pot for p and stick
; it at the front of the pot-lst.  The second is not too bad: cancel p
; against every poly of opposite sign in this pot to generate a bunch
; of new polys that belong earlier in the pot-lst and then add p to
; the current pot.  The third is the worst: Recursively add p to the
; rest of the pot-lst, get back a bunch of polys that need processing,
; process the ones that belong where you're standing and pass up the
; ones that go earlier.
|#

; Add-poly1 historical comment
#|
; This is a subroutine of add-poly.  See the comment there.  Suppose
; we've just gotten back from a recursive call of add-poly and it
; returned to us a bunch of polys that belong earlier in the pot-lst
; (from it).  Some of those polys may belong here where we are
; standing.  Others should be passed up.

; To-do is the list of polys produced by the recursive add-poly.  Var,
; positives, and negatives are the appropriate components of the pot
; that add-poly is standing on.  We process those polys in to-do that
; go here, producing new positives and negatives, and set aside those
; that don't go here.  The processing of the ones that do go here may
; create some additional polys that don't go here.  To-do-next is the
; accumulation site for the to-do's we don't handle and the ones our
; processing creates.
|#

; Add-poly is still the fundamental routine for adding a poly to the
; pot-lst.  However, we now merely gather up newly generated polys and
; pass them back out to add-polys --- changing the routines which
; add polys to the pot list from a depth-first search to a
; breadth-first search.

(defun add-poly (p pot-lst to-do-next pt nonlinearp)

; This is the fundamental function for changing a pot-lst.  It adds a
; single poly p to pot-lst.  All the other functions which construct
; pot lists do it, ultimately, via calls to add-poly.

; This function adds a poly p to the pot-lst and returns 3 values.
; The first is the standard contradictionp.  The second value, of
; interest only when we don't find a contradiction, is the new pot-lst
; obtained by adding p to pot-lst.  The third value is a list of new
; polys generated by the adding of p to pot-lst, which must be
; processed.  We cons our own generated polys onto the incoming
; to-do-next to form this result.

; An invariant exploited by infect-new-polys is that all of the new
; polys in any linear pot occur at the front of the list and no polys
; are ever deleted.  That is, if this or any other function wants to
; add a poly to the positives, say, it must cons it onto the front.
; In general, if we have an old linear pot and a new one produced from
; it and we want to process all the polys in the positives, say, of the
; new pot that are not in the old one, it suffices to process the first
; n elements of the new positives, where n is the difference in their
; lengths.

; Note:  If adding a poly creates a new pot, its loop-stopper value is set to
; 0.  This is changed to the correct value (if necessary) in
; add-linear-lemma.

; Trace Note:
#|
  (trace (add-poly
          :entry (let ((args si::arglist))
                   (list (show-poly (nth 0 args)) ;p
                         (show-pot-lst (nth 1 args)) ;pot-lst
                         (show-poly-lst (nth 2 args)) ;to-do-next
                         (nth 3 args)
                         (nth 4 args)
                         '|ens| (nth 6 args) '|wrld|))
          :exit (cond ((null (car values))
                       (list nil
                             (show-pot-lst (mv-ref 1))
                             (show-poly-lst (mv-ref 2))))
                      (t (list (show-poly (car values)) nil nil)))))|#


  (cond
   ((time-limit4-reached-p "Out of time in add-poly.") ; nil, or throws
    (mv nil nil nil))
   ((or (null pot-lst)
        (not (arith-term-order (access linear-pot (car pot-lst) :var)
                               (first-var p))))
    (mv nil
        (cons (if (< 0 (first-coefficient p)) ; p is normalized (below too)
                  (make linear-pot
                        :var (first-var p)
                        :loop-stopper-value 0
                        :positives (list p)
                        :negatives nil)
                (make linear-pot
                      :var (first-var p)
                      :loop-stopper-value 0
                      :positives nil
                      :negatives (list p)))
              pot-lst)
        to-do-next))
   ((equal (access linear-pot (car pot-lst) :var)
           (first-var p))
    (cond
     ((poly-member p
                   (if (< 0 (first-coefficient p))
                       (access linear-pot (car pot-lst) :positives)
                     (access linear-pot (car pot-lst) :negatives)))
      (mv nil pot-lst to-do-next))
     (t (mv-let (contradictionp to-do-next)
          (cancel-poly-against-all-polys
           p
           (if (< 0 (first-coefficient p))
               (access linear-pot (car pot-lst) :negatives)
             (access linear-pot (car pot-lst) :positives))
           pt
           to-do-next)
          (cond
           (contradictionp (mv contradictionp nil nil))

; Non-linear optimization
; Magic number.  If non-linear arithmetic is enabled, and there are
; more than 20 polys in the appropriate side of the pot, we give up
; and do not add the new poly.  This has proven to be a useful heuristic.
; Increasing this number will slow ACL2 down sometimes, but it may
; allow more proofs to go through.  So far I have not seen one which
; needs more than 20, but less than 100 --- which is too much.
; Note that the pot-lst isn't changed (i.e., poly wasn't added to its
; pot) but we will propagate the children poly and (possibly) add them
; to their pots.  These children are "orphans" because a parent is
; missing from the pot-lst.


           ((and nonlinearp
                 (>=-len (if (< 0 (first-coefficient p))
                             (access linear-pot (car pot-lst)
                                     :positives)
                           (access linear-pot (car pot-lst)
                                   :negatives))
                         21))
            (mv nil
                pot-lst
                to-do-next))
           (t (mv nil
                  (cons
                   (if (< 0 (first-coefficient p))
                       (change linear-pot (car pot-lst)
                               :positives
                               (cons p (access linear-pot (car pot-lst)
                                               :positives)))
                     (change linear-pot (car pot-lst)
                             :negatives
                             (cons p (access linear-pot (car pot-lst)
                                             :negatives))))
                   (cdr pot-lst))
                  to-do-next)))))))
   (t
    (mv-let
      (contradictionp cdr-pot-lst to-do-next)
      (add-poly p (cdr pot-lst) to-do-next pt nonlinearp)
      (cond
       (contradictionp (mv contradictionp nil nil))
       (t
        (mv nil (cons (car pot-lst) cdr-pot-lst) to-do-next)))))))

(defun prune-poly-lst (poly-lst ans)
  (cond ((null poly-lst)
         ans)
        ((endp (cddr (access poly (car poly-lst) :alist)))
         (prune-poly-lst (cdr poly-lst) (cons (car poly-lst) ans)))
        (t
         (prune-poly-lst (cdr poly-lst) ans))))

(defun add-polys1 (lst pot-lst new-lst pt nonlinearp max-rounds
                       rounds-completed)

; This function adds every element of the poly list lst to pot-lst and
; accumulates the new polys in new-lst.  When lst is exhausted it
; starts over on the ones in new-lst and iterates that until no new polys
; are produced.  It returns 2 values:  the standard contradictionp in the
; the first and the final pot-lst in the second.

  (cond ((eql max-rounds rounds-completed)
         (mv nil pot-lst))
        ((null lst)
         (cond ((null new-lst)
                (mv nil pot-lst))

; Non-linear optimization
; Magic number.  If non-linear arithmetic is enabled, and there are
; more than 100 polys in lst waiting to be added to the pot-lst, we
; try pruning the list of new polys.  This has proven to be a useful
; heuristic.  Increasing this number will slow ACL2 down sometimes,
; but it may allow more proofs to go through.  So far I have not seen
; one which needs more than 100, but less than 500 --- which is too
; much.
               
               ((and nonlinearp 
                     (>=-len new-lst 101))
                (add-polys1 (prune-poly-lst new-lst nil)
                            pot-lst nil pt nonlinearp
                            max-rounds (+ 1 rounds-completed)))
               (t 
                (add-polys1 new-lst pot-lst nil
                            pt nonlinearp
                            max-rounds (+ 1 rounds-completed)))))
        (t (mv-let (contradictionp new-pot-lst new-lst)
             (add-poly (car lst) pot-lst new-lst pt nonlinearp)
             (cond (contradictionp (mv contradictionp nil))
                   (t (add-polys1 (cdr lst)
                                  new-pot-lst
                                  new-lst
                                  pt
                                  nonlinearp
                                  max-rounds
                                  rounds-completed)))))))

(defun add-polys0 (lst pot-lst pt nonlinearp max-rounds)

; Lst is a list of polys.  We filter out the true ones (and detect any
; impossible ones) and then normalize and add the rest to pot-lst.
; Any new polys thereby produced are also added until there's nothing
; left to do.  We return the standard contradictionp and a new pot-lst.

  (mv-let (contradictionp lst)
    (filter-polys lst nil)
    (cond (contradictionp (mv contradictionp nil))
          (t (add-polys1 lst pot-lst nil pt nonlinearp max-rounds 0)))))

;=================================================================
#|

; "Show-" functions

; The next group of "show-" functions are not part of the system but are
; convenient for system debugging.  (show-poly poly) will create a list
; structure that prints so as to show a polynomial in the conventional
; notation.  The term enclosed in an extra set of parentheses is the leading
; term of the poly.  An example show-poly is '(3 J + (I) + 77 <= 4 M + 2 N).

(defun show-poly2 (pair lst)
  (let ((n (abs (cdr pair)))
        (x (car pair)))
    (cond ((= n 1) (cond ((null lst) (list x))
                         (t (list* x '+ lst))))
          (t (cond ((null lst) (list n x))
                   (t (list* n x '+ lst)))))))

(defun show-poly1 (alist lhs rhs)

; Note: This function ought to return (mv lhs rhs) but when it is used in
; tracing multiply valued functions that functionality hurts us: the
; computation performed during the tracing destroys the multiple value being
; manipulated by the function being traced.  So that we can use this function
; conveniently during tracing, we make it a single valued function.

  (cond ((null alist) (cons lhs rhs))
        ((logical-< 0 (cdar alist))
         (show-poly1 (cdr alist) lhs (show-poly2 (car alist) rhs)))
        (t (show-poly1 (cdr alist) (show-poly2 (car alist) lhs) rhs))))

(defun show-poly (poly)
  (let* ((pair (show-poly1
                   (cond ((null (access poly poly :alist)) nil)
                         (t (cons (cons (list (caar (access poly poly :alist)))
                                        (cdar (access poly poly :alist)))
                                  (cdr (access poly poly :alist)))))
                   (cond ((= (access poly poly :constant) 0)
                          nil)
                         ((logical-< 0 (access poly poly :constant)) nil)
                         (t (cons (- (access poly poly :constant)) nil)))
                   (cond ((= (access poly poly :constant) 0)
                          nil)
                         ((logical-< 0 (access poly poly :constant))
                          (cons (access poly poly :constant) nil))
                         (t nil))))
         (lhs (car pair))
         (rhs (cdr pair)))

; The let* above would be (mv-let (lhs rhs) (show-poly1 ...) ...) had
; show-poly1 been specified to return two values instead of a pair.
; See note above.

    (append (or lhs '(0))
            (cons (access poly poly :relation) (or rhs '(0))))))

(defun show-poly-lst (poly-lst)
  (cond ((null poly-lst) nil)
        (t (cons (show-poly (car poly-lst))
                 (show-poly-lst (cdr poly-lst))))))


(defun show-pot-lst (pot-lst)
  (cond
   ((null pot-lst) nil)
   (t (cons
       (list* :var (access linear-pot (car pot-lst) :var)
              (append (show-poly-lst
                       (access linear-pot (car pot-lst) :negatives))
                      (show-poly-lst
                       (access linear-pot (car pot-lst) :positives))))
       (show-pot-lst (cdr pot-lst))))))

(defun show-type-alist (type-alist)
  (cond ((endp type-alist) nil)
        (t (cons (list (car (car type-alist))
                       (decode-type-set (cadr (car type-alist))))
                 (show-type-alist (cdr type-alist))))))

|#