Commit | Line | Data |
---|---|---|
1b706edf LC |
1 | ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; |
2 | ; File: sboyer.sch | |
3 | ; Description: The Boyer benchmark | |
4 | ; Author: Bob Boyer | |
5 | ; Created: 5-Apr-85 | |
6 | ; Modified: 10-Apr-85 14:52:20 (Bob Shaw) | |
7 | ; 22-Jul-87 (Will Clinger) | |
8 | ; 2-Jul-88 (Will Clinger -- distinguished #f and the empty list) | |
9 | ; 13-Feb-97 (Will Clinger -- fixed bugs in unifier and rules, | |
10 | ; rewrote to eliminate property lists, and added | |
11 | ; a scaling parameter suggested by Bob Boyer) | |
12 | ; 19-Mar-99 (Will Clinger -- cleaned up comments) | |
13 | ; 4-Apr-01 (Will Clinger -- changed four 1- symbols to sub1) | |
14 | ; Language: Scheme | |
15 | ; Status: Public Domain | |
16 | ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; | |
17 | ||
18 | ;;; SBOYER -- Logic programming benchmark, originally written by Bob Boyer. | |
19 | ;;; Much less CONS-intensive than NBOYER because it uses Henry Baker's | |
20 | ;;; "sharing cons". | |
21 | ||
22 | ; Note: The version of this benchmark that appears in Dick Gabriel's book | |
23 | ; contained several bugs that are corrected here. These bugs are discussed | |
24 | ; by Henry Baker, "The Boyer Benchmark Meets Linear Logic", ACM SIGPLAN Lisp | |
25 | ; Pointers 6(4), October-December 1993, pages 3-10. The fixed bugs are: | |
26 | ; | |
27 | ; The benchmark now returns a boolean result. | |
28 | ; FALSEP and TRUEP use TERM-MEMBER? rather than MEMV (which is called MEMBER | |
29 | ; in Common Lisp) | |
30 | ; ONE-WAY-UNIFY1 now treats numbers correctly | |
31 | ; ONE-WAY-UNIFY1-LST now treats empty lists correctly | |
32 | ; Rule 19 has been corrected (this rule was not touched by the original | |
33 | ; benchmark, but is used by this version) | |
34 | ; Rules 84 and 101 have been corrected (but these rules are never touched | |
35 | ; by the benchmark) | |
36 | ; | |
37 | ; According to Baker, these bug fixes make the benchmark 10-25% slower. | |
38 | ; Please do not compare the timings from this benchmark against those of | |
39 | ; the original benchmark. | |
40 | ; | |
41 | ; This version of the benchmark also prints the number of rewrites as a sanity | |
42 | ; check, because it is too easy for a buggy version to return the correct | |
43 | ; boolean result. The correct number of rewrites is | |
44 | ; | |
45 | ; n rewrites peak live storage (approximate, in bytes) | |
46 | ; 0 95024 | |
47 | ; 1 591777 | |
48 | ; 2 1813975 | |
49 | ; 3 5375678 | |
50 | ; 4 16445406 | |
51 | ; 5 51507739 | |
52 | ||
53 | ; Sboyer is a 2-phase benchmark. | |
54 | ; The first phase attaches lemmas to symbols. This phase is not timed, | |
55 | ; but it accounts for very little of the runtime anyway. | |
56 | ; The second phase creates the test problem, and tests to see | |
57 | ; whether it is implied by the lemmas. | |
58 | ||
59 | (define (sboyer-benchmark . args) | |
60 | (let ((n (if (null? args) 0 (car args)))) | |
61 | (setup-boyer) | |
62 | (run-benchmark (string-append "sboyer" | |
63 | (number->string n)) | |
64 | 1 | |
65 | (lambda () (test-boyer n)) | |
66 | (lambda (rewrites) | |
67 | (and (number? rewrites) | |
68 | (case n | |
69 | ((0) (= rewrites 95024)) | |
70 | ((1) (= rewrites 591777)) | |
71 | ((2) (= rewrites 1813975)) | |
72 | ((3) (= rewrites 5375678)) | |
73 | ((4) (= rewrites 16445406)) | |
74 | ((5) (= rewrites 51507739)) | |
75 | ; If it works for n <= 5, assume it works. | |
76 | (else #t))))))) | |
77 | ||
78 | (define (setup-boyer) #t) ; assigned below | |
79 | (define (test-boyer) #t) ; assigned below | |
80 | ||
81 | ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; | |
82 | ; | |
83 | ; The first phase. | |
84 | ; | |
85 | ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; | |
86 | ||
87 | ; In the original benchmark, it stored a list of lemmas on the | |
88 | ; property lists of symbols. | |
89 | ; In the new benchmark, it maintains an association list of | |
90 | ; symbols and symbol-records, and stores the list of lemmas | |
91 | ; within the symbol-records. | |
92 | ||
93 | (let () | |
94 | ||
95 | (define (setup) | |
96 | (add-lemma-lst | |
97 | (quote ((equal (compile form) | |
98 | (reverse (codegen (optimize form) | |
99 | (nil)))) | |
100 | (equal (eqp x y) | |
101 | (equal (fix x) | |
102 | (fix y))) | |
103 | (equal (greaterp x y) | |
104 | (lessp y x)) | |
105 | (equal (lesseqp x y) | |
106 | (not (lessp y x))) | |
107 | (equal (greatereqp x y) | |
108 | (not (lessp x y))) | |
109 | (equal (boolean x) | |
110 | (or (equal x (t)) | |
111 | (equal x (f)))) | |
112 | (equal (iff x y) | |
113 | (and (implies x y) | |
114 | (implies y x))) | |
115 | (equal (even1 x) | |
116 | (if (zerop x) | |
117 | (t) | |
118 | (odd (sub1 x)))) | |
119 | (equal (countps- l pred) | |
120 | (countps-loop l pred (zero))) | |
121 | (equal (fact- i) | |
122 | (fact-loop i 1)) | |
123 | (equal (reverse- x) | |
124 | (reverse-loop x (nil))) | |
125 | (equal (divides x y) | |
126 | (zerop (remainder y x))) | |
127 | (equal (assume-true var alist) | |
128 | (cons (cons var (t)) | |
129 | alist)) | |
130 | (equal (assume-false var alist) | |
131 | (cons (cons var (f)) | |
132 | alist)) | |
133 | (equal (tautology-checker x) | |
134 | (tautologyp (normalize x) | |
135 | (nil))) | |
136 | (equal (falsify x) | |
137 | (falsify1 (normalize x) | |
138 | (nil))) | |
139 | (equal (prime x) | |
140 | (and (not (zerop x)) | |
141 | (not (equal x (add1 (zero)))) | |
142 | (prime1 x (sub1 x)))) | |
143 | (equal (and p q) | |
144 | (if p (if q (t) | |
145 | (f)) | |
146 | (f))) | |
147 | (equal (or p q) | |
148 | (if p (t) | |
149 | (if q (t) | |
150 | (f)))) | |
151 | (equal (not p) | |
152 | (if p (f) | |
153 | (t))) | |
154 | (equal (implies p q) | |
155 | (if p (if q (t) | |
156 | (f)) | |
157 | (t))) | |
158 | (equal (fix x) | |
159 | (if (numberp x) | |
160 | x | |
161 | (zero))) | |
162 | (equal (if (if a b c) | |
163 | d e) | |
164 | (if a (if b d e) | |
165 | (if c d e))) | |
166 | (equal (zerop x) | |
167 | (or (equal x (zero)) | |
168 | (not (numberp x)))) | |
169 | (equal (plus (plus x y) | |
170 | z) | |
171 | (plus x (plus y z))) | |
172 | (equal (equal (plus a b) | |
173 | (zero)) | |
174 | (and (zerop a) | |
175 | (zerop b))) | |
176 | (equal (difference x x) | |
177 | (zero)) | |
178 | (equal (equal (plus a b) | |
179 | (plus a c)) | |
180 | (equal (fix b) | |
181 | (fix c))) | |
182 | (equal (equal (zero) | |
183 | (difference x y)) | |
184 | (not (lessp y x))) | |
185 | (equal (equal x (difference x y)) | |
186 | (and (numberp x) | |
187 | (or (equal x (zero)) | |
188 | (zerop y)))) | |
189 | (equal (meaning (plus-tree (append x y)) | |
190 | a) | |
191 | (plus (meaning (plus-tree x) | |
192 | a) | |
193 | (meaning (plus-tree y) | |
194 | a))) | |
195 | (equal (meaning (plus-tree (plus-fringe x)) | |
196 | a) | |
197 | (fix (meaning x a))) | |
198 | (equal (append (append x y) | |
199 | z) | |
200 | (append x (append y z))) | |
201 | (equal (reverse (append a b)) | |
202 | (append (reverse b) | |
203 | (reverse a))) | |
204 | (equal (times x (plus y z)) | |
205 | (plus (times x y) | |
206 | (times x z))) | |
207 | (equal (times (times x y) | |
208 | z) | |
209 | (times x (times y z))) | |
210 | (equal (equal (times x y) | |
211 | (zero)) | |
212 | (or (zerop x) | |
213 | (zerop y))) | |
214 | (equal (exec (append x y) | |
215 | pds envrn) | |
216 | (exec y (exec x pds envrn) | |
217 | envrn)) | |
218 | (equal (mc-flatten x y) | |
219 | (append (flatten x) | |
220 | y)) | |
221 | (equal (member x (append a b)) | |
222 | (or (member x a) | |
223 | (member x b))) | |
224 | (equal (member x (reverse y)) | |
225 | (member x y)) | |
226 | (equal (length (reverse x)) | |
227 | (length x)) | |
228 | (equal (member a (intersect b c)) | |
229 | (and (member a b) | |
230 | (member a c))) | |
231 | (equal (nth (zero) | |
232 | i) | |
233 | (zero)) | |
234 | (equal (exp i (plus j k)) | |
235 | (times (exp i j) | |
236 | (exp i k))) | |
237 | (equal (exp i (times j k)) | |
238 | (exp (exp i j) | |
239 | k)) | |
240 | (equal (reverse-loop x y) | |
241 | (append (reverse x) | |
242 | y)) | |
243 | (equal (reverse-loop x (nil)) | |
244 | (reverse x)) | |
245 | (equal (count-list z (sort-lp x y)) | |
246 | (plus (count-list z x) | |
247 | (count-list z y))) | |
248 | (equal (equal (append a b) | |
249 | (append a c)) | |
250 | (equal b c)) | |
251 | (equal (plus (remainder x y) | |
252 | (times y (quotient x y))) | |
253 | (fix x)) | |
254 | (equal (power-eval (big-plus1 l i base) | |
255 | base) | |
256 | (plus (power-eval l base) | |
257 | i)) | |
258 | (equal (power-eval (big-plus x y i base) | |
259 | base) | |
260 | (plus i (plus (power-eval x base) | |
261 | (power-eval y base)))) | |
262 | (equal (remainder y 1) | |
263 | (zero)) | |
264 | (equal (lessp (remainder x y) | |
265 | y) | |
266 | (not (zerop y))) | |
267 | (equal (remainder x x) | |
268 | (zero)) | |
269 | (equal (lessp (quotient i j) | |
270 | i) | |
271 | (and (not (zerop i)) | |
272 | (or (zerop j) | |
273 | (not (equal j 1))))) | |
274 | (equal (lessp (remainder x y) | |
275 | x) | |
276 | (and (not (zerop y)) | |
277 | (not (zerop x)) | |
278 | (not (lessp x y)))) | |
279 | (equal (power-eval (power-rep i base) | |
280 | base) | |
281 | (fix i)) | |
282 | (equal (power-eval (big-plus (power-rep i base) | |
283 | (power-rep j base) | |
284 | (zero) | |
285 | base) | |
286 | base) | |
287 | (plus i j)) | |
288 | (equal (gcd x y) | |
289 | (gcd y x)) | |
290 | (equal (nth (append a b) | |
291 | i) | |
292 | (append (nth a i) | |
293 | (nth b (difference i (length a))))) | |
294 | (equal (difference (plus x y) | |
295 | x) | |
296 | (fix y)) | |
297 | (equal (difference (plus y x) | |
298 | x) | |
299 | (fix y)) | |
300 | (equal (difference (plus x y) | |
301 | (plus x z)) | |
302 | (difference y z)) | |
303 | (equal (times x (difference c w)) | |
304 | (difference (times c x) | |
305 | (times w x))) | |
306 | (equal (remainder (times x z) | |
307 | z) | |
308 | (zero)) | |
309 | (equal (difference (plus b (plus a c)) | |
310 | a) | |
311 | (plus b c)) | |
312 | (equal (difference (add1 (plus y z)) | |
313 | z) | |
314 | (add1 y)) | |
315 | (equal (lessp (plus x y) | |
316 | (plus x z)) | |
317 | (lessp y z)) | |
318 | (equal (lessp (times x z) | |
319 | (times y z)) | |
320 | (and (not (zerop z)) | |
321 | (lessp x y))) | |
322 | (equal (lessp y (plus x y)) | |
323 | (not (zerop x))) | |
324 | (equal (gcd (times x z) | |
325 | (times y z)) | |
326 | (times z (gcd x y))) | |
327 | (equal (value (normalize x) | |
328 | a) | |
329 | (value x a)) | |
330 | (equal (equal (flatten x) | |
331 | (cons y (nil))) | |
332 | (and (nlistp x) | |
333 | (equal x y))) | |
334 | (equal (listp (gopher x)) | |
335 | (listp x)) | |
336 | (equal (samefringe x y) | |
337 | (equal (flatten x) | |
338 | (flatten y))) | |
339 | (equal (equal (greatest-factor x y) | |
340 | (zero)) | |
341 | (and (or (zerop y) | |
342 | (equal y 1)) | |
343 | (equal x (zero)))) | |
344 | (equal (equal (greatest-factor x y) | |
345 | 1) | |
346 | (equal x 1)) | |
347 | (equal (numberp (greatest-factor x y)) | |
348 | (not (and (or (zerop y) | |
349 | (equal y 1)) | |
350 | (not (numberp x))))) | |
351 | (equal (times-list (append x y)) | |
352 | (times (times-list x) | |
353 | (times-list y))) | |
354 | (equal (prime-list (append x y)) | |
355 | (and (prime-list x) | |
356 | (prime-list y))) | |
357 | (equal (equal z (times w z)) | |
358 | (and (numberp z) | |
359 | (or (equal z (zero)) | |
360 | (equal w 1)))) | |
361 | (equal (greatereqp x y) | |
362 | (not (lessp x y))) | |
363 | (equal (equal x (times x y)) | |
364 | (or (equal x (zero)) | |
365 | (and (numberp x) | |
366 | (equal y 1)))) | |
367 | (equal (remainder (times y x) | |
368 | y) | |
369 | (zero)) | |
370 | (equal (equal (times a b) | |
371 | 1) | |
372 | (and (not (equal a (zero))) | |
373 | (not (equal b (zero))) | |
374 | (numberp a) | |
375 | (numberp b) | |
376 | (equal (sub1 a) | |
377 | (zero)) | |
378 | (equal (sub1 b) | |
379 | (zero)))) | |
380 | (equal (lessp (length (delete x l)) | |
381 | (length l)) | |
382 | (member x l)) | |
383 | (equal (sort2 (delete x l)) | |
384 | (delete x (sort2 l))) | |
385 | (equal (dsort x) | |
386 | (sort2 x)) | |
387 | (equal (length (cons x1 | |
388 | (cons x2 | |
389 | (cons x3 (cons x4 | |
390 | (cons x5 | |
391 | (cons x6 x7))))))) | |
392 | (plus 6 (length x7))) | |
393 | (equal (difference (add1 (add1 x)) | |
394 | 2) | |
395 | (fix x)) | |
396 | (equal (quotient (plus x (plus x y)) | |
397 | 2) | |
398 | (plus x (quotient y 2))) | |
399 | (equal (sigma (zero) | |
400 | i) | |
401 | (quotient (times i (add1 i)) | |
402 | 2)) | |
403 | (equal (plus x (add1 y)) | |
404 | (if (numberp y) | |
405 | (add1 (plus x y)) | |
406 | (add1 x))) | |
407 | (equal (equal (difference x y) | |
408 | (difference z y)) | |
409 | (if (lessp x y) | |
410 | (not (lessp y z)) | |
411 | (if (lessp z y) | |
412 | (not (lessp y x)) | |
413 | (equal (fix x) | |
414 | (fix z))))) | |
415 | (equal (meaning (plus-tree (delete x y)) | |
416 | a) | |
417 | (if (member x y) | |
418 | (difference (meaning (plus-tree y) | |
419 | a) | |
420 | (meaning x a)) | |
421 | (meaning (plus-tree y) | |
422 | a))) | |
423 | (equal (times x (add1 y)) | |
424 | (if (numberp y) | |
425 | (plus x (times x y)) | |
426 | (fix x))) | |
427 | (equal (nth (nil) | |
428 | i) | |
429 | (if (zerop i) | |
430 | (nil) | |
431 | (zero))) | |
432 | (equal (last (append a b)) | |
433 | (if (listp b) | |
434 | (last b) | |
435 | (if (listp a) | |
436 | (cons (car (last a)) | |
437 | b) | |
438 | b))) | |
439 | (equal (equal (lessp x y) | |
440 | z) | |
441 | (if (lessp x y) | |
442 | (equal (t) z) | |
443 | (equal (f) z))) | |
444 | (equal (assignment x (append a b)) | |
445 | (if (assignedp x a) | |
446 | (assignment x a) | |
447 | (assignment x b))) | |
448 | (equal (car (gopher x)) | |
449 | (if (listp x) | |
450 | (car (flatten x)) | |
451 | (zero))) | |
452 | (equal (flatten (cdr (gopher x))) | |
453 | (if (listp x) | |
454 | (cdr (flatten x)) | |
455 | (cons (zero) | |
456 | (nil)))) | |
457 | (equal (quotient (times y x) | |
458 | y) | |
459 | (if (zerop y) | |
460 | (zero) | |
461 | (fix x))) | |
462 | (equal (get j (set i val mem)) | |
463 | (if (eqp j i) | |
464 | val | |
465 | (get j mem))))))) | |
466 | ||
467 | (define (add-lemma-lst lst) | |
468 | (cond ((null? lst) | |
469 | #t) | |
470 | (else (add-lemma (car lst)) | |
471 | (add-lemma-lst (cdr lst))))) | |
472 | ||
473 | (define (add-lemma term) | |
474 | (cond ((and (pair? term) | |
475 | (eq? (car term) | |
476 | (quote equal)) | |
477 | (pair? (cadr term))) | |
478 | (put (car (cadr term)) | |
479 | (quote lemmas) | |
480 | (cons | |
481 | (translate-term term) | |
482 | (get (car (cadr term)) (quote lemmas))))) | |
483 | (else (error "ADD-LEMMA did not like term: " term)))) | |
484 | ||
485 | ; Translates a term by replacing its constructor symbols by symbol-records. | |
486 | ||
487 | (define (translate-term term) | |
488 | (cond ((not (pair? term)) | |
489 | term) | |
490 | (else (cons (symbol->symbol-record (car term)) | |
491 | (translate-args (cdr term)))))) | |
492 | ||
493 | (define (translate-args lst) | |
494 | (cond ((null? lst) | |
495 | '()) | |
496 | (else (cons (translate-term (car lst)) | |
497 | (translate-args (cdr lst)))))) | |
498 | ||
499 | ; For debugging only, so the use of MAP does not change | |
500 | ; the first-order character of the benchmark. | |
501 | ||
502 | (define (untranslate-term term) | |
503 | (cond ((not (pair? term)) | |
504 | term) | |
505 | (else (cons (get-name (car term)) | |
506 | (map untranslate-term (cdr term)))))) | |
507 | ||
508 | ; A symbol-record is represented as a vector with two fields: | |
509 | ; the symbol (for debugging) and | |
510 | ; the list of lemmas associated with the symbol. | |
511 | ||
512 | (define (put sym property value) | |
513 | (put-lemmas! (symbol->symbol-record sym) value)) | |
514 | ||
515 | (define (get sym property) | |
516 | (get-lemmas (symbol->symbol-record sym))) | |
517 | ||
518 | (define (symbol->symbol-record sym) | |
519 | (let ((x (assq sym *symbol-records-alist*))) | |
520 | (if x | |
521 | (cdr x) | |
522 | (let ((r (make-symbol-record sym))) | |
523 | (set! *symbol-records-alist* | |
524 | (cons (cons sym r) | |
525 | *symbol-records-alist*)) | |
526 | r)))) | |
527 | ||
528 | ; Association list of symbols and symbol-records. | |
529 | ||
530 | (define *symbol-records-alist* '()) | |
531 | ||
532 | ; A symbol-record is represented as a vector with two fields: | |
533 | ; the symbol (for debugging) and | |
534 | ; the list of lemmas associated with the symbol. | |
535 | ||
536 | (define (make-symbol-record sym) | |
537 | (vector sym '())) | |
538 | ||
539 | (define (put-lemmas! symbol-record lemmas) | |
540 | (vector-set! symbol-record 1 lemmas)) | |
541 | ||
542 | (define (get-lemmas symbol-record) | |
543 | (vector-ref symbol-record 1)) | |
544 | ||
545 | (define (get-name symbol-record) | |
546 | (vector-ref symbol-record 0)) | |
547 | ||
548 | (define (symbol-record-equal? r1 r2) | |
549 | (eq? r1 r2)) | |
550 | ||
551 | ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; | |
552 | ; | |
553 | ; The second phase. | |
554 | ; | |
555 | ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; | |
556 | ||
557 | (define (test n) | |
558 | (let ((term | |
559 | (apply-subst | |
560 | (translate-alist | |
561 | (quote ((x f (plus (plus a b) | |
562 | (plus c (zero)))) | |
563 | (y f (times (times a b) | |
564 | (plus c d))) | |
565 | (z f (reverse (append (append a b) | |
566 | (nil)))) | |
567 | (u equal (plus a b) | |
568 | (difference x y)) | |
569 | (w lessp (remainder a b) | |
570 | (member a (length b)))))) | |
571 | (translate-term | |
572 | (do ((term | |
573 | (quote (implies (and (implies x y) | |
574 | (and (implies y z) | |
575 | (and (implies z u) | |
576 | (implies u w)))) | |
577 | (implies x w))) | |
578 | (list 'or term '(f))) | |
579 | (n n (- n 1))) | |
580 | ((zero? n) term)))))) | |
581 | (tautp term))) | |
582 | ||
583 | (define (translate-alist alist) | |
584 | (cond ((null? alist) | |
585 | '()) | |
586 | (else (cons (cons (caar alist) | |
587 | (translate-term (cdar alist))) | |
588 | (translate-alist (cdr alist)))))) | |
589 | ||
590 | (define (apply-subst alist term) | |
591 | (cond ((not (pair? term)) | |
592 | (let ((temp-temp (assq term alist))) | |
593 | (if temp-temp | |
594 | (cdr temp-temp) | |
595 | term))) | |
596 | (else (cons (car term) | |
597 | (apply-subst-lst alist (cdr term)))))) | |
598 | ||
599 | (define (apply-subst-lst alist lst) | |
600 | (cond ((null? lst) | |
601 | '()) | |
602 | (else (cons (apply-subst alist (car lst)) | |
603 | (apply-subst-lst alist (cdr lst)))))) | |
604 | ||
605 | (define (tautp x) | |
606 | (tautologyp (rewrite x) | |
607 | '() '())) | |
608 | ||
609 | (define (tautologyp x true-lst false-lst) | |
610 | (cond ((truep x true-lst) | |
611 | #t) | |
612 | ((falsep x false-lst) | |
613 | #f) | |
614 | ((not (pair? x)) | |
615 | #f) | |
616 | ((eq? (car x) if-constructor) | |
617 | (cond ((truep (cadr x) | |
618 | true-lst) | |
619 | (tautologyp (caddr x) | |
620 | true-lst false-lst)) | |
621 | ((falsep (cadr x) | |
622 | false-lst) | |
623 | (tautologyp (cadddr x) | |
624 | true-lst false-lst)) | |
625 | (else (and (tautologyp (caddr x) | |
626 | (cons (cadr x) | |
627 | true-lst) | |
628 | false-lst) | |
629 | (tautologyp (cadddr x) | |
630 | true-lst | |
631 | (cons (cadr x) | |
632 | false-lst)))))) | |
633 | (else #f))) | |
634 | ||
635 | (define if-constructor '*) ; becomes (symbol->symbol-record 'if) | |
636 | ||
637 | (define rewrite-count 0) ; sanity check | |
638 | ||
639 | ; The next procedure is Henry Baker's sharing CONS, which avoids | |
640 | ; allocation if the result is already in hand. | |
641 | ; The REWRITE and REWRITE-ARGS procedures have been modified to | |
642 | ; use SCONS instead of CONS. | |
643 | ||
644 | (define (scons x y original) | |
645 | (if (and (eq? x (car original)) | |
646 | (eq? y (cdr original))) | |
647 | original | |
648 | (cons x y))) | |
649 | ||
650 | (define (rewrite term) | |
651 | (set! rewrite-count (+ rewrite-count 1)) | |
652 | (cond ((not (pair? term)) | |
653 | term) | |
654 | (else (rewrite-with-lemmas (scons (car term) | |
655 | (rewrite-args (cdr term)) | |
656 | term) | |
657 | (get-lemmas (car term)))))) | |
658 | ||
659 | (define (rewrite-args lst) | |
660 | (cond ((null? lst) | |
661 | '()) | |
662 | (else (scons (rewrite (car lst)) | |
663 | (rewrite-args (cdr lst)) | |
664 | lst)))) | |
665 | ||
666 | (define (rewrite-with-lemmas term lst) | |
667 | (cond ((null? lst) | |
668 | term) | |
669 | ((one-way-unify term (cadr (car lst))) | |
670 | (rewrite (apply-subst unify-subst (caddr (car lst))))) | |
671 | (else (rewrite-with-lemmas term (cdr lst))))) | |
672 | ||
673 | (define unify-subst '*) | |
674 | ||
675 | (define (one-way-unify term1 term2) | |
676 | (begin (set! unify-subst '()) | |
677 | (one-way-unify1 term1 term2))) | |
678 | ||
679 | (define (one-way-unify1 term1 term2) | |
680 | (cond ((not (pair? term2)) | |
681 | (let ((temp-temp (assq term2 unify-subst))) | |
682 | (cond (temp-temp | |
683 | (term-equal? term1 (cdr temp-temp))) | |
684 | ((number? term2) ; This bug fix makes | |
685 | (equal? term1 term2)) ; nboyer 10-25% slower! | |
686 | (else | |
687 | (set! unify-subst (cons (cons term2 term1) | |
688 | unify-subst)) | |
689 | #t)))) | |
690 | ((not (pair? term1)) | |
691 | #f) | |
692 | ((eq? (car term1) | |
693 | (car term2)) | |
694 | (one-way-unify1-lst (cdr term1) | |
695 | (cdr term2))) | |
696 | (else #f))) | |
697 | ||
698 | (define (one-way-unify1-lst lst1 lst2) | |
699 | (cond ((null? lst1) | |
700 | (null? lst2)) | |
701 | ((null? lst2) | |
702 | #f) | |
703 | ((one-way-unify1 (car lst1) | |
704 | (car lst2)) | |
705 | (one-way-unify1-lst (cdr lst1) | |
706 | (cdr lst2))) | |
707 | (else #f))) | |
708 | ||
709 | (define (falsep x lst) | |
710 | (or (term-equal? x false-term) | |
711 | (term-member? x lst))) | |
712 | ||
713 | (define (truep x lst) | |
714 | (or (term-equal? x true-term) | |
715 | (term-member? x lst))) | |
716 | ||
717 | (define false-term '*) ; becomes (translate-term '(f)) | |
718 | (define true-term '*) ; becomes (translate-term '(t)) | |
719 | ||
720 | ; The next two procedures were in the original benchmark | |
721 | ; but were never used. | |
722 | ||
723 | (define (trans-of-implies n) | |
724 | (translate-term | |
725 | (list (quote implies) | |
726 | (trans-of-implies1 n) | |
727 | (list (quote implies) | |
728 | 0 n)))) | |
729 | ||
730 | (define (trans-of-implies1 n) | |
731 | (cond ((equal? n 1) | |
732 | (list (quote implies) | |
733 | 0 1)) | |
734 | (else (list (quote and) | |
735 | (list (quote implies) | |
736 | (- n 1) | |
737 | n) | |
738 | (trans-of-implies1 (- n 1)))))) | |
739 | ||
740 | ; Translated terms can be circular structures, which can't be | |
741 | ; compared using Scheme's equal? and member procedures, so we | |
742 | ; use these instead. | |
743 | ||
744 | (define (term-equal? x y) | |
745 | (cond ((pair? x) | |
746 | (and (pair? y) | |
747 | (symbol-record-equal? (car x) (car y)) | |
748 | (term-args-equal? (cdr x) (cdr y)))) | |
749 | (else (equal? x y)))) | |
750 | ||
751 | (define (term-args-equal? lst1 lst2) | |
752 | (cond ((null? lst1) | |
753 | (null? lst2)) | |
754 | ((null? lst2) | |
755 | #f) | |
756 | ((term-equal? (car lst1) (car lst2)) | |
757 | (term-args-equal? (cdr lst1) (cdr lst2))) | |
758 | (else #f))) | |
759 | ||
760 | (define (term-member? x lst) | |
761 | (cond ((null? lst) | |
762 | #f) | |
763 | ((term-equal? x (car lst)) | |
764 | #t) | |
765 | (else (term-member? x (cdr lst))))) | |
766 | ||
767 | (set! setup-boyer | |
768 | (lambda () | |
769 | (set! *symbol-records-alist* '()) | |
770 | (set! if-constructor (symbol->symbol-record 'if)) | |
771 | (set! false-term (translate-term '(f))) | |
772 | (set! true-term (translate-term '(t))) | |
773 | (setup))) | |
774 | ||
775 | (set! test-boyer | |
776 | (lambda (n) | |
777 | (set! rewrite-count 0) | |
778 | (let ((answer (test n))) | |
779 | (write rewrite-count) | |
780 | (display " rewrites") | |
781 | (newline) | |
782 | (if answer | |
783 | rewrite-count | |
784 | #f))))) |