/usr/share/acl2-6.3/books/misc/hons-tests.lisp is in acl2-books-source 6.3-5.
This file is owned by root:root, with mode 0o644.
The actual contents of the file can be viewed below.
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 | (in-package "ACL2")
; Courtesy of Bob Boyer and Warren Hunt:
(include-book "qi")
(defun fib (x)
(declare (xargs :guard (and (integerp x)
(<= 0 x))))
(mbe
:logic
(cond ((zp x) 0)
((= x 1) 1)
(t (+ (fib (- x 1)) (fib (- x 2)))))
:exec
(if (< x 2)
x
(+ (fib (- x 1)) (fib (- x 2))))))
#+hons
(memoize 'fib)
#+hons
(defthm fib-test0
; SBCL 1.03 has given the following error for fib-test, below, when not
; including fib-test0 first:
; Error: Control stack exhausted (no more space for function call frames).
; Since fib is not tail-recursive, the problem presumably is that even with
; memoization, we need a control stack of size about 10000 for fib-test. By
; putting fib-test0 first, we presumably stay within SBCL's stack size limit.
(equal (integer-length (fib 5000)) 3471))
#+hons
(defthm fib-test
(equal (integer-length (fib 10000)) 6942))
(defn tree-depth (x)
; This is the same as max-depth, but we want to
; hack with it so we give it another name.
(if (atom x)
0
(1+ (max (tree-depth (car x))
(tree-depth (cdr x))))))
(defun build-tree (n)
(declare (xargs :guard t))
(if (posp n)
(hons (build-tree (1- n)) (build-tree (1- n)))
nil))
#+hons
(memoize 'build-tree)
#+hons
(memoize 'tree-depth)
#+hons
(defthm build-tree-test
(let ((n 1000))
(equal (tree-depth (build-tree n)) n)))
(defn make-list-of-numbers (n)
(declare (xargs :guard (natp n)))
(if (zp n)
(list n)
(hons n (make-list-of-numbers (1- n)))))
(comp 'make-list-of-numbers)
(defun lots (n)
(declare (xargs :guard (posp n)))
(let* ((lots-of-numbers (make-list-of-numbers n)))
(equal (+ (len (hons-intersection lots-of-numbers
lots-of-numbers))
(len (hons-union lots-of-numbers
lots-of-numbers))
(len (hons-set-diff lots-of-numbers
lots-of-numbers)))
(+ 2 (* 2 n)))))
(defthm lots-thm (lots 6000))
#+hons
(memoize 'q-ite :condition '(and (consp x) (or (consp y) (consp z))))
#+hons
(memoize 'qnorm1)
#+hons
(memoize 'qvar-n)
(defn lfoo (x) (if (atom x) 0 (+ 1 (lfoo (cdr x)))))
#+hons
(memoize 'lfoo :trace 'notinline)
(defthm l-thm (equal (lfoo (hons-copy '(a b c))) 3))
(defthm l-thm2 (equal (lfoo (hons-copy '(a b c))) 3))
(defthm quick-sanity-check (check-q))
|