Major Section: MISCELLANEOUS
Useful Forms: (accumulated-persistence t) ; activate statistics gathering(show-accumulated-persistence :frames) ; display statistics ordered by (show-accumulated-persistence :tries) ; frames built, times tried, (show-accumulated-persistence :ratio) ; or their ratio
(accumulated-persistence nil) ; deactivate
Generally speaking, the more ACL2 knows, the slower it runs. That is because the search space grows with the number of alternative rules. Often, the system tries to apply rules that you have forgotten were even there, if you knew about them in the first place! ``Accumulated-persistence'' is a statistic (originally developed for Nqthm) that helps you identify the rules that are causing ACL2's search space to explode.
Accumulated persistence tracking can be turned on or off. It is generally off. When on, the system runs about 4 times slower than otherwise! But some useful numbers are collected. When it is turned on, by
ACL2 !>(accumulated-persistence t)an accumulation site is initialized and henceforth data about which rules are being tried is accumulated into that site. That accumulated data can be displayed with
show-accumulated-persistence
,
as described in detail below. When accumulated persistence is
turned off, with (accumulated-persistence nil)
, the accumulation
site is wiped out and the data in it is lost.The ``accumulated persistence'' of a rune is the number of runes the system has attempted to apply (since accumulated persistence was last activated) while the given rune was being tried.
Consider a :
rewrite
rule named rune
. For simplicity, let us imagine
that rune
is tried only once in the period during which accumulated
persistence is being monitored. Recall that to apply a rewrite rule
we must match the left-hand side of the conclusion to some term we
are trying to rewrite, establish the hypotheses of rune
by
rewriting, and, if successful, then rewrite the right-hand side of
the conclusion. We say rune
is ``being tried'' from the time we
have matched its left-hand side to the time we have either abandoned
the attempt or rewritten its right-hand side. During that period of
time other rules might be tried, e.g., to establish the hypotheses.
The rules tried while rune
is being tried are ``billed'' to rune
in
the sense that they are being considered here only because of the
demands of rune
. Thus, if no other rules are tried during that
period, the accumulated persistence of rune
is 1
-- we ``bill'' rune
once for its own application attempt. If, on the other hand, we
tried 10
rules on behalf of that application of rune
, then rune
's
accumulated persistence would be 11
.
One way to envision accumulated persistence is to imagine that every time a rune is tried it is pushed onto a stack. The rules tried on behalf of a given application of a rune are thus pushed and popped on the stack above that rune. A lot of work might be done on its behalf -- the stack above the rune grows and shrinks repeatedly as the search continues for a way to use the rune. All the while, the rune itself ``persists'' in the stack, until we finish with the attempt to apply it, at which time we pop it off. The accumulated persistence of a rune is thus the number of stack frames built while the given rune was on the stack.
Note that accumulated persistence is not concerned with whether the attempt to apply a rune is successful. Each of the rules tried on its behalf might have failed and the attempt to apply the rune might have also failed. The ACL2 proof script would make no mention of the rune or the rules tried on its behalf because they did not contribute to the proof. But time was spent pursuing the possible application of the rune and accumulated persistence is a measure of that time.
A high accumulated persistence might come about in two extreme ways. One is that the rule causes a great deal of work every time it is tried. The other is that the rule is ``cheap'' but is tried very often. We therefore keep track of the number of times each rule is tried as well as its persistence. The ratio between the two is the average amount of work done on behalf of the rule each time it is tried.
When the accumulated persistence totals are displayed by the
function show-accumulated-persistence
we sort them so that the most
expensive runes are shown first. We can sort according to one of
three keys:
:frames - the number of frames built on behalf of the rune :tries - the number of times the rune was tried :ratio - frames built per tryThe key simply determines the order in which the information is presented. If no argument is supplied to
show-accumulated-persistence
, :frames
is used.
Note that a rune with high accumulated persistence may not actually
be the ``culprit.'' For example, suppose rune1
is reported to have
a :ratio
of 101
, meaning that on the average a hundred and one
frames were built each time rune1
was tried. Suppose rune2
has a
:ratio
of 100
. It could be that the attempt to apply rune1
resulted
in the attempted application of rune2
and no other rune. Thus, in
some sense, rune1
is ``cheap'' and rune2
is the ``culprit'' even
though it costs less than rune1
.
Users are encouraged to think about other meters we could install in
ACL2 to help diagnose performance problems.
Major Section: MISCELLANEOUS
The development of ACL2 was made possible by funding from the U. S. Department of Defense, including ARPA and ONR.
ACL2 was started in August, 1989 by Boyer and Moore working together. They co-authored the first versions of axioms.lisp and basis.lisp, with Boyer taking the lead in the formalization of ``state'' and the most primitive io functions. Boyer also had a significant hand in the development of the early versions of the files interface-raw.lisp and translate.lisp. For several years, Moore alone was responsible for developing the ACL2 system code, though he consulted often with both Boyer and Kaufmann. In August, 1993, Kaufmann became jointly responsible with Moore for developing the system. Boyer has continued to provide valuable consulting on an informal basis.
Bishop Brock was the heaviest early user of ACL2, and provided many
suggestions for improvements. In particular, the :cases
and
:restrict
hints were his idea; he developed an early version
of congruence-based reasoning for Nqthm; and he helped in the
development of some early books about arithmetic.
John Cowles also helped in the development of some early books about arithmetic, and also provided valuable feedback and bug reports.
Other early users of ACL2 at Computational Logic, Inc. helped influence its development. In particular, Warren Hunt helped with the port to Macintosh Common Lisp, and Art Flatau and Mike Smith provided useful general feedback.
Mike Smith helped develop the Emacs portion of the implementation of proof trees.
Bill Schelter made some enhancements to akcl (now gcl) that helped to enhance ACL2 performance in that Common Lisp implementation, and more generally, responded helpfully to our bug reports.
Kent Pitman helped in our interaction with the ANSI Common Lisp standardization committee, X3J13.
Regarding the documentation:
Bill Young wrote significant portions of the ACL2-TUTORIAL section of the ACL2 documentation, an important task for which we are grateful. He, Bishop Brock, Rich Cohen, and Noah Friedman read over considerable amounts of the documentation, and made many useful comments. Others, particularly Bill Bevier and John Cowles, have also made useful comments on the documentation.
Art Flatau helped develop the ACL2 markup language and translators from that language to Texinfo and HTML.
Laura Lawless provided many hours of help in marking up appropriate parts of the documentation in typewriter font.
Noah Friedman developed an Emacs tool that helped us insert ``invisible links'' into the documentation, which improve the usability of that documentation under HTML readers such as Mosaic.
Richard Stallman contributed a texinfo patch, to be found in the
file doc/texinfo.tex
.
Major Section: MISCELLANEOUS
(Acl2-count x)
returns a nonnegative integer that indicates the
``size'' of its argument x
.
All characters and symbols have acl2-count 0
. The acl2-count
of a
string is the number of characters in it, i.e., its length. The
acl2-count
of a cons
is one greater than the sum of the acl2-count
s
of the car
and cdr
. The acl2-count
of an integer is its absolute
value. The acl2-count
of a rational is the sum of the acl2-count
s
of the numerator and denominator. The acl2-count
of a complex
rational is one greater than the sum of the acl2-count
s of the real
and imaginary parts.
Major Section: MISCELLANEOUS
The file "acl2-customization.lisp"
is automatically loaded, via
ld
, the first time lp
is called in an ACL2 session, provided
such a file exists on the current directory. Except for the fact
that this ld
command is not typed explicitly by you, it is a
standard ld
command, with one exception: any settings of ld
specials are remembered once this call of ld
has completed. For
example, suppose that you start your customization file with
(set-ld-skip-proofsp t state)
, so that proofs are skipped as it is
loaded with ld
. Then the ld
special ld-skip-proofsp
will remain t
after the ld
has completed, causing proofs to be skipped in your
ACL2 session, unless your customization file sets this variable back
to nil
, say with (set-ld-skip-proofsp nil state)
.
The customization file "acl2-customization.lisp"
actually
resides on the connected book directory; see cbd. Except, if
that file does not exist, then ACL2 looks for
"acl2-customization.lisp"
on your home directory. If ACL2 does
not find that file either, then no customization occurs and lp
enters the standard ACL2 read-eval-print loop.
If the customization file exists, it is loaded with ld
using the
usual default values for the ld
specials (see ld). Thus, if an
error is encountered, no subsequent forms in the file will be
evaluated.
To create a customization file it is recommended that you first give
it a name other than "acl2-customization.lisp"
so that ACL2 does
not try to include it prematurely when you next enter lp
. Then,
while in the uncustomized lp
, explicitly invoke ld
on your evolving
(but renamed) customization file until all forms are successfully
evaluated. The same procedure is recommended if for some reason
ACL2 cannot successfully evaluate all forms in your customization
file: rename your customization file so that ACL2 does not try to
ld
it automatically and then debug the new file by explicit calls to
ld
.
When you have created a file that can be loaded with ld
without
error and that you wish to be your customization file, name it
"acl2-customization.lisp"
and put it on the current directory or
in your home directory. The first time after starting up ACL2 that
you invoke (lp)
, ACL2 will automatically load the
"acl2-customization.lisp"
file from the cbd (see cbd) if
there is one, and otherwise will load it from your home directory.
Note that if you certify a book after the (automatic) loading of an
acl2-customization
file, the forms in that file will be part of the
portcullis of the books you certify! That is, the forms in your
customization file at certification time will be loaded whenever
anybody uses the books you are certifying. Since customization
files generally contain idiosyncratic commands, you may not want
yours to be part of the books you create for others. Thus, if you
have a customization file then you may want to invoke :ubt 1
before
certifying any books.
The conventions concerning ACL2 customization are liable to change
as we get more experience with the interaction between
customization, certification of books for others, and routine
undoing. For example, at the moment it is regarded as a feature of
customization that it can be undone but it might be regarded as a
bug if you accidentally undo your customization.
:
doc
and :
more-doc
text
Major Section: MISCELLANEOUS
NOTE: The :
docs
command only makes sense at the terminal.
Example: :Docs "compile" will find all documented topics mentioning the string "compile"
When the :
docs
command is given a stringp
argument it searches the
text produced by :
doc
and :
more-doc
and lists all the documented
topics whose text contains the given string. For purposes of this
string matching we ignore distinctions of case and the amount and
kind (but not presence) of white space. We also treat hyphen as
whitespace.
Major Section: MISCELLANEOUS
Below we begin a detailed presentation of ACL2 arrays. Related topics:
:default
from the header of a 1- or 2-dimensional array
:dimensions
from the header of a 1- or 2-dimensional array
:maximum-length
from the header of an array
In this note we explain 1-dimensional arrays. In particular, we explain briefly how to create, access, and ``modify'' them, how they are implemented, and how to program with them. 2-dimensional arrays are dealt with by analogy.
The Logical Description of ACL2 Arrays
An ACL2 1-dimensional array is an object that associates arbitrary
objects with certain integers, called ``indices.'' Every array has a
dimension, dim
, which is a positive integer. The indices of an
array are the consecutive integers from 0
through dim-1
. To obtain
the object associated with the index i
in an array a
, one uses
(aref1 name a i)
. Name
is a symbol that is irrelevant to the
semantics of aref1
but affects the speed with which it computes. We
will talk more about array ``names'' later. To produce a new array
object that is like a
but which associates val
with index i
, one
uses (aset1 name a i val)
.
An ACL2 1-dimensional array is actually an alist. There is no
special ACL2 function for creating arrays; they are generally built
with the standard list processing functions list
and cons
. However,
there is a special ACL2 function, called compress1
, for speeding up
access to the elements of such an alist. We discuss compress1
later.
One element of the alist must be the ``header'' of the array. The
header of a 1-dimensional array with dimension dim
is of the form:
(:HEADER :DIMENSIONS (dim) :MAXIMUM-LENGTH max :DEFAULT obj :NAME name).
Obj
may be any object and is called the ``default value'' of the
array. Max
must be an integer greater than dim
. Name
must be a
symbol. The :
default
and :name
entries are optional; if :
default
is
omitted, the default value is nil
. The function header
, when given
a name and a 1- or 2-dimensional array, returns the header of the
array. The functions dimensions
, maximum-length
, and default
are
similar and return the corresponding fields of the header of the
array. The role of the :
dimensions
field is obvious: it specifies
the legal indices into the array. The roles played by the
:
maximum-length
and :
default
fields are described below.
Aside from the header, the other elements of the alist must each be
of the form (i . val)
, where i
is an integer and 0 <= i < dim
, and
val
is an arbitrary object.
(Aref1 name a i)
is guarded so that name
must be a symbol, a
must be
an array and i
must be an index into a
. The value of
(aref1 name a i)
is either (cdr (assoc i a))
or else is the
default value of a
, depending on whether there is a pair in a
whose car
is i
. Note that name
is irrelevant to the value of
an aref1
expression. You might :pe aref1
to see how simple
the definition is.
(Aset1 name a i val)
is guarded analogously to the aref1
expression.
The value of the aset1
expression is essentially
(cons (cons i val) a)
. Again, name
is irrelevant. Note
(aset1 name a i val)
is an array, a'
, with the property that
(aref1 name a' i)
is val
and, except for index i
, all other
indices into a'
produce the same value as in a
. Note also
that if a
is viewed as an alist (which it is) the pair
``binding'' i
to its old value is in a'
but ``covered up'' by
the new pair. Thus, the length of an array grows by one when
aset1
is done.
Because aset1
covers old values with new ones, an array produced by
a sequence of aset1
calls may have many irrelevant pairs in it. The
function compress1
removes these irrelevant pairs. Thus,
(compress1 name a)
returns an array that is equivalent
(vis-a-vis aref1
) to a
but which may be shorter. For technical
reasons, the alist returned by compress1
may also list the pairs
in a different order than listed in a
.
To prevent arrays from growing excessively long due to repeated
aset1
operations, aset1
actually calls compress1
on the new
alist whenever the length of the new alist exceeds the
:
maximum-length
entry, max
, in the header of the array. See
the definition of aset1
(for example by using :
pe
). This is
primarily just a mechanism for freeing up cons
space consumed
while doing aset1
operations.
This completes the logical description of 1-dimensional arrays.
2-dimensional arrays are analogous. The :
dimensions
entry of the
header of a 2-dimensional array should be (dim1 dim2)
. A pair of
indices, i
and j
, is legal iff 0 <= i < dim1
and 0 <= j < dim2
.
The :
maximum-length
must be greater than dim1*dim2
. Aref2
, aset2
,
and compress2
are like their counterparts but take an additional
index
argument. Finally, the pairs in a 2-dimensional array are of
the form ((i . j) . val)
.
The Implementation of ACL2 Arrays
Very informally speaking, the function compress1
``creates'' an
ACL2 array that provides fast access, while the function aref1
``maintains'' fast access. We now describe this informal idea more
carefully.
Aref1
is essentially assoc
. If aref1
were implemented naively the
time taken to access an array element would be linear in the
dimension of the array and the number of ``assignments'' to it (the
number of aset1
calls done to create the array from the initial
alist). This is intolerable; arrays are ``supposed'' to provide
constant-time access and change.
The apparently irrelevant names associated with ACL2 arrays allow us to provide constant-time access and change when arrays are used in ``conventional'' ways. The implementation of arrays makes it clear what we mean by ``conventional.''
Recall that array names are symbols. Behind the scenes, ACL2 associates two objects with each ACL2 array name. The first object is called the ``semantic value'' of the name and is an alist. The second object is called the ``raw lisp array'' and is a Common Lisp array.
When (compress1 name alist)
builds a new alist, a'
, it sets the
semantic value of name
to that new alist. Furthermore, it creates a
Common Lisp array and writes into it all of the index/value pairs of
a'
, initializing unassigned indices with the default value. This
array becomes the raw lisp array of name
. Compress1
then returns
a'
, the semantic value, as its result, as required by the definition
of compress1
.
When (aref1 name a i)
is invoked, aref1
first determines whether the
semantic value of name
is a
(i.e., is eq
to the alist a
). If so,
aref1
can determine the i
th element of a
by invoking Common Lisp's
aref
function on the raw lisp array associated with name. Note that
no linear search of the alist a
is required; the operation is done
in constant time and involves retrieval of two global variables, an
eq
test and jump
, and a raw lisp array access. In fact, an ACL2
array access of this sort is about 5 times slower than a C array
access. On the other hand, if name
has no semantic value or if it
is different from a
, then aref1
determines the answer by linear
search of a
as suggested by the assoc-like
definition of aref1
.
Thus, aref1
always returns the axiomatically specified result. It
returns in constant time if the array being accessed is the current
semantic value of the name used. The ramifications of this are
discussed after we deal with aset1
.
When (aset1 name a i val)
is invoked, aset1
does two cons
es to
create the new array. Call that array a'
. It will be returned as
the answer. (In this discussion we ignore the case in which aset1
does a compress1
.) However, before returning, aset1
determines if
name
's semantic value is a
. If so, it makes the new semantic value
of name
be a'
and it smashes the raw lisp array of name
with val
at
index i
, before returning a'
as the result. Thus, after doing an
aset1
and obtaining a new semantic value a'
, all aref1
s on that new
array will be fast. Any aref1
s on the old semantic value, a
, will
be slow.
To understand the performance implications of this design, consider
the chronological sequence in which ACL2 (Common Lisp) evaluates
expressions: basically inner-most first, left-to-right,
call-by-value. An array use, such as (aref1 name a i)
, is ``fast''
(constant-time) if the alist supplied, a
, is the value returned by
the most recently executed compress1
or aset1
on the name supplied.
In the functional expression of ``conventional'' array processing,
all uses of an array are fast.
The :name
field of the header of an array is completely irrelevant.
Our convention is to store in that field the symbol we mean to use
as the name of the raw lisp array. But no ACL2 function inspects
:name
and its primary value is that it allows the user, by
inspecting the semantic value of the array -- the alist -- to recall
the name of the raw array that probably holds that value. We say
``probably'' since there is no enforcement that the alist was
compressed under the name in the header or that all aset
s used that
name. Such enforcement would be inefficient.
Some Programming Examples
In the following examples we will use ACL2 ``global variables'' to hold several arrays. See @, and see assign.
Let the state
global variable a
be the 1-dimensional compressed
array of dimension 5
constructed below.
ACL2 !>(assign a (compress1 'demo '((:header :dimensions (5) :maximum-length 15 :default uninitialized :name demo) (0 . zero))))Then
(aref1 'demo (@ a) 0)
is zero
and (aref1 'demo (@ a) 1)
is
uninitialized
.Now execute
ACL2 !>(assign b (aset1 'demo (@ a) 1 'one))Then
(aref1 'demo (@ b) 0)
is zero
and (aref1 'demo (@ b) 1)
is
one
.
All of the aref1
s done so far have been ``fast.''
Note that we now have two array objects, one in the global variable
a
and one in the global variable b
. B
was obtained by assigning to
a
. That assignment does not affect the alist a
because this is an
applicative language. Thus, (aref1 'demo (@ a) 1)
must still be
uninitialized
. And if you execute that expression in ACL2 you will
see that indeed it is. However, a rather ugly comment is printed,
namely that this array access is ``slow.'' The reason it is slow is
that the raw lisp array associated with the name demo
is the array
we are calling b
. To access the elements of a
, aref1
must now do a
linear search. Any reference to a
as an array is now
``unconventional;'' in a conventional language like Ada or Common
Lisp it would simply be impossible to refer to the value of the
array before the assignment that produced our b
.
Now let us define a function that counts how many times a given
object, x
, occurs in an array. For simplicity, we will pass in the
name and highest index of the array:
ACL2 !>(defun cnt (name a i x) (declare (xargs :guard (and (array1p name a) (integerp i) (>= i -1) (< i (car (dimensions name a)))) :mode :logic :measure (nfix (+ 1 i)))) (cond ((zp (1+ i)) 0) ; return 0 if i is at most -1 ((equal x (aref1 name a i)) (1+ (cnt name a (1- i) x))) (t (cnt name a (1- i) x))))To determine how many times
zero
appears in (@ b)
we can execute:
ACL2 !>(cnt 'demo (@ b) 4 'zero)The answer is
1
. How many times does uninitialized
appear in
(@ b)
?
ACL2 !>(cnt 'demo (@ b) 4 'uninitialized)The answer is
3
, because positions 2
, 3
and 4
of the array contain
that default value.
Now imagine that we want to assign 'two
to index 2
and then count
how many times the 2nd element of the array occurs in the array.
This specification is actually ambiguous. In assigning to b
we
produce a new array, which we might call c
. Do we mean to count the
occurrences in c
of the 2nd element of b
or the 2nd element of c
?
That is, do we count the occurrences of uninitialized
or the
occurrences of two
? If we mean the former the correct answer is 2
(positions 3
and 4
are uninitialized
in c
); if we mean the latter,
the correct answer is 1
(there is only one occurrence of two
in c
).
Below are ACL2 renderings of the two meanings, which we call
[former]
and [latter]
. (Warning: Our description of these
examples, and of an example [fast former]
that follows, assumes
that only one of these three examples is actually executed; for
example, they are not executed in sequence. See ``A Word of
Warning'' below for more about this issue.)
(cnt 'demo (aset1 'demo (@ b) 2 'two) 4 (aref1 'demo (@ b) 2)) ; [former]Note that in(let ((c (aset1 'demo (@ b) 2 'two))) ; [latter] (cnt 'demo c 4 (aref1 'demo c 2)))
[former]
we create c
in the second argument of the
call to cnt
(although we do not give it a name) and then refer to b
in the fourth argument. This is unconventional because the second
reference to b
in [former]
is no longer the semantic value of demo
.
While ACL2 computes the correct answer, namely 2
, the execution of
the aref1
expression in [former]
is done slowly.A conventional rendering with the same meaning is
(let ((x (aref1 'demo (@ b) 2))) ; [fast former] (cnt 'demo (aset1 'demo (@ b) 2 'two) 4 x))which fetches the 2nd element of
b
before creating c
by
assignment. It is important to understand that [former]
and
[fast former]
mean exactly the same thing: both count the number
of occurrences of uninitialized
in c
. Both are legal ACL2 and
both compute the same answer, 2
. Indeed, we can symbolically
transform [fast former]
into [former]
merely by substituting
the binding of x
for x
in the body of the let
. But [fast former]
can be evaluated faster than [former]
because all of the
references to demo
use the then-current semantic value of
demo
, which is b
in the first line and c
throughout the
execution of the cnt
in the second line. [Fast former]
is
the preferred form, both because of its execution speed and its
clarity. If you were writing in a conventional language you would
have to write something like [fast former]
because there is no
way to refer to the 2nd element of the old value of b
after
smashing b
unless it had been saved first.
We turn now to [latter]
. It is both clear and efficient. It
creates c
by assignment to b
and then it fetches the 2nd element of
c
, two
, and proceeds to count the number of occurrences in c
. The
answer is 1
. [Latter]
is a good example of typical ACL2 array
manipulation: after the assignment to b
that creates c
, c
is used
throughout.
It takes a while to get used to this because most of us have grown
accustomed to the peculiar semantics of arrays in conventional
languages. For example, in raw lisp we might have written something
like the following, treating b
as a ``global variable'':
(cnt 'demo (aset 'demo b 2 'two) 4 (aref 'demo b 2))which sort of resembles
[former]
but actually has the semantics of
[latter]
because the b
from which aref
fetches the 2nd element is
not the same b
used in the aset
! The array b
is destroyed by the
aset
and b
henceforth refers to the array produced by the aset
, as
written more clearly in [latter]
.
A Word of Warning: Users must exercise care when experimenting with
[former]
, [latter]
and [fast former]
. Suppose you have
just created b
with the assignment shown above,
ACL2 !>(assign b (aset1 'demo (@ a) 1 'one))If you then evaluate
[former]
in ACL2 it will complain that the
aref1
is slow and compute the answer, as discussed. Then suppose
you evaluate [latter]
in ACL2. From our discussion you might expect
it to execute fast -- i.e., issue no complaint. But in fact you
will find that it complains repeatedly. The problem is that the
evaluation of [former]
changed the semantic value of demo
so that it
is no longer b
. To try the experiment correctly you must make b
be
the semantic value of demo
again before the next example is
evaluated. One way to do that is to execute
ACL2 !>(assign b (compress1 'demo (@ b)))before each expression. Because of issues like this it is often hard to experiment with ACL2 arrays at the top-level. We find it easier to write functions that use arrays correctly and efficiently than to so use them interactively.
This last assignment also illustrates a very common use of
compress1
. While it was introduced as a means of removing
irrelevant pairs from an array built up by repeated assignments, it
is actually most useful as a way of insuring fast access to the
elements of an array.
Many array processing tasks can be divided into two parts. During
the first part the array is built. During the second part the array
is used extensively but not modified. If your programming task can
be so divided, it might be appropriate to construct the array
entirely with list processing, thereby saving the cost of
maintaining the semantic value of the name while few references are
being made. Once the alist has stabilized, it might be worthwhile
to treat it as an array by calling compress1
, thereby gaining
constant time access to it.
ACL2's theorem prover uses this technique in connection with its
implementation of the notion of whether a rune is disabled or not.
Associated with every rune is a unique integer index
, called its
``nume.'' When each rule is stored, the corresponding nume is
stored as a component of the rule. Theories are lists of runes and
membership in the ``current theory'' indicates that the
corresponding rule is enabled. But these lists are very long and
membership is a linear-time operation. So just before a proof
begins we map the list of runes in the current theory into an alist
that pairs the corresponding numes with t
. Then we compress this
alist into an array. Thus, given a rule we can obtain its nume
(because it is a component) and then determine in constant time
whether it is enabled. The array is never modified during the
proof, i.e., aset1
is never used in this example. From the logical
perspective this code looks quite odd: we have replaced a
linear-time membership test with an apparently linear-time assoc
after going to the trouble of mapping from a list of runes to an
alist of numes. But because the alist of numes is an array, the
``apparently linear-time assoc
'' is more apparent than real; the
operation is constant-time.
Major Section: ARRAYS
Example Form: (aref1 'delta1 a (+ i k))whereGeneral Form: (aref1 name alist index)
name
is a symbol, alist
is a 1-dimensional array and index
is a legal index into alist
. This function returns the value
associated with index
in alist
, or else the default value of the
array. See arrays for details.
This function executes in virtually constant time if alist
is in
fact the ``semantic value'' associated with name
(see arrays).
When it is not, aref1
must do a linear search through alist
. In
that case the correct answer is returned but a slow array comment is
printed to the comment window. See slow-array-warning.
Major Section: ARRAYS
Example Form: (aref2 'delta1 a i j)whereGeneral Form: (aref2 name alist i j)
name
is a symbol, alist
is a 2-dimensional array and i
and j
are legal indices into alist
. This function returns the value
associated with (i . j)
in alist
, or else the default value of the
array. See arrays for details.
This function executes in virtually constant time if alist
is in
fact the ``semantic value'' associated with name
(see arrays).
When it is not, aref2
must do a linear search through alist
. In
that case the correct answer is returned but a slow array comment is
printed to the comment window. See slow-array-warning.
Major Section: ARRAYS
Example Form: (array1p 'delta1 a)whereGeneral Form: (array1p name alist)
name
and alist
are arbitrary objects. This function
returns t
if alist
is a 1-dimensional ACL2 array. Otherwise it
returns nil
. The function operates in constant time if alist
is the
semantic value of name
. See arrays.
Major Section: ARRAYS
Example Form: (array2p 'delta1 a)whereGeneral Form: (array2p name alist)
name
and alist
are arbitrary objects. This function returns t
if
alist
is a 2-dimensional ACL2 array. Otherwise it returns nil
. The function
operates in constant time if alist
is the semantic value of name
. See arrays.
Major Section: ARRAYS
Example Form: (aset1 'delta1 a (+ i k) 27)whereGeneral Form: (aset1 name alist index val)
name
is a symbol, alist
is a 1-dimensional array named name
,
index
is a legal index into alist
, and val
is an arbitrary object.
See arrays for details. Roughly speaking this function
``modifies'' alist
so that the value associated with index
is val
.
More precisely, it returns a new array, alist'
, of the same name and
dimension as alist
that, under aref1
, is everywhere equal to alist
except at index
where the result is val
. That is,
(aref1 name alist' i)
is (aref1 name alist i)
for all legal
indices i
except index
, where (aref1 name alist' i)
is val
.
In order to ``modify'' alist
, aset1
cons
es a new pair onto the
front. If the length of the resulting alist exceeds the
:
maximum-length
entry in the array header, aset1
compresses the
array as with compress1
.
It is generally expected that the ``semantic value'' of name
will be
alist
(see arrays). This function operates in virtually
constant time whether this condition is true or not (unless the
compress1
operation is required). But the value returned by this
function cannot be used efficiently by subsequent aset1
operations
unless alist
is the semantic value of name
when aset1
is executed.
Thus, if the condition is not true, aset1
prints a slow array
warning to the comment window. See slow-array-warning.
Major Section: ARRAYS
Example Form: (aset2 'delta1 a i j 27)whereGeneral Form: (aset2 name alist i j val)
name
is a symbol, alist
is a 2-dimensional array named name
,
i
and j
are legal indices into alist
, and val
is an arbitrary
object. See arrays for details. Roughly speaking this
function ``modifies'' alist
so that the value associated with
(i . j)
is val
. More precisely, it returns a new array,
alist'
, of the same name and dimension as alist
that, under
aref2
, is everywhere equal to alist
except at (i . j)
where
the result is val
. That is, (aref2 name alist' x y)
is
(aref2 name alist x y)
for all legal indices x
y
except
i
and j
where (aref2 name alist' i j)
is val
.
In order to ``modify'' alist
, aset2
cons
es a new pair onto the
front. If the length of the resulting alist
exceeds the
:
maximum-length
entry in the array header, aset2
compresses the
array as with compress2
.
It is generally expected that the ``semantic value'' of name
will be
alist
(see arrays). This function operates in virtually
constant time whether this condition is true or not (unless the
compress2
operation is required). But the value returned by this
function cannot be used efficiently by subsequent aset2
operations
unless alist
is the semantic value of name
when aset2
is executed.
Thus, if the condition is not true, aset2
prints a slow array
warning to the comment window. See slow-array-warning.
Major Section: ARRAYS
Example Form: (compress1 'delta1 a)whereGeneral Form: (compress1 name alist)
name
is a symbol and alist
is a 1-dimensional array named
name
. See arrays for details. Logically speaking, this
function removes irrelevant pairs from alist
, possibly shortening
it. The function returns a new array, alist'
, of the same name and
dimension as alist
, that, under aref1
, is everywhere equal to alist
.
That is, (aref1 name alist' i)
is (aref1 name alist i)
, for all
legal indices i
. Alist'
may be shorter than alist
and the
non-irrelevant pairs may occur in a different order than in alist
.
Practically speaking, this function plays an important role in the
efficient implementation of aref1
. In addition to creating the new
array, alist'
, compress1
makes that array the ``semantic value'' of
name
and allocates a raw lisp array to name
. For each legal index,
i
, that raw lisp array contains (aref1 name alist' i)
in slot i
.
Thus, subsequent aref1
operations can be executed in virtually
constant time provided they are given name
and the alist'
returned
by the most recently executed compress1
or aset1
on name
.
See arrays.
Major Section: ARRAYS
Example Form: (compress2 'delta1 a)whereGeneral Form: (compress2 name alist)
name
is a symbol and alist
is a 2-dimensional array named
name
. See arrays for details. Logically speaking, this
function removes irrelevant pairs from alist
, possibly shortening
it. The function returns a new array, alist'
, of the same name and
dimension as alist
, that, under aref2
, is everywhere equal to alist
.
That is, (aref2 name alist' i j)
is (aref2 name alist i j)
, for all
legal indices i
and j
. Alist'
may be shorter than alist
and the
non-irrelevant pairs may occur in a different order in alist'
than
in alist
.
Practically speaking, this function plays an important role in the
efficient implementation of aref2
. In addition to creating the new
array, alist'
, compress2
makes that array the ``semantic value'' of
name
and allocates a raw lisp array to name
. For all legal indices,
i
and j
, that raw lisp array contains (aref2 name alist' i j)
in
slot i
,j
. Thus, subsequent aref2
operations can be executed in
virtually constant time provided they are given name
and the alist'
returned by the most recently executed compress2
or aset2
on name
.
See arrays.
:default
from the header of a 1- or 2-dimensional array
Major Section: ARRAYS
Example Form: (default 'delta1 a)whereGeneral Form: (default name alist)
name
is an arbitrary object and alist
is a 1- or
2-dimensional array. This function returns the contents of the
:default
field of the header of alist
. When aref1
or aref2
is used
to obtain a value for an index (or index pair) not bound in alist
,
the default value is returned instead. Thus, the array alist
may be
thought of as having been initialized with the default value.
default
operates in virtually constant time if alist
is the semantic
value of name
. See arrays.
:dimensions
from the header of a 1- or 2-dimensional array
Major Section: ARRAYS
Example Form: (dimensions 'delta1 a)whereGeneral Form: (dimensions name alist)
name
is arbitrary and alist
is a 1- or 2-dimensional array.
This function returns the dimensions list of the array alist
. That
list will either be of the form (dim1)
or (dim1 dim2)
, depending on
whether alist
is a 1- or 2-dimensional array. Dim1
and dim2
will be
integers and each exceed by 1 the maximum legal corresponding index.
Thus, if dimensions
returns, say, '(100)
for an array a
named 'delta1
, then (aref1 'delta1 a 99)
is legal but
(aref1 'delta1 a 100)
violates the guards on aref1
.
Dimensions
operates in virtually constant time if alist
is the
semantic value of name
. See arrays.
Major Section: ARRAYS
Example Form: (header 'delta1 a)whereGeneral Form: (header name alist)
name
is arbitrary and alist
is a 1- or 2-dimensional array.
This function returns the header of the array alist
. The function
operates in virtually constant time if alist
is the semantic value
of name
. See arrays.
:maximum-length
from the header of an array
Major Section: ARRAYS
Example Form: (maximum-length 'delta1 a)whereGeneral Form: (maximum-length name alist)
name
is an arbitrary object and alist
is a 1- or
2-dimensional array. This function returns the contents of the
:maximum-length
field of the header of alist
. Whenever an aset1
or
aset2
would cause the length of the alist to exceed its maximum
length, a compress1
or compress2
is done automatically to remove
irrelevant pairs from the array. Maximum-length
operates in
virtually constant time if alist
is the semantic value of name
.
See arrays.
Major Section: ARRAYS
If you use ACL2 arrays you may sometimes see a slow array warning. We here explain what that warning means and some likely ``mistakes'' it may signify.
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 intended.
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 you write
(foo (let ((alist (aset1 name alist i val))) ...) ; arg 1 (bar alist)) ; arg 2you 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 2Of 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.