• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Community
    • Proof-automation
    • Macro-libraries
      • B*
      • Defunc
      • Fty
      • Apt
        • Simplify-defun
        • Isodata
        • Tailrec
        • Schemalg
        • Restrict
          • Restrict-implementation
            • Restrict-event-generation
              • Restrict-gen-verify-guards
              • Restrict-gen-everything
              • Restrict-gen-old-to-new
              • Restrict-gen-new
              • Restrict-gen-restriction-of-rec-calls-consequent-term
              • Restrict-gen-new-to-old
              • Restrict-gen-appconds
                • Restrict-gen-restriction-of-rec-calls-consequent-term-aux
              • Restrict-fn
              • Restrict-macro-definition
              • Restrict-input-processing
          • Expdata
          • Casesplit
          • Simplify-term
          • Simplify-defun-sk
          • Parteval
          • Solve
          • Wrap-output
          • Propagate-iso
          • Simplify
          • Finite-difference
          • Drop-irrelevant-params
          • Copy-function
          • Lift-iso
          • Rename-params
          • Utilities
          • Simplify-term-programmatic
          • Simplify-defun-sk-programmatic
          • Simplify-defun-programmatic
          • Simplify-defun+
          • Common-options
          • Common-concepts
        • Std/util
        • Defdata
        • Defrstobj
        • Seq
        • Match-tree
        • Defrstobj
        • With-supporters
        • Def-partial-measure
        • Template-subst
        • Soft
        • Defthm-domain
        • Event-macros
        • Def-universal-equiv
        • Def-saved-obligs
        • With-supporters-after
        • Definec
        • Sig
        • Outer-local
        • Data-structures
      • ACL2
      • Interfacing-tools
      • Hardware-verification
      • Software-verification
      • Math
      • Testing-utilities
    • 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)))))