Major Section: OTHER
See verify-guards, and see guard for a discussion of guards. Also
see verify-guards-formula for a utility provided for viewing the guard proof
obligation, without proof. Guard-obligation is a lower level function
for use in system programs, not typically appropriate for most ACL2 users.
If you simply want to see the guard proof obligations,
see verify-guards-formula.
Example Form: (guard-obligation 'foo nil 'top-level state) (guard-obligation '(if (consp x) (foo (car x)) t) nil 'my-function state) General Forms: (guard-obligation name guard-debug ctx state) (guard-obligation term guard-debug ctx state)where the first argument is either the name of a function or theorem or is a non-variable term that may be in untranslated form;
guard-debug is
typically nil but may be t (see guard-debug); ctx is a context
(typically, a symbol used in error and warning messages); and state
references the ACL2 state.If you want to obtain the formula but you don't care about the so-called ``tag tree'':
(mv-let (erp val state)
(guard-obligation x guard-debug 'top-level state)
(if erp
( .. code for handling error case, e.g., name is undefined .. )
(let ((cl-set (cadr val))) ; to be proved for guard verification
( .. code using cl-set, which is a list of clauses,
implicitly conjoined, each of which is viewed as
a disjunction .. ))))
The form (guard-obligation x guard-debug ctx state) evaluates to a triple
(mv erp val state), where erp is nil unless there is an error,
and state is the ACL2 state. Suppose erp is nil. Then val
is the keyword :redundant if the corresponding verify-guards event
would be redundant; see redundant-events. Otherwise, val is a tuple
(list* names cl-set ttree), where: names is (cons :term xt) if
x is not a variable, where xt is the translated form of x; and
otherwise is a list containing x along with, if x is defined in a
mutual-recursion, any other functions defined in the same
mutual-recursion nest; cl-set is a list of lists of terms, viewed
as a conjunction of clauses (each viewed (as a disjunction); and ttree is
an assumption-free tag-tree that justifies cl-set. (The notion of
``tag-tree'' may probably be ignored except for system developers.)
Guard-obligation is typically used for function names or non-variable
terms, but as for verify-guards, it may also be applied to theorem
names.
See the source code for verify-guards-formula for an example of how to
use guard-obligation.
