ABORT!

Major Section:  MISCELLANEOUS

When (abort!) is evaluated inside of ACL2's command loop, the current computation is aborted and control returns to the top of the command loop, exactly as though the user had interrupted and aborted the current computation.

Logically speaking, (abort!) = nil. But imagine that it is defined in such a way that it causes a stack overflow or other resource exhaustion when called.

ACCUMULATED-PERSISTENCE

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)

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 try

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.

ACKNOWLEDGEMENTS

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.

ACL2-COUNT

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-counts 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-counts of the numerator and denominator. The acl2-count of a complex rational is one greater than the sum of the acl2-counts of the real and imaginary parts.

ACL2-CUSTOMIZATION

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.

APROPOS

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.

ARRAYS

Major Section:  MISCELLANEOUS

Below we begin a detailed presentation of ACL2 arrays. Related topics:

• AREF1 -- access the elements of a 1-dimensional array

• AREF2 -- access the elements of a 2-dimensional array

• ARRAY1P -- recognize a 1-dimensional array

• ARRAY2P -- recognize a 2-dimensional array

• ASET1 -- set the elements of a 1-dimensional array

• ASET2 -- set the elements of a 2-dimensional array

• COMPRESS1 -- remove irrelevant pairs from a 1-dimensional array

• COMPRESS2 -- remove irrelevant pairs from a 2-dimensional array

• DEFAULT -- return the :default from the header of a 1- or 2-dimensional array

• DIMENSIONS -- return the :dimensions from the header of a 1- or 2-dimensional array

• HEADER -- return the header of a 1- or 2-dimensional array

• MAXIMUM-LENGTH -- return the :maximum-length from the header of an array

• SLOW-ARRAY-WARNING -- a warning issued when arrays are used inefficiently

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).

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 ith 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 conses 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 aref1s on that new array will be fast. Any aref1s 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 asets 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))))

Now execute

ACL2 !>(assign b (aset1 'demo (@ a) 1 'one))

All of the aref1s 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))))

ACL2 !>(cnt 'demo (@ b) 4 'zero)

ACL2 !>(cnt 'demo (@ b) 4 'uninitialized)

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]


(let ((c (aset1 'demo (@ b) 2 'two)))                           ; [latter]
  (cnt 'demo c 4 (aref1 'demo c 2)))

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))

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))

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))

ACL2 !>(assign b (compress1 'demo (@ b)))

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.

AREF1

Major Section:  ARRAYS

Example Form:
(aref1 'delta1 a (+ i k))

General Form:
(aref1 name alist index)

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.

AREF2

Major Section:  ARRAYS

Example Form:
(aref2 'delta1 a i j)

General Form:
(aref2 name alist i j)

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.

ARRAY1P

Major Section:  ARRAYS

Example Form:
(array1p 'delta1 a)

General Form:
(array1p name alist)

ARRAY2P

Major Section:  ARRAYS

Example Form:
(array2p 'delta1 a)

General Form:
(array2p name alist)

ASET1

Major Section:  ARRAYS

Example Form:
(aset1 'delta1 a (+ i k) 27)

General Form:
(aset1 name alist index val)

In order to ``modify'' alist, aset1 conses 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.

ASET2

Major Section:  ARRAYS

Example Form:
(aset2 'delta1 a i j 27)

General Form:
(aset2 name alist i j val)

In order to ``modify'' alist, aset2 conses 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.

COMPRESS1

Major Section:  ARRAYS

Example Form:
(compress1 'delta1 a)

General Form:
(compress1 name 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.

COMPRESS2

Major Section:  ARRAYS

Example Form:
(compress2 'delta1 a)

General Form:
(compress2 name 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

Major Section:  ARRAYS

Example Form:
(default 'delta1 a)

General Form:
(default name alist)

DIMENSIONS

Major Section:  ARRAYS

Example Form:
(dimensions 'delta1 a)

General Form:
(dimensions name alist)

HEADER

Major Section:  ARRAYS

Example Form:
(header 'delta1 a)

General Form:
(header name alist)

MAXIMUM-LENGTH

Major Section:  ARRAYS

Example Form:
(maximum-length 'delta1 a)

General Form:
(maximum-length name alist)

SLOW-ARRAY-WARNING

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))) ...)

 (foo (let ((alist (aset1 name alist i val))) ...)  ; arg 1
      (bar alist))                                  ; arg 2

 (let ((alist (aset1 name alist alist i val)))
   (foo ...                                         ; arg 1
        (bar alist)))                               ; arg 2

(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.