gc-benchmarks/larceny/nboyer.sch

   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)))))