-
Notifications
You must be signed in to change notification settings - Fork 0
/
simplify.lisp
10007 lines (8635 loc) · 441 KB
/
simplify.lisp
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
; ACL2 Version 8.6 -- A Computational Logic for Applicative Common Lisp
; Copyright (C) 2024, Regents of the University of Texas
; 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 LICENSE file distributed with ACL2.
; 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
; LICENSE for more details.
; Written by: Matt Kaufmann and J Strother Moore
; email: [email protected] and [email protected]
; Department of Computer Science
; University of Texas at Austin
; Austin, TX 78712 U.S.A.
(in-package "ACL2")
; A quick sketch of the three main functions here
; We renamed these functions because their Nqthm names were confusing to
; one of us.
; ACL2 Nqthm
; simplify-clause SIMPLIFY-CLAUSE
; simplify-clause1 SIMPLIFY-CLAUSE0
; rewrite-clause SIMPLIFY-CLAUSE1
; Simplify-clause is the top-level clause simplifier but it does
; relatively little work. It merely determines what to expand and
; what not to, taking into account induction as described in comments
; in simplify-clause. The real workhorse of simplify-clause is its
; subroutine, simplify-clause1.
; Simplify-clause1 is non-recursive. It does an enormous amount of
; clause level work: removing trivial equations, detecting
; propositional tautologies with type-set, setting up the
; simplify-clause-pot-lst for the later literal-by-literal-rewriting,
; detecting linear arithmetic tautologies, and retrieving useful
; equalities from the linear arithmetic pot-lst. Once all that has
; happened, it calls rewrite-clause which begins the classic sweep of
; the clause rewriting each literal.
; Rewrite-clause is concerned only with rewriting the literals of a
; clause. It does not do any clause level work aside from that
; necessary to avoid tail biting. It rewrites each lit in turn,
; clausifies the result into a bunch of segments and splices them into
; the evolving set of answers.
; In this section we develop rewrite-clause.
; Note: The following two functions are no longer called. They were
; called before we made type-set track dependencies. However, after
; that change, we found the burden of passing up the ttrees generated
; below to be so off-putting that we eliminated their calls in favor
; of dumb-negate-lit and a no-op. It is our belief that these changes
; do not seriously weaken the system. Comments indicating the changes
; contain calls of the two functions so these decisions can be
; reconsidered.
(defun negate-lit (term type-alist ens force-flg wrld)
; This function returns a term equivalent to (not term) under the
; given type-alist and wrld. It also returns a ttree justifying this
; result.
; Note Added After This Function Became Obsolete: Because
; known-whether-nil now may generate 'assumptions, negate-lit may
; generate 'assumptions. Thus, use of this function is even more
; problematic since the ttrees not only must be tracked but the
; necessary case splits done.
(mv-let (knownp nilp ttree)
(known-whether-nil term type-alist ens force-flg
nil ; dwp
wrld nil)
(cond (knownp
(cond (nilp (mv *t* ttree))
(t (mv *nil* ttree))))
(t (mv (dumb-negate-lit term) nil)))))
(defun pegate-lit (term type-alist ens force-flg wrld)
; Like negate-lit but returns a term equivalent to term, and a ttree.
; Note Added After This Function Became Obsolete: Because
; known-whether-nil now may generate 'assumptions, negate-lit may
; generate 'assumptions. Thus, use of this function is even more
; problematic since the ttrees not only must be tracked but the
; necessary case splits done.
(mv-let (knownp nilp ttree)
(known-whether-nil term type-alist ens force-flg
nil ; dwp
wrld nil)
(cond (knownp
(cond (nilp (mv *nil* ttree))
(t (mv *t* ttree))))
(t (mv term nil)))))
; Rockwell Addition: Now we know hard-error returns nil too.
(defun add-literal (lit cl at-end-flg)
; We add lit to clause cl, optionally at the end as per the flag.
; We assume that lit has been subjected to rewriting modulo the geneqv
; iff. Therefore, though we check lit against *t* and *nil* we do
; not do more powerful type-set reasoning. In addition, we know that
; (hard-error ctx str alist) is logically nil.
(cond ((quotep lit)
(cond ((equal lit *nil*) cl)
(t *true-clause*)))
((equal cl *true-clause*) *true-clause*)
((member-complement-term lit cl) *true-clause*)
((variablep lit)
(cond ((member-term lit cl) cl)
(at-end-flg (append cl (list lit)))
(t (cons lit cl))))
; Now we can take the ffn-symb of lit.
((eq (ffn-symb lit) 'hard-error)
; (Hard-error ctx str alist) = nil.
cl)
((and (eq (ffn-symb lit) 'rationalp)
(member-complement-term1 (fcons-term 'integerp (fargs lit))
cl))
*true-clause*)
((and (eq (ffn-symb lit) 'not)
(ffn-symb-p (fargn lit 1) 'integerp)
(member-equal (fcons-term 'rationalp (fargs (fargn lit 1))) cl))
*true-clause*)
((member-term lit cl) cl)
(at-end-flg (append cl (list lit)))
(t (cons lit cl))))
(defun add-each-literal (cl)
(cond ((null cl) nil)
(t (add-literal (car cl)
(add-each-literal (cdr cl))
nil))))
; By definition, clause cl1 subsumes clause cl2 provided some instance of cl1
; is a subset of cl2. Operationally, we think of finding a suitable
; substitution, alist. But this involves search since a given literal, lit1,
; of cl1 might be instantiated so that it becomes one of several literals in
; cl2, and which instantiation we choose depends on how we can similarly get
; the rest of cl1's literals ``absorbed.''
; We augment subsumption to handle the special case of clauses containing
; (EQUAL x 'const1) atoms. First, note that cl1 subsumes cl2 below:
; cl1: ((equal x 'const1) p...)
; cl2: ((not (equal x 'const2)) p... q...)
; In particular, modulo the instantiation done for subsumption, subsumption
; just checks the truth of (IMPLIES (OR . cl1) (OR . cl2)). But cl2 may be
; thought of as (IMPLIES (equal x 'const2) (OR p... q...)) and thus we are
; checking
; (IMPLIES (AND (equal x 'const2) (OR (equal x 'const1) p...))
; (OR p... q...))
; which is the same as
; (IMPLIES (AND (equal x 'const2) (OR p...))
; (OR p... q...))
; and hence true.
; To check this thinking for sanity, consider a specific application. Suppose
; we have proved cl1: (or (equal x 'const1) (p x)), and we are later confronted
; by cl2: (or (not (equal A 'const2)) (p A) (q A)). Are we justified in saying
; that the proved theorem establishes cl2? Yes. Think of cl1 as a rewrite
; rule: (implies (not (equal x 'const1)) (iff (p x) t)). Now consider
; rewriting (p A) in cl2. You may assume the falsity of the other literals of
; cl2. So we have (equal A 'const2). Backchain with cl1. We must prove (not
; (equal A 'const1)), which is true because A is 'const2.
; So how extend subsumption to handle instantiation of an
; ``equality-with-a-constant''? First recall the basic subsumption algorithm.
; We think of a literal lit2 from cl2 as ``absorbing'' a literal lit1 of cl1 if
; there is an extension of the current unify substitution alist such that
; lit1/alist is lit2. Then we say that cl1 subsumes cl2 if for every literal
; lit1 of cl1 there is a literal lit2 of cl2 that absorbs it so that the rest
; of the literals of cl1 are subsumed. To extend this basic idea to handle
; equality-with-constants we extend the notion of absorption. We say (NOT
; (EQUAL a const2)) absorbs (EQUAL x const1) if const1 and const2 are distinct
; constants and x unifies with a. This is implemented in the function
; subsumes!1-equality-with-const below.
; We code two versions of subsumption. One, subsumes-rec fails after a certain
; specified number of unification calls. The other, subsumes!-rec has no such
; limit. They must be kept in sync. Both handle the special case of
; equalities with constants and of the dummy EXTRA-INFO literal.
(mutual-recursion
(defun subsumes-rec (count cl1 cl2 alist)
; Keep this nest in sync with the subsumes!-rec nest, which is similar except
; that there is no restriction (count) on the number of one-way-unify1 calls.
; We return a positive or negative integer, according to whether or not
; (respectively) some instance of cl1 via an extension of alist is a subset of
; clause cl2. In either case, the absolute value n of that integer is at most
; count, and (- count n) is the number of one-way-unify1 calls that were made.
; Otherwise we return 0, indicating that we could not determine subsumption
; using fewer than count such calls.
; Here is why subsumes-rec and subsumes1 take a "count" argument to limit the
; number of calls:
; Note that in the worst case, checking whether clause2 of length len2 is an
; instance of clause1 of length len1 is roughly on the order of len2^len1. For
; suppose every term in each clause is (integerp x) for a distinct x, except
; that the last term in the first clause is not a match for any member of the
; second clause. Then each (integerp x) in clause1 can be matched against any
; (integerp y) in clause2, so we have len2*len2*...*len2, len1-1 times.
(declare (type #.*fixnum-type* count))
(the #.*fixnum-type*
(cond ((eql count 0) 0)
((null cl1) count)
((extra-info-lit-p (car cl1))
(subsumes-rec count (cdr cl1) cl2 alist))
((ffn-symb-p (car cl1) 'EQUAL)
(cond ((quotep (fargn (car cl1) 1))
(subsumes1-equality-with-const count
(car cl1)
(fargn (car cl1) 2)
(fargn (car cl1) 1)
(cdr cl1) cl2 cl2 alist))
((quotep (fargn (car cl1) 2))
(subsumes1-equality-with-const count
(car cl1)
(fargn (car cl1) 1)
(fargn (car cl1) 2)
(cdr cl1) cl2 cl2 alist))
(t (subsumes1 count (car cl1) (cdr cl1) cl2 cl2 alist))))
(t (subsumes1 count (car cl1) (cdr cl1) cl2 cl2 alist)))))
(defun subsumes1-equality-with-const (count lit x const1 tl1 tl2 cl2 alist)
(the
#.*fixnum-type*
(cond ((eql count 0) 0)
((null tl2) (-f count))
((extra-info-lit-p (car tl2))
(subsumes1-equality-with-const count lit x const1 tl1 (cdr tl2) cl2 alist))
((and (ffn-symb-p (car tl2) 'NOT)
(ffn-symb-p (fargn (car tl2) 1) 'EQUAL))
(let ((arg1 (fargn (fargn (car tl2) 1) 1))
(arg2 (fargn (fargn (car tl2) 1) 2)))
(cond ((and (quotep arg1)
(not (equal arg1 const1)))
(mv-let
(wonp alist1)
(one-way-unify1 x arg2 alist)
(cond ((not wonp)
(subsumes1-equality-with-const (1-f count) lit x const1 tl1 (cdr tl2) cl2 alist))
(t (let ((new-count (subsumes-rec (1-f count) tl1 cl2 alist1)))
(cond ((<= 0 new-count) new-count)
(t (subsumes1-equality-with-const (-f new-count)
lit x const1 tl1 (cdr tl2)
cl2 alist))))))))
((and (quotep arg2)
(not (equal arg2 const1)))
(mv-let
(wonp alist1)
(one-way-unify1 x arg1 alist)
(cond ((not wonp)
(subsumes1-equality-with-const (1-f count)
lit x const1 tl1 (cdr tl2) cl2 alist))
(t (let ((new-count (subsumes-rec (1-f count) tl1 cl2 alist1)))
(cond ((<= 0 new-count) new-count)
(t (subsumes1-equality-with-const (-f new-count)
lit x const1 tl1 (cdr tl2)
cl2 alist))))))))
(t (subsumes1-equality-with-const count lit x const1 tl1 (cdr tl2) cl2 alist)))))
(t (mv-let
(wonp alist1)
(one-way-unify1 lit (car tl2) alist)
(cond ((not wonp)
(subsumes1-equality-with-const (1-f count) lit x const1 tl1 (cdr tl2) cl2 alist))
(t (let ((new-count (subsumes-rec (1-f count) tl1 cl2 alist1)))
(cond
((<= 0 new-count) new-count)
(t (subsumes1-equality-with-const (-f new-count) lit x const1 tl1 (cdr tl2) cl2 alist)))))))))))
(defun subsumes1 (count lit tl1 tl2 cl2 alist)
; Keep this nest in sync with the subsumes!-rec nest, which is similar except
; that there is no restriction (count) on the number of one-way-unify1 calls.
; If we can extend alist to an alist1 so that lit/alist1 is a member of tl2 and
; tl1/alist1 is a subset of cl2, we return a positive integer obtained by
; decreasing count by the number of one-way-unify1 calls. If we determine that
; there is no such alist, we return a negative integer whose absolute value is
; obtained by decreasing count as above. But, if the number of one-way-unify1
; calls necessary is not less than count, we return 0.
(declare (type #.*fixnum-type* count))
(the #.*fixnum-type*
(cond ((eql count 0) 0)
((null tl2) (-f count))
((extra-info-lit-p (car tl2))
(subsumes1 count lit tl1 (cdr tl2) cl2 alist))
(t (mv-let
(wonp alist1)
(one-way-unify1 lit (car tl2) alist)
(cond
((not wonp)
(subsumes1 (1-f count) lit tl1 (cdr tl2) cl2 alist))
(t
(let ((new-count (subsumes-rec (1-f count) tl1 cl2 alist1)))
(declare (type #.*fixnum-type* new-count))
(cond ((<= 0 new-count) new-count)
(t (subsumes1 (-f new-count) lit tl1 (cdr tl2) cl2
alist)))))))))))
)
(mutual-recursion
(defun subsumes!-rec (cl1 cl2 alist)
; Keep this nest in sync with the subsumes1 nest, which is similar except that
; there is a restriction (count) on the number of one-way-unify1 calls.
; We return t if some instance of cl1 via an extension of alist is a subset of
; clause cl2, otherwise nil.
(cond ((null cl1) t)
((extra-info-lit-p (car cl1))
(subsumes!-rec (cdr cl1) cl2 alist))
((ffn-symb-p (car cl1) 'EQUAL)
(cond ((quotep (fargn (car cl1) 1))
(subsumes!1-equality-with-const (car cl1)
(fargn (car cl1) 2)
(fargn (car cl1) 1)
(cdr cl1) cl2 cl2 alist))
((quotep (fargn (car cl1) 2))
(subsumes!1-equality-with-const (car cl1)
(fargn (car cl1) 1)
(fargn (car cl1) 2)
(cdr cl1) cl2 cl2 alist))
(t (subsumes!1 (car cl1) (cdr cl1) cl2 cl2 alist))))
(t (subsumes!1 (car cl1) (cdr cl1) cl2 cl2 alist))))
(defun subsumes!1-equality-with-const (lit x const1 tl1 tl2 cl2 alist)
(cond ((null tl2) nil)
((extra-info-lit-p (car tl2))
(subsumes!1-equality-with-const lit x const1 tl1 (cdr tl2) cl2 alist))
((and (ffn-symb-p (car tl2) 'NOT)
(ffn-symb-p (fargn (car tl2) 1) 'EQUAL))
(let ((arg1 (fargn (fargn (car tl2) 1) 1))
(arg2 (fargn (fargn (car tl2) 1) 2)))
(cond ((and (quotep arg1)
(not (equal arg1 const1)))
(mv-let
(wonp alist1)
(one-way-unify1 x arg2 alist)
(cond ((and wonp (subsumes!-rec tl1 cl2 alist1))
t)
(t (subsumes!1-equality-with-const lit x const1 tl1 (cdr tl2) cl2 alist)))))
((and (quotep arg2)
(not (equal arg2 const1)))
(mv-let
(wonp alist1)
(one-way-unify1 x arg1 alist)
(cond ((and wonp (subsumes!-rec tl1 cl2 alist1))
t)
(t (subsumes!1-equality-with-const lit x const1 tl1 (cdr tl2) cl2 alist)))))
(t (subsumes!1-equality-with-const lit x const1 tl1 (cdr tl2) cl2 alist)))))
(t (mv-let
(wonp alist1)
(one-way-unify1 lit (car tl2) alist)
(cond ((and wonp (subsumes!-rec tl1 cl2 alist1))
t)
(t (subsumes!1-equality-with-const lit x const1 tl1 (cdr tl2) cl2 alist)))))))
(defun subsumes!1 (lit tl1 tl2 cl2 alist)
; Keep this nest in sync with the subsumes1 nest, which is similar except that
; there is a restriction (count) on the number of one-way-unify1 calls.
; If we can extend alist to an alist1 so that lit/alist1 is a member of tl2 and
; tl1/alist1 is a subset of cl2, we return t; otherwise, nil.
(cond ((null tl2) nil)
((extra-info-lit-p (car tl2))
(subsumes!1 lit tl1 (cdr tl2) cl2 alist))
(t (mv-let
(wonp alist1)
(one-way-unify1 lit (car tl2) alist)
(cond ((and wonp (subsumes!-rec tl1 cl2 alist1))
t)
(t (subsumes!1 lit tl1 (cdr tl2) cl2 alist)))))))
)
(defconst *init-subsumes-count*
(the #.*fixnum-type*
; The following value is rather arbitrary, determined by experimentation so
; that subsumes doesn't run for more than a small fraction of a second on a
; 2.6GH P4 (depending on the underlying Lisp). The following takes about 0.04
; seconds to return '? (signaling that we have done 1,000,000 calls of
; one-way-unify1) on that machine using GCL 2.6.7 and about 0.17 seconds using
; Allegro CL 7.0.
; (subsumes 1000000
; '((integerp x1) (integerp x2) (integerp x3) (integerp x4)
; (integerp x5) (integerp x6) (integerp x7) (integerp x8)
; (foo a))
; '((integerp x1) (integerp x2) (integerp x3) (integerp x4)
; (integerp x5) (integerp x6) (integerp x7) (integerp x8))
; nil)
1000000))
(defun subsumes (init-subsumes-count cl1 cl2 alist)
; If init-subsumes-count is not nil, then it is a nonnegative integer
; specifying a strict upper bound on the number of one-way-unify1 calls. See
; the comment in subsumes-rec for an explanation of why we may want this bound.
; If the return value is t, then we can extend alist to a substitution s such
; that cl1/s is a subset of cl2. If the return value is nil, then we cannot
; thus extend alist. Otherwise (only possible if init-subsumes-count is not
; nil), the return value is '?, in which case we could not make such a
; determination with fewer than init-subsumes-count one-way-unify1 calls.
(cond
((time-limit5-reached-p
"Out of time in subsumption (subsumes).") ; nil, or throws
nil)
((null init-subsumes-count)
(subsumes!-rec cl1 cl2 alist))
(t (let ((temp (subsumes-rec init-subsumes-count cl1 cl2 alist)))
(cond ((eql temp 0)
'?)
(t (< 0 temp)))))))
(defun some-member-subsumes (init-subsumes-count cl-set cl acc)
; Returns t if some member of cl-set subsumes cl, acc if no member of cl-set
; subsumes cl, and '? (only possible if init-subsumes-count is non-nil) if we
; don't know.
(cond ((null cl-set) acc)
(t (let ((temp (subsumes init-subsumes-count (car cl-set) cl nil)))
(cond
((eq temp t))
(t (some-member-subsumes init-subsumes-count (cdr cl-set) cl
(or temp acc))))))))
(defun equal-mod-commuting-lst (cl1 cl2)
(cond ((endp cl1) (endp cl2))
((endp cl2) nil)
(t (and (equal-mod-commuting (car cl1) (car cl2) nil)
(equal-mod-commuting-lst (cdr cl1) (cdr cl2))))))
(defun member-equal-mod-commuting-lst (cl cl-set)
; Consider the following definition (which could be shortened, but equivalent,
; by calling mbt*).
; (defun foo (x)
; (declare (xargs :guard (and (integerp x)
; (< 10 x))))
; (mbe :logic t
; :exec (mbe :logic (car (cons (< 5 x) t))
; :exec t)))
; The naively generated guard proof obligation is as follows.
; (AND (IMPLIES (AND (< 10 X) (INTEGERP X))
; (EQUAL (CAR (CONS (< 5 X) T)) T))
; (IMPLIES (AND (< 10 X) (INTEGERP X))
; (EQUAL T (CAR (CONS (< 5 X) T)))))
; We would like to avoid generating one of those two clauses, and we can do so
; by checking that the two clauses are equal except perhaps for commuted
; equalities and calls of iff. (We could allow calls of equivalence relations
; too, but then we would need to pass in the world and, more significantly, we
; would feel obligated to track equivalence relations by passing back a tag
; ttree.) The present function is essentially (member-equal cl cl-set), except
; that equality is tested using equal-mod-commuting-lst: thus, some member of
; cl-set is identical to cl except that literals can be commuted as explained
; above.
(cond ((endp cl-set) nil)
((equal-mod-commuting-lst cl (car cl-set)) t)
(t (member-equal-mod-commuting-lst cl (cdr cl-set)))))
(defun conjoin-clause-to-clause-set (cl cl-set)
; Once upon a time, in particular, in the two weeks before January 25,
; 1990, we did a subsumption check here. The idea was that if cl was
; subsumed by some member of cl-set, don't add it and if it subsumes
; some member of cl-set, delete that member. That caused unsoundness.
; The reason is that cl-set is not a set of clauses that is
; necessarily going to be proved. For example, cl-set may contain a
; collection of clause segments to which we will eventually add some
; additional hypotheses. If cl-set contains the clause segment ((P
; I)) and then we conjoin the clause segment ((P (F X))) to it, we
; don't want the first segment to subsume the second because we may
; eventually add the additional hypothesis (INTEGERP I) to all the
; segments.
(cond ((member-equal *t* cl) cl-set)
((member-equal-mod-commuting-lst cl cl-set) cl-set)
(t (cons cl cl-set))))
(defun add-each-literal-lst (cl-set)
(cond ((null cl-set) nil)
(t (conjoin-clause-to-clause-set
(add-each-literal (car cl-set))
(add-each-literal-lst (cdr cl-set))))))
(encapsulate
; See conjoin-clause-sets.
((conjoin-clause-sets-bound () t))
(logic)
(local (defun conjoin-clause-sets-bound () 0))
(defthm natp-conjoin-clause-sets-bound
(natp (conjoin-clause-sets-bound))
:rule-classes :type-prescription))
(defun conjoin-clause-sets-bound-builtin ()
; See conjoin-clause-sets.
(declare (xargs :guard t :mode :logic))
50)
(defattach conjoin-clause-sets-bound conjoin-clause-sets-bound-builtin)
(defun conjoin-clause-sets-rec (cl-set1 cl-set2)
(cond ((null cl-set1) cl-set2)
(t (conjoin-clause-to-clause-set
(car cl-set1)
(conjoin-clause-sets-rec (cdr cl-set1) cl-set2)))))
(defun conjoin-clause-to-clause-set-trivial (cl cl-set)
(cond ((member-equal *t* cl) cl-set)
(t (cons cl cl-set))))
(defun conjoin-clause-sets-trivial (cl-set1 cl-set2)
(cond ((null cl-set1) cl-set2)
(t (conjoin-clause-to-clause-set-trivial
(car cl-set1)
(conjoin-clause-sets-trivial (cdr cl-set1) cl-set2)))))
(defun conjoin-clause-sets (cl-set1 cl-set2)
; This function is generally just a thin wrapper for conjoin-clause-sets-rec.
; However, that function has quadratic behavior.
; Here is the motivating example from Alessandro Coglio for
; ; a predicate used below as guard on x, parameterized on a:
; (defund p (x a)
; (declare (xargs :guard (integerp a)))
; (and (natp x)
; (< x a)))
;
; ; a nullary function for an integer, used as the parameter a below:
; (defund c ()
; (declare (xargs :guard t))
; 10)
;
; ; define a function with 1000 params and 1000 guard conjuncts:
; (make-event
; (let ((vars (loop$ for i from 1 to 1000
; collect (packn-pos (list 'x i) 'x)))
; (conjuncts (loop$ for i from 1 to 1000
; collect `(p ,(packn-pos (list 'x i) 'x) (c)))))
; `(defun f ,vars
; (declare (xargs :guard (and ,@conjuncts)))
; (list ,@vars))))
; Here are times measured for the make-event during development of the
; restriction to avoid quadratic behavior, described below, as a function of
; the value attached to conjoin-clause-sets-bound.
; 10: 3.30 seconds
; 50: 3.45 seconds
; 100: 4.22 seconds
; 200: 10.47 seconds
; We rather arbitrarily chose 50, which should be large enough to make it rare
; for the bound to kick in, but small enough to get most of the potential
; benefit of avoiding quadratic behavior. To see the quadratic behavior
; analytically, consider a call (conjoin-clause-sets cl-set1 cl-set2). There
; are |cl-set1| recursive calls, and for each of those we'll count 1 for the
; recursive call and the current |cl-set2| for the call of
; conjoin-clause-to-clause-set. So we have the following, where m is |cl-set1|
; and n is |cl-set2|.
; (n+1) + (n+2) + ... + (n + m)
; = nm + m(m+1)/2
; Our trivial way to avoid quadratic behavior is to bound m: if it exceeds the
; bound then we use a "trivial" (linear) version of conjoin-clause-sets that
; doesn't check membership (mod commuting or otherwise) of a clause in the
; accumulated clause-set.
(cond ((nthcdr (conjoin-clause-sets-bound) cl-set1)
; The bound is exceeded by the length of cl-set1.
(conjoin-clause-sets-trivial cl-set1 cl-set2))
(t
(conjoin-clause-sets-rec cl-set1 cl-set2))))
(defun some-element-member-complement-term (lst1 lst2)
(cond ((null lst1) nil)
((member-complement-term (car lst1) lst2) t)
(t (some-element-member-complement-term (cdr lst1) lst2))))
; Rockwell Addition: We used to just stick them together. Now we add
; each literal to catch cases like hard-error.
(defun disjoin-clauses1 (cl1 cl2)
; This is equivalent to (append cl1 (set-difference-equal cl2 cl1))
; except that we add each literal with add-literal to check for
; complementary pairs, etc.
; Note: This function repeatedly adds literals from cl2 to cl1, at the
; end. So it copies cl1's spine as many times as there are literals
; to add. We used to use the append formulation above but found that
; complementary pairs were being missed once we extended the notion of
; complementary to include rational v integer.
(cond ((endp cl2) cl1)
(t (disjoin-clauses1 (add-literal (car cl2) cl1 t)
(cdr cl2)))))
(defun disjoin-clauses (cl1 cl2)
(cond ((or (equal cl1 *true-clause*)
(equal cl2 *true-clause*))
*true-clause*)
((null cl1) cl2)
((null cl2) cl1)
(t (disjoin-clauses1 cl1 cl2))))
; See comment in disjoin-clause-segment-to-clause-set.
; (defun disjoin-clause-segment-to-clause-set-rec (segment cl-set acc)
; (cond ((null cl-set) acc)
; (t (disjoin-clause-segment-to-clause-set-rec
; segment
; (cdr cl-set)
; (conjoin-clause-to-clause-set
; (disjoin-clauses segment (car cl-set))
; acc)))))
(defun disjoin-clause-segment-to-clause-set (segment cl-set)
; This code is not tail-recursive, but it could be. At one time it caused
; stack overflow problems in LispWorks 4.2.0. Below is some alternate code,
; with a reverse call in order to provide unchanged functionality. Would we
; gain efficiency by eliminating tail recursion at the cost of that reverse
; call? Maybe. A clearer win would be to avoid the reverse call, which should
; be logically OK but could change the prover's behavior, thus invalidating huge
; portions of the regression suite.
; The alternate code is simply the following line, in place of all that
; follows:
; (disjoin-clause-segment-to-clause-set-rec segment (reverse cl-set) nil)
(cond ((null cl-set) nil)
(t (conjoin-clause-to-clause-set
(disjoin-clauses segment (car cl-set))
(disjoin-clause-segment-to-clause-set segment (cdr cl-set))))))
(defun split-on-assumptions (assumptions cl ans)
; Cl is a clause and ans is a set of clauses that will be our answer.
; Assumptions is a list of literals. For each lit in assumptions
; we add a new clause to ans, obtained by adding lit to cl.
(cond ((null assumptions) ans)
(t (split-on-assumptions
(cdr assumptions)
cl
(conjoin-clause-to-clause-set
(add-literal (car assumptions) cl nil)
ans)))))
(defun rewrite-clause-action (lit branches)
; Lit is a term. Branches is the result of clausifying the result of
; rewriting lit. We want to know if anything has happened. The table
; below indicates our result:
; branches result meaning
; {} 'shown-true Lit was rewritten and clausified to
; the empty set, i.e., lit is T under our
; assumptions.
; {NIL} 'shown-false Lit was rewritten and clausified to
; the set containing the empty clause, i.e.,
; lit is NIL under our assumptions.
; {{lit}} 'no-change Neither rewrite nor clausify did anything.
; otherwise 'change
(cond ((consp branches)
(cond ((null (cdr branches))
(cond ((null (car branches))
'shown-false)
((and (null (cdr (car branches)))
(equal lit (car (car branches))))
'no-change)
(t 'change)))
(t 'change)))
(t 'shown-true)))
; Forward Chaining
; ACL2 implements a rudimentary form of forward chaining -- though it is
; getting less rudimentary as time goes on! Its primary use is at the
; top-level of clause simplification (simplify-clause1), where before we begin
; to rewrite the literals of the clause (and in the same place we set up the
; simplify-clause-pot-lst), we forward chain from the negations of the literals
; of the clause and construct a list of all the (heuristically approved)
; conclusions we can derive. Each concl is paired with a tree that contains
; the 'lemma and 'pt dependencies. That list of pairs is passed down to the
; rewrite-clause level, where it is used to augment the type-alist before
; rewriting any given literal.
; This is the fourth (or fifth, depending on how you count) version of forward
; chaining. For an extensive comment on version II, see the historical plaque
; after the definition of rewrite-clause-type-alist. (There are also
; historical plaques elsewhere in this code.)
; The top-level interface to forward chaining is the function named
; forward-chain. However, forward-chain just calls forward-chain-top with one
; more argument, a token identifying the caller. We tend to use
; forward-chain-top in our code so that a sensible caller is known. But we
; provide forward-chain, with caller 'miscellaneous, mainly for builders of
; tools.
; Besides its use in simplify-clause1, forward-chain-top is called in several
; other places, including built-in-clausep (which is used in preprocess-clause
; and indirectly in defun's prove-termination), bdd-clause (which is used when
; we apply :bdd hints), get-induction-cands-from-cl-set1 (used in firing
; induction rules while computing induction schemes), and hyps-type-alist (used
; in show-rewrites). All of these provide sensible caller tokens. The caller
; is only relevant to the trace-like reporting facility.
; Basic Ideas and Terminology
; Forward chaining is implemented by the function forward-chain-top. At the
; highest level, think of forward chaining as ``activating'' all the forward
; chaining rules triggered by the terms in the problem and then ``advancing''
; each activation in the context of a type-alist that tells us all the things
; we know. An activation is actually an object with fields such as the
; instantiated hypothesis we're trying to relieve, the remaining hyps, the
; unify substitution, etc. To advance an activation we check each
; (instantiated) hyp successively against the type-alist with type-set. If we
; reach the end of the hyps, we know the conclusions of the rule are all true.
; We record each such deduced conclusion as an ``fc-derivation,'' aka an
; ``fcd,'' a kind of record. (Note that just because we create an fcd does not
; mean we will incorporate it into our assumptions. More on this below.) If
; we reach a hyp whose truth is not known under the current type-alist, we
; ``suspend'' the activation. Of course, if a hyp is found to be false, we
; simply drop the activation. We must also handle the branching caused by free
; vars in a hyp -- which causes an activation to split into several different
; activations under each of the possible matches for the free vars plus to
; remain suspended in case additional matches arise later.
; When we have advanced all the activations we have a list of still-suspended
; activations and a list of forward-chaining derivations deduced so far. We
; then heuristically decide which of the derivations to keep. This is called
; ``approving'' the derivations and is imposed to prevent pumps like (implies
; (p x) (p (f x))) from causing infinite forward chaining. Thus, one must be
; careful to distinguish ``fcds'' from ``approved fcds,'' a subset of the
; former though there is no indicator in the fc-derivation record to indicate
; that an fcd has been approved. A key heuristic in approving an fcd is that
; the derived conclusion should not be worse than any conclusion used in its
; derivation. This means we must be able to determine which conclusions were
; used in the derivation of another one. We do that rather cheaply by
; embedding ttrees in fc-derivations. These ttrees are tainted from the
; perspective of the rest of the code, because they have dependencies buried
; inside them. We discuss this when we introduce them but it gives rise to
; such notions as an ``fcd-free'' ttree -- that is, a normal ttree as opposed
; to one with fc-derivations containing other ttrees in it -- and ``expunging''
; the fc-derivations from a non-fcd-free ttree to get an fcd-free ttree. The
; forward chaining module traffics in non-fcd-free ttrees but ultimately
; returns fcd-free ttrees and type-alists that may be used in the rest of the
; prover.
; Once we have collected the approved derivations, we assume them all obtaining
; a new type-alist. It is at that point that we process the disjunction
; triples, possibly shrinking some clauses or even deducing some new
; conclusions and getting a new type-alist. During the processing we assume
; that if an fcd was approved then any disjunct in it is approved. Thus, the
; fcds produced by eliminating all but one literal in a clause is added to the
; list of approved fcds. Since the newly added conclusions may contain new
; terms, we add more activations to our list of suspended activations. Then we
; start another ``round'' in which we try again to advance the suspended
; activations in the context of the new type-alist.
; The notion of a round is implemented by forward-chain1. The top-level
; forward chain just sets up the initial type-alist and the initial activations
; and calls forward-chain1, and then expunges and elaborates the type-alist a
; little. The notion of advancing an activation is implemented by a nest of
; three functions named advance-fc-activation1, 2, and 3, which roughly put,
; are designed to relieve a single hyp, relieve a list of hyps, and relieve
; hyps under a multiplicity of matches for free-vars. Advancing an
; fc-activation introduces the notion of a ``virtual activation'' to avoid
; consing up activation objects as we move from hyp to hyp, for example. A
; virtual activation, v, is an ordinary activation object, o, together with
; values held in certain local variables of the ``advance-fc-activation''
; functions; the actual activation represented by v could be obtained by
; writing those values to their respective fields in o. But we don't do that
; until it is time to suspend the virtual activation because we get blocked.
; Finally, we also squirrel away certain data in a wormhole, named
; ``fc-wormhole'' to allow us to create a ``report'' on what happened in
; forward chaining. Because forward chaining is called in several places and
; is an algorithm (like resolution) in which things are happening on many
; fronts (activations) at once, rather than a real-time trace-like facility we
; provide an after-the-fact reporting facility.
; We repeat some of this introductory material as we develop the code. We also
; provide prettyify-fc-activation and prettyify-fc-derivation for debugging
; purposes even though they are not used in this code. Prettyify-fc-derivation
; is particularly useful because it builds a decent representation of the
; derivation tree of conclusion produced by forward chaining and thus can help
; you understand fc-derivations and what has actually happened in a proof
; attempt.
; A forward chaining rule is (not defined in rewrite.lisp):
; (defrec forward-chaining-rule
; ((rune . nume) trigger hyps concls . match-free) nil)
; One of the main inefficiencies in our earlier forward chaining schemes
; was that if a rule began to fire but misfired because some hyp could
; not be relieved, we would reconsider firing it later and redo the work
; associated with the misfire. We avoid that by storing what we call a
; "forward chaining activation" record which permits us to suspend the
; attempt to fire a rule and resume it later.
(defrec fc-activation
(inst-hyp (hyps . ttree)
unify-subst inst-trigger . rule) t)
; Warning: Despite the name, inst-hyp is not necessarily a term!
; See below.
; Warning: If you reorder the fields or add new ones, reconsider
; suspend-fc-activation, which is designed to save conses by exploiting
; the layout. Suspend-fc-activation is correct independently of the
; order of the fields, but may not actually save conses if they're
; rearranged.
; An fc-activation represents an attempt to apply the given
; forward-chaining-rule. Suppose a term of interest unifies with the
; trigger term of some rule. Then we try to relieve the hypotheses of
; that rule, using the current set of assumptions coded in a type-alist.
; Imagine that we relieve all those up to but not including hypn,
; producing an extended unify substitution and a ttree recording the
; dependencies so far. But then we learn that hypn is not yet
; definitely nil or definitely non-nil. Since the list of assumptions
; is growing, we may be able eventually to establish hypn. Therefore,
; instead of just quitting and starting over we suspend the attempted
; application of rule by producing an fc-activation record containing
; our current state.
; The current :unify-subst, :ttree and :rule are stored in the slots of
; those names. The :inst-trigger is the term in the current problem
; that fired this rule. What about :inst-hyps and :hyps? What do they
; hold? There are two cases of interest depending on whether the hyp we
; are stuck on (hypn above) contains free variables under unify-subst.
; :Inst-hyp is just hypn/unify-subst if hypn contains no free variables
; wrt unify-subst. In that case, :hyps is the cdr of the rule's hyps
; starting immediately after hypn. Furthermore, :inst-hyp is never an
; evaluable ground term (or else we would have evaluated it) or a FORCE
; or CASE-SPLIT (or else we would have forced or split on it). That is,
; :inst-hyp is a term that must be true under type-alist to proceed, and
; :hyps contains the hyps we must relieve after relieving inst-hyp. (We
; cannot get stuck on a hypothesis that is forced or split unless it
; contains free variables. So we never build an activation stuck on
; such a hyp.)
; :Inst-hyp is a special marker, called the :FC-FREE-VARS marker, if
; hypn contains free variables wrt unify-subst. In this case, :hyps is
; the cdr of the rule's hyps starting with the problematic hypn. The
; :FC-FREE-VARS marker looks like this and so is not a term:
; (:FC-FREE-VARS forcer-fn . last-keys-seen)
; Forcer-fn is nil if the hyp is not to be forced, and is either FORCE
; or CASE-SPLIT otherwise. (By providing for forcer-fn we can isolate
; the handling of free vars into one piece of code. Observe how
; advance-fc-activation2 calls advance-fc-activation1 when the hyp in
; question has free vars.) The FORCE or CASE-SPLIT annotation will have
; been stripped off of the car of :hyps, so that what is there is what
; must be found. Last-keys-seen is a list of all the keys ever
; used to create matches up to now -- and thus those keys should be
; avoided in the future.
; Summary: :inst-hyp is either a term or a non-term starting with
; :FC-FREE-VARS. If the former, it is the fully instantiated term that
; must be true under the current type-alist to proceed, it is not an
; evaluable ground term (except for possibly a constant like *t*) or a
; FORCE or CASE-SPLIT, and :hyps is the rest of the hyps. If the
; latter, the marker tells us how to match it without reproducing
; matches already created and whether to force or split on it. Note
; that we consider it very odd and rare to see a forced or split
; free-var hypothesis since it is either matched right away or
; introduces UNBOUND-FREE-vars into the proof.
; Historical Plaque: Forward chaining was first coded before type-set
; could force 'assumptions. Thus, splitting on 'assumptions was
; uncommon, indeed, it was only done for the output of linear
; arithmetic, where we first used the idea in the late 70's. Thus, the
; forward chaining mechanism was designed so as not to produce any
; 'assumptions, i.e., so as not to call rewrite. When type-set was
; extended, assumption generation and handling became more wide-spread.
; In particular, this function can generate assumptions due to the call
; of type-set below and those assumptions are handled by the caller of
; the forward-chaining module. So now, except for these historical
; comments, there is no rationale behind this function's abstinence from
; rewrite. Mixing forward and backward chaining so intimately might be
; interesting. It might also be a can of worms. It might also be
; inevitable. It just isn't the most important thing to do just yet.
; Historical Plaque: As of Version_4.1 we had a heuristic oversight in
; forward chaining that allowed the presence of one (irrelevant) forward
; chaining rule to thwart the application of a relevant forward chaining
; rule. Here I describe how. Suppose we have a relevant rule whose
; activation is blocked because it needs (FOOP x) where x is free.
; Suppose (FOOP (A)) is derived by some irrelevant rule. Then the
; relevant activation advances, choosing (A) for x. Eventually that
; activation terminates, e.g., because we can't prove the next hyp about
; x when x is (A). In Version_4.1 and before, all traces of the
; relevant activation are lost when it is advanced over (FOOP x). So if
; a subsequent rule derives (FOOP (B)) for us, we never make that choice
; for x. In summary: the irrelevant rule derives a spurious guess for x
; and we never try the relevant rule with the right choice of x, even
; though the choice is suggested on the eventual type-alist. This
; actually happened in an example distilled by Dave Greve. The obvious
; problem with leaving the relevant activation around, still blocked on
; (FOOP x), is that we'll repeatedly re-discover the possibility that x
; is (A). In discussing how to avoid such redundancy, Dave suggested
; searching only the ``new'' part of each type-alist (new since the last
; attempt to guess free vars). However, that idea doesn't work because
; we cannot determine what part of the type-alist is ``new'' since we do
; not necessary just add pairs to a type-alist. End of Plaque.
; When we advance an activation we keep the inst-hyp, hyp, unify-subst,
; and ttree fields in variables and only put them back into the activation
; record when we decide to suspend it. They may or may not have changed.
(defun suspend-fc-activation (act inst-hyp hyps unify-subst ttree)
; This function is equivalent to
; (change fc-activation act
; :inst-hyp inst-hyp
; :hyps hyps
; :unify-subst unify-subst
; :ttree ttree)
; This would take 4 conses given the layout:
; (defrec fc-activation
; (inst-hyp (hyps . ttree)
; unify-subst inst-trigger . rule) t)
; But, for example, if only inst-hyp changes, then it could be done in 1 cons.
; So we optimize three cases: (a) where none of the fields change, (b) where
; :unify-subst didn't change, and (c) where only :inst-hyp changed. These
; cases are chosen both for their estimated frequency and the fact that the
; data structure actually permits conses to be saved. Case (a) is perhaps most
; common, when we make no progress relieving the hypothesis we're stuck on and
; free variables are not involved at all. Case (b) is when we've made progress
; but not selected any new free variables. Case (c) probably cannot occur --
; if inst-hyp changed then hyps changes too -- but we coded it because it was
; straightforward to do and because in past versions of this code it was
; possible for inst-hyp alone to change and thus it may become possible again.
; The only sense in which this function depends on the shape of
; fc-activation records is that if the shape were rearranged these
; optimizations might not save any conses. The correctness of the
; function (given its arguments) is independent of the shape of the
; record.