home *** CD-ROM | disk | FTP | other *** search
/ Usenet 1994 January / usenetsourcesnewsgroupsinfomagicjanuary1994.iso / sources / misc / volume1 / 8707 / 49 / boyer.cl next >
Encoding:
Text File  |  1990-07-13  |  12.9 KB  |  559 lines
  1. ;From: ihnp4!utah-cs!shebs@utah-cs.UTAH-CS (Stanley Shebs)
  2. ;Organization: University of Utah, Salt Lake City
  3.  
  4. ;BTW, we have complete sets for PSL and Common Lisp that I can probably
  5. ;shar together and send.  The code below is basically what's in Gabriel's
  6. ;book, but the PSL version bears less resemblance (different dialect):
  7.  
  8. ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
  9. ; File:         boyer.cl
  10. ; Description:  The Boyer benchmark
  11. ; Author:       Bob Boyer
  12. ; Created:      5-Apr-85
  13. ; Modified:     10-Apr-85 14:52:20 (Bob Shaw)
  14. ; Language:     Common Lisp
  15. ; Package:      User
  16. ; Status:       Public Domain
  17. ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
  18.  
  19. ;;; BOYER -- Logic programming benchmark, originally written by Bob Boyer.
  20. ;;; Fairly CONS intensive.
  21.  
  22. (defvar unify-subst)
  23. (defvar temp-temp)
  24.  
  25. (defun add-lemma (term)
  26.   (cond ((and (not (atom term))
  27.           (eq (car term)
  28.           (quote equal))
  29.           (not (atom (cadr term))))
  30.      (setf (get (car (cadr term)) (quote lemmas))
  31.            (cons term (get (car (cadr term)) (quote lemmas)))))
  32.     (t (error "~%ADD-LEMMA did not like term:  ~a" term))))
  33.  
  34. (defun add-lemma-lst (lst)
  35.   (cond ((null lst)
  36.      t)
  37.     (t (add-lemma (car lst))
  38.        (add-lemma-lst (cdr lst)))))
  39.  
  40. (defun apply-subst (alist term)
  41.   (cond ((atom term)
  42.      (cond ((setq temp-temp (assoc term alist :test #'eq))
  43.         (cdr temp-temp))
  44.            (t term)))
  45.     (t (cons (car term)
  46.          (apply-subst-lst alist (cdr term))))))
  47.  
  48. (defun apply-subst-lst (alist lst)
  49.   (cond ((null lst)
  50.      nil)
  51.     (t (cons (apply-subst alist (car lst))
  52.          (apply-subst-lst alist (cdr lst))))))
  53.  
  54. (defun falsep (x lst)
  55.   (or (equal x (quote (f)))
  56.       (member x lst)))
  57.  
  58. (defun one-way-unify (term1 term2)
  59.   (progn (setq unify-subst nil)
  60.      (one-way-unify1 term1 term2)))
  61.  
  62. (defun one-way-unify1 (term1 term2)
  63.   (cond ((atom term2)
  64.      (cond ((setq temp-temp (assoc term2 unify-subst :test #'eq))
  65.         (equal term1 (cdr temp-temp)))
  66.            (t (setq unify-subst (cons (cons term2 term1)
  67.                       unify-subst))
  68.           t)))
  69.     ((atom term1)
  70.      nil)
  71.     ((eq (car term1)
  72.          (car term2))
  73.      (one-way-unify1-lst (cdr term1)
  74.                  (cdr term2)))
  75.     (t nil)))
  76.  
  77. (defun one-way-unify1-lst (lst1 lst2)
  78.   (cond ((null lst1)
  79.      t)
  80.     ((one-way-unify1 (car lst1)
  81.              (car lst2))
  82.      (one-way-unify1-lst (cdr lst1)
  83.                  (cdr lst2)))
  84.     (t nil)))
  85.  
  86. (defun rewrite (term)
  87.   (cond ((atom term)
  88.      term)
  89.     (t (rewrite-with-lemmas (cons (car term)
  90.                       (rewrite-args (cdr term)))
  91.                 (get (car term)
  92.                      (quote lemmas))))))
  93.  
  94. (defun rewrite-args (lst)
  95.   (cond ((null lst)
  96.      nil)
  97.     (t (cons (rewrite (car lst))
  98.          (rewrite-args (cdr lst))))))
  99.  
  100. (defun rewrite-with-lemmas (term lst)
  101.   (cond ((null lst)
  102.      term)
  103.     ((one-way-unify term (cadr (car lst)))
  104.      (rewrite (apply-subst unify-subst (caddr (car lst)))))
  105.     (t (rewrite-with-lemmas term (cdr lst)))))
  106.  
  107. (defun setup ()
  108.   (add-lemma-lst
  109.     (quote ((equal (compile form)
  110.            (reverse (codegen (optimize form)
  111.                      (nil))))
  112.         (equal (eqp x y)
  113.            (equal (fix x)
  114.               (fix y)))
  115.         (equal (greaterp x y)
  116.            (lessp y x))
  117.         (equal (lesseqp x y)
  118.            (not (lessp y x)))
  119.         (equal (greatereqp x y)
  120.            (not (lessp x y)))
  121.         (equal (boolean x)
  122.            (or (equal x (t))
  123.                (equal x (f))))
  124.         (equal (iff x y)
  125.            (and (implies x y)
  126.             (implies y x)))
  127.         (equal (even1 x)
  128.            (if (zerop x)
  129.                (t)
  130.                (odd (1- x))))
  131.         (equal (countps- l pred)
  132.            (countps-loop l pred (zero)))
  133.         (equal (fact- i)
  134.            (fact-loop i 1))
  135.         (equal (reverse- x)
  136.            (reverse-loop x (nil)))
  137.         (equal (divides x y)
  138.            (zerop (remainder y x)))
  139.         (equal (assume-true var alist)
  140.            (cons (cons var (t))
  141.              alist))
  142.         (equal (assume-false var alist)
  143.            (cons (cons var (f))
  144.              alist))
  145.         (equal (tautology-checker x)
  146.            (tautologyp (normalize x)
  147.                    (nil)))
  148.         (equal (falsify x)
  149.            (falsify1 (normalize x)
  150.                  (nil)))
  151.         (equal (prime x)
  152.            (and (not (zerop x))
  153.             (not (equal x (add1 (zero))))
  154.             (prime1 x (1- x))))
  155.         (equal (and p q)
  156.            (if p (if q (t)
  157.                  (f))
  158.                (f)))
  159.         (equal (or p q)
  160.            (if p (t)
  161.                (if q (t)
  162.                (f))
  163.                (f)))
  164.         (equal (not p)
  165.            (if p (f)
  166.                (t)))
  167.         (equal (implies p q)
  168.            (if p (if q (t)
  169.                  (f))
  170.                (t)))
  171.         (equal (fix x)
  172.            (if (numberp x)
  173.                x
  174.                (zero)))
  175.         (equal (if (if a b c)
  176.                d e)
  177.            (if a (if b d e)
  178.                (if c d e)))
  179.         (equal (zerop x)
  180.            (or (equal x (zero))
  181.                (not (numberp x))))
  182.         (equal (plus (plus x y)
  183.              z)
  184.            (plus x (plus y z)))
  185.         (equal (equal (plus a b)
  186.               (zero))
  187.            (and (zerop a)
  188.             (zerop b)))
  189.         (equal (difference x x)
  190.            (zero))
  191.         (equal (equal (plus a b)
  192.               (plus a c))
  193.            (equal (fix b)
  194.               (fix c)))
  195.         (equal (equal (zero)
  196.               (difference x y))
  197.            (not (lessp y x)))
  198.         (equal (equal x (difference x y))
  199.            (and (numberp x)
  200.             (or (equal x (zero))
  201.                 (zerop y))))
  202.         (equal (meaning (plus-tree (append x y))
  203.                 a)
  204.            (plus (meaning (plus-tree x)
  205.                   a)
  206.              (meaning (plus-tree y)
  207.                   a)))
  208.         (equal (meaning (plus-tree (plus-fringe x))
  209.                 a)
  210.            (fix (meaning x a)))
  211.         (equal (append (append x y)
  212.                z)
  213.            (append x (append y z)))
  214.         (equal (reverse (append a b))
  215.            (append (reverse b)
  216.                (reverse a)))
  217.         (equal (times x (plus y z))
  218.            (plus (times x y)
  219.              (times x z)))
  220.         (equal (times (times x y)
  221.               z)
  222.            (times x (times y z)))
  223.         (equal (equal (times x y)
  224.               (zero))
  225.            (or (zerop x)
  226.                (zerop y)))
  227.         (equal (exec (append x y)
  228.              pds envrn)
  229.            (exec y (exec x pds envrn)
  230.              envrn))
  231.         (equal (mc-flatten x y)
  232.            (append (flatten x)
  233.                y))
  234.         (equal (member x (append a b))
  235.            (or (member x a)
  236.                (member x b)))
  237.         (equal (member x (reverse y))
  238.            (member x y))
  239.         (equal (length (reverse x))
  240.            (length x))
  241.         (equal (member a (intersect b c))
  242.            (and (member a b)
  243.             (member a c)))
  244.         (equal (nth (zero)
  245.             i)
  246.            (zero))
  247.         (equal (exp i (plus j k))
  248.            (times (exp i j)
  249.               (exp i k)))
  250.         (equal (exp i (times j k))
  251.            (exp (exp i j)
  252.             k))
  253.         (equal (reverse-loop x y)
  254.            (append (reverse x)
  255.                y))
  256.         (equal (reverse-loop x (nil))
  257.            (reverse x))
  258.         (equal (count-list z (sort-lp x y))
  259.            (plus (count-list z x)
  260.              (count-list z y)))
  261.         (equal (equal (append a b)
  262.               (append a c))
  263.            (equal b c))
  264.         (equal (plus (remainder x y)
  265.              (times y (quotient x y)))
  266.            (fix x))
  267.         (equal (power-eval (big-plus1 l i base)
  268.                    base)
  269.            (plus (power-eval l base)
  270.              i))
  271.         (equal (power-eval (big-plus x y i base)
  272.                    base)
  273.            (plus i (plus (power-eval x base)
  274.                  (power-eval y base))))
  275.         (equal (remainder y 1)
  276.            (zero))
  277.         (equal (lessp (remainder x y)
  278.               y)
  279.            (not (zerop y)))
  280.         (equal (remainder x x)
  281.            (zero))
  282.         (equal (lessp (quotient i j)
  283.               i)
  284.            (and (not (zerop i))
  285.             (or (zerop j)
  286.                 (not (equal j 1)))))
  287.         (equal (lessp (remainder x y)
  288.               x)
  289.            (and (not (zerop y))
  290.             (not (zerop x))
  291.             (not (lessp x y))))
  292.         (equal (power-eval (power-rep i base)
  293.                    base)
  294.            (fix i))
  295.         (equal (power-eval (big-plus (power-rep i base)
  296.                      (power-rep j base)
  297.                      (zero)
  298.                      base)
  299.                    base)
  300.            (plus i j))
  301.         (equal (gcd x y)
  302.            (gcd y x))
  303.         (equal (nth (append a b)
  304.             i)
  305.            (append (nth a i)
  306.                (nth b (difference i (length a)))))
  307.         (equal (difference (plus x y)
  308.                    x)
  309.            (fix y))
  310.         (equal (difference (plus y x)
  311.                    x)
  312.            (fix y))
  313.         (equal (difference (plus x y)
  314.                    (plus x z))
  315.            (difference y z))
  316.         (equal (times x (difference c w))
  317.            (difference (times c x)
  318.                    (times w x)))
  319.         (equal (remainder (times x z)
  320.                   z)
  321.            (zero))
  322.         (equal (difference (plus b (plus a c))
  323.                    a)
  324.            (plus b c))
  325.         (equal (difference (add1 (plus y z))
  326.                    z)
  327.            (add1 y))
  328.         (equal (lessp (plus x y)
  329.               (plus x z))
  330.            (lessp y z))
  331.         (equal (lessp (times x z)
  332.               (times y z))
  333.            (and (not (zerop z))
  334.             (lessp x y)))
  335.         (equal (lessp y (plus x y))
  336.            (not (zerop x)))
  337.         (equal (gcd (times x z)
  338.             (times y z))
  339.            (times z (gcd x y)))
  340.         (equal (value (normalize x)
  341.               a)
  342.            (value x a))
  343.         (equal (equal (flatten x)
  344.               (cons y (nil)))
  345.            (and (nlistp x)
  346.             (equal x y)))
  347.         (equal (listp (gopher x))
  348.            (listp x))
  349.         (equal (samefringe x y)
  350.            (equal (flatten x)
  351.               (flatten y)))
  352.         (equal (equal (greatest-factor x y)
  353.               (zero))
  354.            (and (or (zerop y)
  355.                 (equal y 1))
  356.             (equal x (zero))))
  357.         (equal (equal (greatest-factor x y)
  358.               1)
  359.            (equal x 1))
  360.         (equal (numberp (greatest-factor x y))
  361.            (not (and (or (zerop y)
  362.                  (equal y 1))
  363.                  (not (numberp x)))))
  364.         (equal (times-list (append x y))
  365.            (times (times-list x)
  366.               (times-list y)))
  367.         (equal (prime-list (append x y))
  368.            (and (prime-list x)
  369.             (prime-list y)))
  370.         (equal (equal z (times w z))
  371.            (and (numberp z)
  372.             (or (equal z (zero))
  373.                 (equal w 1))))
  374.         (equal (greatereqpr x y)
  375.            (not (lessp x y)))
  376.         (equal (equal x (times x y))
  377.            (or (equal x (zero))
  378.                (and (numberp x)
  379.                 (equal y 1))))
  380.         (equal (remainder (times y x)
  381.                   y)
  382.            (zero))
  383.         (equal (equal (times a b)
  384.               1)
  385.            (and (not (equal a (zero)))
  386.             (not (equal b (zero)))
  387.             (numberp a)
  388.             (numberp b)
  389.             (equal (1- a)
  390.                    (zero))
  391.             (equal (1- b)
  392.                    (zero))))
  393.         (equal (lessp (length (delete x l))
  394.               (length l))
  395.            (member x l))
  396.         (equal (sort2 (delete x l))
  397.            (delete x (sort2 l)))
  398.         (equal (dsort x)
  399.            (sort2 x))
  400.         (equal (length (cons x1
  401.                  (cons x2
  402.                        (cons x3 (cons x4
  403.                               (cons x5
  404.                                 (cons x6 x7)))))))
  405.            (plus 6 (length x7)))
  406.         (equal (difference (add1 (add1 x))
  407.                    2)
  408.            (fix x))
  409.         (equal (quotient (plus x (plus x y))
  410.                  2)
  411.            (plus x (quotient y 2)))
  412.         (equal (sigma (zero)
  413.               i)
  414.            (quotient (times i (add1 i))
  415.                  2))
  416.         (equal (plus x (add1 y))
  417.            (if (numberp y)
  418.                (add1 (plus x y))
  419.                (add1 x)))
  420.         (equal (equal (difference x y)
  421.               (difference z y))
  422.            (if (lessp x y)
  423.                (not (lessp y z))
  424.                (if (lessp z y)
  425.                (not (lessp y x))
  426.                (equal (fix x)
  427.                   (fix z)))))
  428.         (equal (meaning (plus-tree (delete x y))
  429.                 a)
  430.            (if (member x y)
  431.                (difference (meaning (plus-tree y)
  432.                         a)
  433.                    (meaning x a))
  434.                (meaning (plus-tree y)
  435.                 a)))
  436.         (equal (times x (add1 y))
  437.            (if (numberp y)
  438.                (plus x (times x y))
  439.                (fix x)))
  440.         (equal (nth (nil)
  441.             i)
  442.            (if (zerop i)
  443.                (nil)
  444.                (zero)))
  445.         (equal (last (append a b))
  446.            (if (listp b)
  447.                (last b)
  448.                (if (listp a)
  449.                (cons (car (last a))
  450.                  b)
  451.                b)))
  452.         (equal (equal (lessp x y)
  453.               z)
  454.            (if (lessp x y)
  455.                (equal t z)
  456.                (equal f z)))
  457.         (equal (assignment x (append a b))
  458.            (if (assignedp x a)
  459.                (assignment x a)
  460.                (assignment x b)))
  461.         (equal (car (gopher x))
  462.            (if (listp x)
  463.                (car (flatten x))
  464.                (zero)))
  465.         (equal (flatten (cdr (gopher x)))
  466.            (if (listp x)
  467.                (cdr (flatten x))
  468.                (cons (zero)
  469.                  (nil))))
  470.         (equal (quotient (times y x)
  471.                  y)
  472.            (if (zerop y)
  473.                (zero)
  474.                (fix x)))
  475.         (equal (get j (set i val mem))
  476.            (if (eqp j i)
  477.                val
  478.                (get j mem)))))))
  479.  
  480. (defun tautologyp (x true-lst false-lst)
  481.   (cond ((truep x true-lst)
  482.      t)
  483.     ((falsep x false-lst)
  484.      nil)
  485.     ((atom x)
  486.      nil)
  487.     ((eq (car x)
  488.          (quote if))
  489.      (cond ((truep (cadr x)
  490.                true-lst)
  491.         (tautologyp (caddr x)
  492.                 true-lst false-lst))
  493.            ((falsep (cadr x)
  494.             false-lst)
  495.         (tautologyp (cadddr x)
  496.                 true-lst false-lst))
  497.            (t (and (tautologyp (caddr x)
  498.                    (cons (cadr x)
  499.                      true-lst)
  500.                    false-lst)
  501.                (tautologyp (cadddr x)
  502.                    true-lst
  503.                    (cons (cadr x)
  504.                      false-lst))))))
  505.     (t nil)))
  506.  
  507. (defun tautp (x)
  508.   (tautologyp (rewrite x)
  509.           nil nil))
  510.  
  511. (defun test ()
  512.   (prog (ans term)
  513.     (setq term
  514.           (apply-subst
  515.         (quote ((x f (plus (plus a b)
  516.                    (plus c (zero))))
  517.             (y f (times (times a b)
  518.                     (plus c d)))
  519.             (z f (reverse (append (append a b)
  520.                           (nil))))
  521.             (u equal (plus a b)
  522.                (difference x y))
  523.             (w lessp (remainder a b)
  524.                (member a (length b)))))
  525.         (quote (implies (and (implies x y)
  526.                      (and (implies y z)
  527.                       (and (implies z u)
  528.                            (implies u w))))
  529.                 (implies x w)))))
  530.     (setq ans (tautp term))))
  531.  
  532. (defun trans-of-implies (n)
  533.   (list (quote implies)
  534.     (trans-of-implies1 n)
  535.     (list (quote implies)
  536.           0 n)))
  537.  
  538. (defun trans-of-implies1 (n)
  539.   (cond ((equal n 1)            ; I think (eql n 1) may work here
  540.      (list (quote implies)
  541.            0 1))
  542.     (t (list (quote and)
  543.          (list (quote implies)
  544.                (1- n)
  545.                n)
  546.          (trans-of-implies1 (1- n))))))
  547.  
  548. (defun truep (x lst)
  549.        (or (equal x (quote (t)))
  550.        (member x lst)))
  551.  
  552. (eval-when (load eval)
  553.   (setup))
  554.  
  555. ;;; make sure you've run (setup) then call:  (test)
  556.  
  557. (run-benchmark "Boyer" '(test))
  558.  
  559.