		Search-engine friendly clone of the ACL2 documentation.

Cutinfo

Cutinfo->size

Access the |AIGNET|::|SIZE| field of a cutinfo bit structure.

Signature
(cutinfo->size x) → size
Arguments: x — Guard (cutinfo-p x).
Returns: size — Type (cutsize-p size).

Definitions and Theorems

Function: cutinfo->size

(defun cutinfo->size (x)
  (declare (xargs :guard (cutinfo-p x)))
  (mbe :logic
       (let ((x (cutinfo-fix x)))
         (part-select x :low 16 :width 3))
       :exec (the (unsigned-byte 3)
                  (logand (the (unsigned-byte 3) 7)
                          (the (unsigned-byte 16)
                               (ash (the (unsigned-byte 32) x)
                                    -16))))))

Theorem: cutsize-p-of-cutinfo->size

(defthm cutsize-p-of-cutinfo->size
  (b* ((size (cutinfo->size x)))
    (cutsize-p size))
  :rule-classes :rewrite)

Theorem: cutinfo->size-of-cutinfo-fix-x

(defthm cutinfo->size-of-cutinfo-fix-x
  (equal (cutinfo->size (cutinfo-fix x))
         (cutinfo->size x)))

Theorem: cutinfo->size-cutinfo-equiv-congruence-on-x

(defthm cutinfo->size-cutinfo-equiv-congruence-on-x
  (implies (cutinfo-equiv x x-equiv)
           (equal (cutinfo->size x)
                  (cutinfo->size x-equiv)))
  :rule-classes :congruence)

Theorem: cutinfo->size-of-cutinfo

(defthm cutinfo->size-of-cutinfo
  (equal (cutinfo->size (cutinfo truth size valid score))
         (cutsize-fix size)))

Theorem: cutinfo->size-of-write-with-mask

(defthm cutinfo->size-of-write-with-mask
 (implies
  (and
    (fty::bitstruct-read-over-write-hyps x cutinfo-equiv-under-mask)
    (cutinfo-equiv-under-mask x acl2::y fty::mask)
    (equal (logand (lognot fty::mask) 458752)
           0))
  (equal (cutinfo->size x)
         (cutinfo->size acl2::y))))