		Search-engine friendly clone of the ACL2 documentation.

Cutinfo

Cutinfo->valid

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

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

Definitions and Theorems

Function: cutinfo->valid

(defun cutinfo->valid (x)
 (declare (xargs :guard (cutinfo-p x)))
 (mbe
  :logic
  (let ((x (cutinfo-fix x)))
    (bit->bool (part-select x :low 19 :width 1)))
  :exec (bit->bool (the (unsigned-byte 1)
                        (logand (the (unsigned-byte 1) 1)
                                (the (unsigned-byte 13)
                                     (ash (the (unsigned-byte 32) x)
                                          -19)))))))

Theorem: booleanp-of-cutinfo->valid

(defthm booleanp-of-cutinfo->valid
  (b* ((valid (cutinfo->valid x)))
    (booleanp valid))
  :rule-classes :rewrite)

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

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

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

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

Theorem: cutinfo->valid-of-cutinfo

(defthm cutinfo->valid-of-cutinfo
  (equal (cutinfo->valid (cutinfo truth size valid score))
         (acl2::bool-fix valid)))

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

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