A warning or error issued when arrays are used inefficiently
If you use ACL2 arrays you may sometimes see a slow array warning. We explain below what that warning means and some likely ``mistakes'' it may signify.
First, we note that you can control whether or not you get a warning and, if so, whether or not a break (error from which you can continue; see break$) ensues:
(assign slow-array-action :warning) ; warn on slow array access (default) (assign slow-array-action :break) ; warn as above, and then call break$ (assign slow-array-action nil) ; do not warn or break on slow array access
If you are using ACL2 arrays, then you probably care about performance, in
which case it is probably best to avoid the
The discussion in the documentation for arrays defines what we mean
by the semantic value of a name. As noted there, behind the scenes ACL2
maintains the invariant that with some names there is associated a pair
consisting of an ACL2 array
If aref1 is called on a name and alist, and the alist is not the then-current semantic value of the name, the correct result is computed but it requires linear time because the alist must be searched. When this happens, aref1 prints a slow array warning message to the comment window. Aset1 behaves similarly because the array it returns will cause the slow array warning every time it is used.
From the purely logical perspective there is nothing ``wrong'' about such use of arrays and it may be spurious to print a warning message. But because arrays are generally used to achieve efficiency, the slow array warning often means the user's intentions are not being realized. Sometimes merely performance expectations are not met; but the message may mean that the functional behavior of the program is different than intended.
Here are some ``mistakes'' that might cause this behavior. In the
following we suppose the message was printed by aset1 about an array
(1) Compress1 was never called on
(3) An aset1 was done to modify
(let ((alist (aset1 name alist i val))) ...)
and make sure that the subsequent function body is entirely within the
scope of the let. Any uses of
(foo (let ((alist (aset1 name alist i val))) ...) ; arg 1 (bar alist)) ; arg 2
you have broken the rules, because in
(let ((alist (aset1 name alist alist i val))) (foo ... ; arg 1 (bar alist))) ; arg 2
Of course, this may not mean the same thing.
(4) A function which takes