		Search-engine friendly clone of the ACL2 documentation.

Cutinfo

Cutinfo->score

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

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

Definitions and Theorems

Function: cutinfo->score

(defun cutinfo->score (x)
  (declare (xargs :guard (cutinfo-p x)))
  (mbe :logic
       (let ((x (cutinfo-fix x)))
         (part-select x :low 20 :width 12))
       :exec (the (unsigned-byte 12)
                  (logand (the (unsigned-byte 12) 4095)
                          (the (unsigned-byte 12)
                               (ash (the (unsigned-byte 32) x)
                                    -20))))))

Theorem: cutscore-p-of-cutinfo->score

(defthm cutscore-p-of-cutinfo->score
  (b* ((score (cutinfo->score x)))
    (cutscore-p score))
  :rule-classes :rewrite)

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

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

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

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

Theorem: cutinfo->score-of-cutinfo

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

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

(defthm cutinfo->score-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) 4293918720)
           0))
  (equal (cutinfo->score x)
         (cutinfo->score acl2::y))))