gc-benchmarks/larceny/sboyer.sch

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