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