Set-verify-guards-eagerness
The eagerness with which guard verification is tried.
Example Forms: try guard verification?
(set-verify-guards-eagerness 0) ; no, unless :verify-guards t
(set-verify-guards-eagerness 1) ; yes if :guard, type :stobjs, or :df present
(set-verify-guards-eagerness 2) ; yes, unless :verify-guards nil
(set-verify-guards-eagerness 3) ; yes
Note: This is an event! It does not print the usual event summary
but nevertheless changes the ACL2 logical world and is so recorded.
General Form:
(set-verify-guards-eagerness n)
where n is a variable-free term that evaluates to 0, 1,
2, or 3. This macro is essentially equivalent to
(table acl2-defaults-table :verify-guards-eagerness n)
and hence is local to any books and encapsulate
events in which it occurs; see ACL2-defaults-table. However,
unlike the above simple call of the table event function (see table), no output results from a set-verify-guards-eagerness event.
Set-verify-guards-eagerness may be thought of as an event that merely
sets a flag to 0, 1, 2, or 3. The flag is used by certain
defun events to determine whether guard verification is
tried. The flag is irrelevant to those defun events in
:program mode. It is also irrelevant to those defun
events in which an explicit :verify-guards setting is
provided among the xargs, except when the flag is 3. In the
:program mode case, guard verification is not done because
it can only be done when logical functions are being defined. Otherwise,
unless the flag is 3, the explicit :verify-guards setting
determines whether guard verification is tried. So consider a
:logic mode defun in which no :verify-guards
setting is provided. Is guard verification tried? The answer depends
on the eagerness setting as follows. If the eagerness is 0, guard
verification is not tried. If the eagerness is 1, it is tried if and
only if a guard is explicitly specified in the defun, in the following
sense: there is an xargs keyword :guard, :stobjs, or :dfs,
or there is a type declaration. If the eagerness is 2 or 3,
guard verification is tried.
The above remarks apply to verify-termination events,
according to whether guards are explicitly specified in the existing,
corresponding :program mode definitions.
The default behavior of the system is as though the
:verify-guards-eagerness is 1. The current behavior can be
ascertained by evaluating the form (default-verify-guards-eagerness (w
state)).
