guard-theorem-no-simplify

(in-package "ACL2")

(defsection guard-theorem-no-simplify
  :parents (std/system/function-queries)
  :short "A version of @(tsee guard-theorem) that does no simplification."
  :long (topstring (p "This definition is based on
     the definition of ACL2 source function @('guard-theorem'),
     with the @('simplify') argument set to @('nil'),
     with no state argument,
     and with new @('safe-mode') and @('gc-off') arguments;
     the latter two can reasonably be
     @('(f-get-global 'safe-mode state)') and @('(gc-off state)'),
     respectively.")
    (p "An advantage of not having the state argument is that
     this function can be called via @(tsee magic-ev-fncall)."))
  (defun guard-theorem-no-simplify
    (fn guard-debug wrld safe-mode gc-off)
    (declare (xargs :mode :program))
    (cond ((not (getpropc fn 'unnormalized-body nil wrld)) *t*)
      (t (let ((names (or (getpropc fn 'recursivep nil wrld) (list fn))))
          (mv-let (cl-set ttree)
            (guard-clauses-for-clique names
              guard-debug
              :do-not-simplify wrld
              safe-mode
              gc-off
              nil)
            (declare (ignore ttree))
            (termify-clause-set cl-set)))))))