SET-BACKCHAIN-LIMIT

Major Section:  SWITCHES-PARAMETERS-AND-MODES

Note: This is an event! It does not print the usual event summary but nevertheless changes the ACL2 logical world and is so recorded. Moreover, its effect is to set the acl2-defaults-table, and hence its effect is local to the book or encapsulate form containing it; see acl2-defaults-table.

This event sets the global backchain-limit used by the ACL2 type-set and rewriting mechanisms. Its value may be a cons whose car and cdr are each either nil or a non-negative integer. Its value x may also be nil or a non-negative integer, which is treated as a cons whose car and cdr are both x.

The car is used to limit backchaining used by the ACL2 type-set mechanism, while the cdr is used to limit backchaining used by the rewriting mechanism. See backchain-limit for details about how backchain-limits are used. Rewrite backchain limits may also be installed at the level of hints; see hints for a discussion of :backchain-limit-rw.

:set-backchain-limit nil  ; do not impose any additional limits
:set-backchain-limit 0    ; allow only type-set reasoning for rewriting
                          ; hypotheses
:set-backchain-limit 500  ; allow backchaining to a depth of no more
                          ; than 500 for rewriting hypotheses
(set-backchain-limit 500) ; same as above
:set-backchain-limit (500 500)
                          ; same as above
(set-backchain-limit '(500 500))
                          ; same as above
(set-backchain-limit '(3 500))
                          ; allow type-set backchaining to a depth of no more
                          ; than 3 and rewriter backchaining to a depth of no
                          ; more than 500