		Search-engine friendly clone of the ACL2 documentation.

Interp-flags

!interp-flags->trace-rewrites

Update the |FGL|::|TRACE-REWRITES| field of a interp-flags bit structure.

Signature
(!interp-flags->trace-rewrites trace-rewrites x) → new-x
Arguments: trace-rewrites — Guard (booleanp trace-rewrites).; x — Guard (interp-flags-p x).
Returns: new-x — Type (interp-flags-p new-x).

Definitions and Theorems

Function: !interp-flags->trace-rewrites

(defun !interp-flags->trace-rewrites (trace-rewrites x)
  (declare (xargs :guard (and (booleanp trace-rewrites)
                              (interp-flags-p x))))
  (mbe :logic
       (b* ((trace-rewrites (bool->bit trace-rewrites))
            (x (interp-flags-fix x)))
         (acl2::part-install trace-rewrites x
                             :width 1
                             :low 3))
       :exec (the (unsigned-byte 6)
                  (logior (the (unsigned-byte 6)
                               (logand (the (unsigned-byte 6) x)
                                       (the (signed-byte 5) -9)))
                          (the (unsigned-byte 4)
                               (ash (the (unsigned-byte 1)
                                         (bool->bit trace-rewrites))
                                    3))))))

Theorem: interp-flags-p-of-!interp-flags->trace-rewrites

(defthm interp-flags-p-of-!interp-flags->trace-rewrites
  (b* ((new-x (!interp-flags->trace-rewrites trace-rewrites x)))
    (interp-flags-p new-x))
  :rule-classes :rewrite)

Theorem: !interp-flags->trace-rewrites-of-bool-fix-trace-rewrites

(defthm !interp-flags->trace-rewrites-of-bool-fix-trace-rewrites
  (equal (!interp-flags->trace-rewrites (bool-fix trace-rewrites)
                                        x)
         (!interp-flags->trace-rewrites trace-rewrites x)))

Theorem: !interp-flags->trace-rewrites-iff-congruence-on-trace-rewrites

(defthm
     !interp-flags->trace-rewrites-iff-congruence-on-trace-rewrites
 (implies
     (iff trace-rewrites trace-rewrites-equiv)
     (equal (!interp-flags->trace-rewrites trace-rewrites x)
            (!interp-flags->trace-rewrites trace-rewrites-equiv x)))
 :rule-classes :congruence)

Theorem: !interp-flags->trace-rewrites-of-interp-flags-fix-x

(defthm !interp-flags->trace-rewrites-of-interp-flags-fix-x
  (equal (!interp-flags->trace-rewrites
              trace-rewrites (interp-flags-fix x))
         (!interp-flags->trace-rewrites trace-rewrites x)))

Theorem: !interp-flags->trace-rewrites-interp-flags-equiv-congruence-on-x

(defthm
   !interp-flags->trace-rewrites-interp-flags-equiv-congruence-on-x
 (implies
     (interp-flags-equiv x x-equiv)
     (equal (!interp-flags->trace-rewrites trace-rewrites x)
            (!interp-flags->trace-rewrites trace-rewrites x-equiv)))
 :rule-classes :congruence)

Theorem: !interp-flags->trace-rewrites-is-interp-flags

(defthm !interp-flags->trace-rewrites-is-interp-flags
  (equal (!interp-flags->trace-rewrites trace-rewrites x)
         (change-interp-flags x
                              :trace-rewrites trace-rewrites)))

Theorem: interp-flags->trace-rewrites-of-!interp-flags->trace-rewrites

(defthm
      interp-flags->trace-rewrites-of-!interp-flags->trace-rewrites
  (b* ((?new-x (!interp-flags->trace-rewrites trace-rewrites x)))
    (equal (interp-flags->trace-rewrites new-x)
           (bool-fix trace-rewrites))))

Theorem: !interp-flags->trace-rewrites-equiv-under-mask

(defthm !interp-flags->trace-rewrites-equiv-under-mask
  (b* ((?new-x (!interp-flags->trace-rewrites trace-rewrites x)))
    (interp-flags-equiv-under-mask new-x x -9)))