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