/usr/share/acl2-6.3/books/parallel/matrix-multiplication-serial.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 | (in-package "ACL2")
(include-book "misc/assert" :dir :system)
(include-book "make-event/embeddable-event-forms" :dir :system)
(include-book "matrix-multiplication-setup")
; NOTE: See the comment at this same point in
; matrix-multiplication-parallel.lisp about apparently 64-bit GCL issues.
(set-compile-fns t)
(defun multiply-matrices-aux (A B)
(declare (xargs :mode :program))
(if (endp A)
nil
(cons (multiply-matrices-row (car A) B)
(multiply-matrices-aux (cdr A) B))))
(defun multiply-matrices (A B)
(declare (xargs :mode :program))
(multiply-matrices-aux A B))
(observe$ "Running simple matrix multiplcation test.")
(assert! (let ((mini-matrix '((1 2 3) (4 5 6) (7 8 9))))
(equal (multiply-matrices mini-matrix mini-matrix)
'((14 32 50)
(32 77 122)
(50 122 194)))))
(observe$ "Generating 32 bit source matrices A and B (serial case).")
(assign$ a (make-matrix *a-rows* *a-cols* nil))
(assign$ b (make-matrix *b-rows* *b-cols* nil))
(observe$ "Testing the time it takes to transpose B.")
(assign$ b-transposed (time$ (transpose-fast (@ b))))
(observe$ "Testing the time it takes to generate the results (serial case). ~
It takes approximately 22.6 seconds on our machine.")
(assert-when-parallel
(time$ (multiply-matrices (@ a) (@ b-transposed))))
(observe$ "Done testing matrix multiplication (serial case).")
|