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 nil setting. Below we assume
the default behavior: a warning, but no break.
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 alist, called the semantic value of the name,
and an equivalent raw lisp array. Access to ACL2 array elements, as in
(aref1 name alist i), is executed in constant time when the array alist
is the semantic value of the name, because we can just use the corresponding
raw lisp array to obtain the answer. Aset1 and compress1
modify the raw lisp array appropriately to maintain the invariant.
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
Here are some ``mistakes'' that might cause this behavior. In the
following we suppose the message was printed by aset1 about an array
named name. Suppose the alist supplied aset1 is alist.
(1) Compress1 was never called on name and alist. That
is, perhaps you created an alist that is an array1p and then proceeded
to access it with aref1 but never gave ACL2 the chance to create a raw
lisp array for it. After creating an alist that is intended for use as an
array, you must do (compress1 name alist) and pass the resulting
alist' as the array.
(2) Name is misspelled. Perhaps the array was compressed under the
name 'delta-1 but accessed under 'delta1?
(3) An aset1 was done to modify alist, producing a new array,
alist', but you subsequently used alist as an array. Inspect all
(aset1 name ...) occurrences and make sure that the alist modified is
never used subsequently (either in that function or any other). It is good
practice to adopt the following syntactic style. Suppose the alist you are
manipulating is the value of the local variable alist. Suppose at some
point in a function definition you wish to modify alist with aset1. Then write
(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 alist subsequently will refer to
the new alist and it is impossible to refer to the old alist. Note that if
(foo (let ((alist (aset1 name alist i val))) ...) ; arg 1
(bar alist)) ; arg 2
you have broken the rules, because in arg 1 you have modified
alist but in arg 2 you refer to the old value. An appropriate
rewriting is to lift the let out:
(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 alist as an argument and modifies it with
aset1 fails to return the modified version. This is really the same
as (3) above, but focuses on function interfaces. If a function takes an
array alist as an argument and the function uses aset1 (or a
subfunction uses aset1, etc.), then the function probably ``ought'' to
return the result produced by aset1. The reasoning is as follows. If
the array is passed into the function, then the caller is holding the array.
After the function modifies it, the caller's version of the array is obsolete.
If the caller is going to make further use of the array, it must obtain the
latest version, i.e., that produced by the function.