1 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
3 ; Description: The Boyer benchmark
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)
15 ; Status: Public Domain
16 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
18 ;;; NBOYER -- Logic programming benchmark, originally written by Bob Boyer.
19 ;;; Fairly CONS intensive.
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:
26 ; The benchmark now returns a boolean result.
27 ; FALSEP and TRUEP use TERM-MEMBER? rather than MEMV (which is called MEMBER
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
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.
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
44 ; n rewrites peak live storage (approximate, in bytes)
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.
58 (define (nboyer-benchmark . args)
59 (let ((n (if (null? args) 0 (car args))))
61 (run-benchmark (string-append "nboyer"
64 (lambda () (test-boyer n))
66 (and (number? rewrites)
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.
77 (define (setup-boyer) #t) ; assigned below
78 (define (test-boyer) #t) ; assigned below
80 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
84 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
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.
96 (quote ((equal (compile form)
97 (reverse (codegen (optimize form)
102 (equal (greaterp x y)
106 (equal (greatereqp x y)
118 (equal (countps- l pred)
119 (countps-loop l pred (zero)))
123 (reverse-loop x (nil)))
125 (zerop (remainder y x)))
126 (equal (assume-true var alist)
129 (equal (assume-false var alist)
132 (equal (tautology-checker x)
133 (tautologyp (normalize x)
136 (falsify1 (normalize x)
140 (not (equal x (add1 (zero))))
141 (prime1 x (sub1 x))))
161 (equal (if (if a b c)
168 (equal (plus (plus x y)
171 (equal (equal (plus a b)
175 (equal (difference x x)
177 (equal (equal (plus a b)
184 (equal (equal x (difference x y))
188 (equal (meaning (plus-tree (append x y))
190 (plus (meaning (plus-tree x)
192 (meaning (plus-tree y)
194 (equal (meaning (plus-tree (plus-fringe x))
197 (equal (append (append x y)
199 (append x (append y z)))
200 (equal (reverse (append a b))
203 (equal (times x (plus y z))
206 (equal (times (times x y)
208 (times x (times y z)))
209 (equal (equal (times x y)
213 (equal (exec (append x y)
215 (exec y (exec x pds envrn)
217 (equal (mc-flatten x y)
220 (equal (member x (append a b))
223 (equal (member x (reverse y))
225 (equal (length (reverse x))
227 (equal (member a (intersect b c))
233 (equal (exp i (plus j k))
236 (equal (exp i (times j k))
239 (equal (reverse-loop x y)
242 (equal (reverse-loop x (nil))
244 (equal (count-list z (sort-lp x y))
245 (plus (count-list z x)
247 (equal (equal (append a b)
250 (equal (plus (remainder x y)
251 (times y (quotient x y)))
253 (equal (power-eval (big-plus1 l i base)
255 (plus (power-eval l base)
257 (equal (power-eval (big-plus x y i base)
259 (plus i (plus (power-eval x base)
260 (power-eval y base))))
261 (equal (remainder y 1)
263 (equal (lessp (remainder x y)
266 (equal (remainder x x)
268 (equal (lessp (quotient i j)
273 (equal (lessp (remainder x y)
278 (equal (power-eval (power-rep i base)
281 (equal (power-eval (big-plus (power-rep i base)
289 (equal (nth (append a b)
292 (nth b (difference i (length a)))))
293 (equal (difference (plus x y)
296 (equal (difference (plus y x)
299 (equal (difference (plus x y)
302 (equal (times x (difference c w))
303 (difference (times c x)
305 (equal (remainder (times x z)
308 (equal (difference (plus b (plus a c))
311 (equal (difference (add1 (plus y z))
314 (equal (lessp (plus x y)
317 (equal (lessp (times x z)
321 (equal (lessp y (plus x y))
323 (equal (gcd (times x z)
326 (equal (value (normalize x)
329 (equal (equal (flatten x)
333 (equal (listp (gopher x))
335 (equal (samefringe x y)
338 (equal (equal (greatest-factor x y)
343 (equal (equal (greatest-factor x y)
346 (equal (numberp (greatest-factor x y))
347 (not (and (or (zerop y)
350 (equal (times-list (append x y))
351 (times (times-list x)
353 (equal (prime-list (append x y))
356 (equal (equal z (times w z))
360 (equal (greatereqp x y)
362 (equal (equal x (times x y))
366 (equal (remainder (times y x)
369 (equal (equal (times a b)
371 (and (not (equal a (zero)))
372 (not (equal b (zero)))
379 (equal (lessp (length (delete x l))
382 (equal (sort2 (delete x l))
383 (delete x (sort2 l)))
386 (equal (length (cons x1
391 (plus 6 (length x7)))
392 (equal (difference (add1 (add1 x))
395 (equal (quotient (plus x (plus x y))
397 (plus x (quotient y 2)))
400 (quotient (times i (add1 i))
402 (equal (plus x (add1 y))
406 (equal (equal (difference x y)
414 (equal (meaning (plus-tree (delete x y))
417 (difference (meaning (plus-tree y)
420 (meaning (plus-tree y)
422 (equal (times x (add1 y))
431 (equal (last (append a b))
438 (equal (equal (lessp x y)
443 (equal (assignment x (append a b))
447 (equal (car (gopher x))
451 (equal (flatten (cdr (gopher x)))
456 (equal (quotient (times y x)
461 (equal (get j (set i val mem))
466 (define (add-lemma-lst lst)
469 (else (add-lemma (car lst))
470 (add-lemma-lst (cdr lst)))))
472 (define (add-lemma term)
473 (cond ((and (pair? term)
477 (put (car (cadr term))
480 (translate-term term)
481 (get (car (cadr term)) (quote lemmas)))))
482 (else (error "ADD-LEMMA did not like term: " term))))
484 ; Translates a term by replacing its constructor symbols by symbol-records.
486 (define (translate-term term)
487 (cond ((not (pair? term))
489 (else (cons (symbol->symbol-record (car term))
490 (translate-args (cdr term))))))
492 (define (translate-args lst)
495 (else (cons (translate-term (car lst))
496 (translate-args (cdr lst))))))
498 ; For debugging only, so the use of MAP does not change
499 ; the first-order character of the benchmark.
501 (define (untranslate-term term)
502 (cond ((not (pair? term))
504 (else (cons (get-name (car term))
505 (map untranslate-term (cdr term))))))
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.
511 (define (put sym property value)
512 (put-lemmas! (symbol->symbol-record sym) value))
514 (define (get sym property)
515 (get-lemmas (symbol->symbol-record sym)))
517 (define (symbol->symbol-record sym)
518 (let ((x (assq sym *symbol-records-alist*)))
521 (let ((r (make-symbol-record sym)))
522 (set! *symbol-records-alist*
524 *symbol-records-alist*))
527 ; Association list of symbols and symbol-records.
529 (define *symbol-records-alist* '())
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.
535 (define (make-symbol-record sym)
538 (define (put-lemmas! symbol-record lemmas)
539 (vector-set! symbol-record 1 lemmas))
541 (define (get-lemmas symbol-record)
542 (vector-ref symbol-record 1))
544 (define (get-name symbol-record)
545 (vector-ref symbol-record 0))
547 (define (symbol-record-equal? r1 r2)
550 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
554 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
560 (quote ((x f (plus (plus a b)
562 (y f (times (times a b)
564 (z f (reverse (append (append a b)
568 (w lessp (remainder a b)
569 (member a (length b))))))
572 (quote (implies (and (implies x y)
577 (list 'or term '(f)))
579 ((zero? n) term))))))
582 (define (translate-alist alist)
585 (else (cons (cons (caar alist)
586 (translate-term (cdar alist)))
587 (translate-alist (cdr alist))))))
589 (define (apply-subst alist term)
590 (cond ((not (pair? term))
591 (let ((temp-temp (assq term alist)))
595 (else (cons (car term)
596 (apply-subst-lst alist (cdr term))))))
598 (define (apply-subst-lst alist lst)
601 (else (cons (apply-subst alist (car lst))
602 (apply-subst-lst alist (cdr lst))))))
605 (tautologyp (rewrite x)
608 (define (tautologyp x true-lst false-lst)
609 (cond ((truep x true-lst)
611 ((falsep x false-lst)
615 ((eq? (car x) if-constructor)
616 (cond ((truep (cadr x)
618 (tautologyp (caddr x)
622 (tautologyp (cadddr x)
624 (else (and (tautologyp (caddr x)
628 (tautologyp (cadddr x)
634 (define if-constructor '*) ; becomes (symbol->symbol-record 'if)
636 (define rewrite-count 0) ; sanity check
638 (define (rewrite term)
639 (set! rewrite-count (+ rewrite-count 1))
640 (cond ((not (pair? term))
642 (else (rewrite-with-lemmas (cons (car term)
643 (rewrite-args (cdr term)))
644 (get-lemmas (car term))))))
646 (define (rewrite-args lst)
649 (else (cons (rewrite (car lst))
650 (rewrite-args (cdr lst))))))
652 (define (rewrite-with-lemmas term lst)
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)))))
659 (define unify-subst '*)
661 (define (one-way-unify term1 term2)
662 (begin (set! unify-subst '())
663 (one-way-unify1 term1 term2)))
665 (define (one-way-unify1 term1 term2)
666 (cond ((not (pair? term2))
667 (let ((temp-temp (assq term2 unify-subst)))
669 (term-equal? term1 (cdr temp-temp)))
670 ((number? term2) ; This bug fix makes
671 (equal? term1 term2)) ; nboyer 10-25% slower!
673 (set! unify-subst (cons (cons term2 term1)
680 (one-way-unify1-lst (cdr term1)
684 (define (one-way-unify1-lst lst1 lst2)
689 ((one-way-unify1 (car lst1)
691 (one-way-unify1-lst (cdr lst1)
695 (define (falsep x lst)
696 (or (term-equal? x false-term)
697 (term-member? x lst)))
699 (define (truep x lst)
700 (or (term-equal? x true-term)
701 (term-member? x lst)))
703 (define false-term '*) ; becomes (translate-term '(f))
704 (define true-term '*) ; becomes (translate-term '(t))
706 ; The next two procedures were in the original benchmark
707 ; but were never used.
709 (define (trans-of-implies n)
711 (list (quote implies)
712 (trans-of-implies1 n)
713 (list (quote implies)
716 (define (trans-of-implies1 n)
718 (list (quote implies)
720 (else (list (quote and)
721 (list (quote implies)
724 (trans-of-implies1 (- n 1))))))
726 ; Translated terms can be circular structures, which can't be
727 ; compared using Scheme's equal? and member procedures, so we
730 (define (term-equal? x y)
733 (symbol-record-equal? (car x) (car y))
734 (term-args-equal? (cdr x) (cdr y))))
735 (else (equal? x y))))
737 (define (term-args-equal? lst1 lst2)
742 ((term-equal? (car lst1) (car lst2))
743 (term-args-equal? (cdr lst1) (cdr lst2)))
746 (define (term-member? x lst)
749 ((term-equal? x (car lst))
751 (else (term-member? x (cdr lst)))))
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)))
763 (set! rewrite-count 0)
764 (let ((answer (test n)))
765 (write rewrite-count)
766 (display " rewrites")