		Search-engine friendly clone of the ACL2 documentation.

Set-register-invariant-risk

Avoid invariant-risk checking for specified functions

See invariant-risk for an introduction to the notion of invariant-risk. Also see set-check-invariant-risk for a way to avoid invariant-risk checking at runtime. The present topic discusses a way to avoid marking specified functions as potentially having invariant-risk.

General Forms:
(set-register-invariant-risk t)   ; default
(set-register-invariant-risk nil) ; requires active trust tag

See community book books/demos/register-invariant-risk.lisp for a demonstration of how to use this utility.

Normally a function is marked by ACL2 as having ``invariant-risk'' if its execution may have the potential to corrupt the ACL2 state. This causes execution slowdown that is not necessary if there is actually no such potential. In such cases it may be advisable to instruct ACL2 to avoid marking that function as having invariant-risk. This can be done by including the form (set-register-invariant-risk nil) in the book (or its portcullis commands) or encapsulate event that contains the definition of that function (or, it can be done in the top-level loop before defining that function). This action requires an active trust tag (see defttag) because you are asserting, without proof, that invariant-risk is impossible for that function. Its effect can be reversed (returning to the default behavior) by evaluating (set-register-invariant-risk t), which does not require an active trust tag.

To see the current setting (i.e., the default of t or else nil after evaluation of (set-register-invariant-risk nil)), evaluate (get-register-invariant-risk state).

Note this utility does not affect whether a stobj primitive is marked with invariant-risk (which seems too dangerous in general); it only applies to functions introduced by defun. If you want a version of a stobj updater that has no invariant-risk and you have invoked (set-register-invariant-risk nil), then define a function that calls the stobj updater.

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.