		Search-engine friendly clone of the ACL2 documentation.

Restrict-event-generation

Restrict-gen-appconds

Generate the applicability conditions.

Signature
(restrict-gen-appconds old restriction verify-guards stub? state) → appconds
Arguments: old — Guard (symbolp old).; restriction — Guard (pseudo-termp restriction).; verify-guards — Guard (booleanp verify-guards).; stub? — Guard (symbolp stub?).
Returns: appconds — A evmac-appcond-listp.

We retrieve the guard with limited simplification, for greater predictability and robustness. This is matched by the fact that we verify guards with limited simplification, in restrict-gen-verify-guards.

Definitions and Theorems

Function: restrict-gen-appconds

(defun restrict-gen-appconds
       (old restriction verify-guards stub? state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (and (symbolp old)
                             (pseudo-termp restriction)
                             (booleanp verify-guards)
                             (symbolp stub?))))
 (let ((__function__ 'restrict-gen-appconds))
  (declare (ignorable __function__))
  (b* ((wrld (w state)))
   (append
    (make-evmac-appcond?
         :restriction-of-rec-calls
         (b* ((rec-calls-with-tests (recursive-calls old wrld))
              (consequent (restrict-gen-restriction-of-rec-calls-consequent-term
                               old rec-calls-with-tests
                               restriction stub? wrld)))
           (implicate restriction consequent))
         :when (recursivep old nil wrld))
    (make-evmac-appcond?
      :restriction-guard
      (b*
        ((old-guard (guard old nil wrld))
         (restriction-guard (term-guard-obligation restriction
                                                   :limited state)))
        (implicate old-guard restriction-guard))
      :when verify-guards)))))