		Search-engine friendly clone of the ACL2 documentation.

Cutinfo

Cutinfo->truth

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

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

Definitions and Theorems

Function: cutinfo->truth

(defun cutinfo->truth (x)
  (declare (xargs :guard (cutinfo-p x)))
  (mbe :logic
       (let ((x (cutinfo-fix x)))
         (part-select x :low 0 :width 16))
       :exec (the (unsigned-byte 16)
                  (logand (the (unsigned-byte 16) 65535)
                          (the (unsigned-byte 32) x)))))

Theorem: truth4-p-of-cutinfo->truth

(defthm truth4-p-of-cutinfo->truth
  (b* ((truth (cutinfo->truth x)))
    (truth::truth4-p truth))
  :rule-classes :rewrite)

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

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

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

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

Theorem: cutinfo->truth-of-cutinfo

(defthm cutinfo->truth-of-cutinfo
  (equal (cutinfo->truth (cutinfo truth size valid score))
         (truth::truth4-fix$ truth)))

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

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