		Search-engine friendly clone of the ACL2 documentation.

Undocumented

Cutinfo

An 32-bit unsigned bitstruct type.

This is a bitstruct type introduced by fty::defbitstruct, represented as a unsigned 32-bit integer.

Fields

truth — truth::truth4
size — cutsize
valid — boolean
score — cutscore

Definitions and Theorems

Function: cutinfo-p

(defun cutinfo-p (x)
       (declare (xargs :guard t))
       (let ((__function__ 'cutinfo-p))
            (declare (ignorable __function__))
            (and (mbe :logic (unsigned-byte-p 32 x)
                      :exec (and (natp x) (< x 4294967296)))
                 (cutsize-p (part-select x :low 16 :width 3)))))

Theorem: unsigned-byte-p-when-cutinfo-p

(defthm unsigned-byte-p-when-cutinfo-p
        (implies (cutinfo-p x)
                 (unsigned-byte-p 32 x)))

Theorem: cutinfo-p-compound-recognizer

(defthm cutinfo-p-compound-recognizer
        (implies (cutinfo-p x) (natp x))
        :rule-classes :compound-recognizer)

Function: cutinfo-fix

(defun
 cutinfo-fix (x)
 (declare (xargs :guard (cutinfo-p x)))
 (let
  ((__function__ 'cutinfo-fix))
  (declare (ignorable __function__))
  (mbe
   :logic
   (loghead
      32
      (logapp 16 (part-select x :width 16 :low 0)
              (logapp 3
                      (cutsize-fix (part-select x :width 3 :low 16))
                      (logapp 1 (part-select x :width 1 :low 19)
                              (part-select x :width 12 :low 20)))))
   :exec x)))

Theorem: cutinfo-p-of-cutinfo-fix

(defthm cutinfo-p-of-cutinfo-fix
        (b* ((fty::fixed (cutinfo-fix x)))
            (cutinfo-p fty::fixed))
        :rule-classes :rewrite)

Theorem: cutinfo-fix-when-cutinfo-p

(defthm cutinfo-fix-when-cutinfo-p
        (implies (cutinfo-p x)
                 (equal (cutinfo-fix x) x)))

Function: cutinfo-equiv$inline

(defun cutinfo-equiv$inline (x acl2::y)
       (declare (xargs :guard (and (cutinfo-p x)
                                   (cutinfo-p acl2::y))))
       (equal (cutinfo-fix x)
              (cutinfo-fix acl2::y)))

Theorem: cutinfo-equiv-is-an-equivalence

(defthm cutinfo-equiv-is-an-equivalence
        (and (booleanp (cutinfo-equiv x y))
             (cutinfo-equiv x x)
             (implies (cutinfo-equiv x y)
                      (cutinfo-equiv y x))
             (implies (and (cutinfo-equiv x y)
                           (cutinfo-equiv y z))
                      (cutinfo-equiv x z)))
        :rule-classes (:equivalence))

Theorem: cutinfo-equiv-implies-equal-cutinfo-fix-1

(defthm cutinfo-equiv-implies-equal-cutinfo-fix-1
        (implies (cutinfo-equiv x x-equiv)
                 (equal (cutinfo-fix x)
                        (cutinfo-fix x-equiv)))
        :rule-classes (:congruence))

Theorem: cutinfo-fix-under-cutinfo-equiv

(defthm cutinfo-fix-under-cutinfo-equiv
        (cutinfo-equiv (cutinfo-fix x) x)
        :rule-classes (:rewrite :rewrite-quoted-constant))

Theorem: cutinfo-fix-of-cutinfo-fix-x

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

Theorem: cutinfo-fix-cutinfo-equiv-congruence-on-x

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

Function: cutinfo

(defun cutinfo (truth size valid score)
       (declare (xargs :guard (and (truth::truth4-p truth)
                                   (cutsize-p size)
                                   (booleanp valid)
                                   (cutscore-p score))))
       (let ((__function__ 'cutinfo))
            (declare (ignorable __function__))
            (b* ((truth (mbe :logic (truth::truth4-fix$ truth)
                             :exec truth))
                 (size (mbe :logic (cutsize-fix size)
                            :exec size))
                 (valid (bool->bit valid))
                 (score (mbe :logic (cutscore-fix score)
                             :exec score)))
                (logapp 16 truth
                        (logapp 3 size (logapp 1 valid score))))))

Theorem: cutinfo-p-of-cutinfo

(defthm cutinfo-p-of-cutinfo
        (b* ((cutinfo (cutinfo truth size valid score)))
            (cutinfo-p cutinfo))
        :rule-classes :rewrite)

Theorem: cutinfo-of-truth4-fix$-truth

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

Theorem: cutinfo-truth4-equiv-congruence-on-truth

(defthm cutinfo-truth4-equiv-congruence-on-truth
        (implies (truth::truth4-equiv truth truth-equiv)
                 (equal (cutinfo truth size valid score)
                        (cutinfo truth-equiv size valid score)))
        :rule-classes :congruence)

Theorem: cutinfo-of-cutsize-fix-size

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

Theorem: cutinfo-cutsize-equiv-congruence-on-size

(defthm cutinfo-cutsize-equiv-congruence-on-size
        (implies (cutsize-equiv size size-equiv)
                 (equal (cutinfo truth size valid score)
                        (cutinfo truth size-equiv valid score)))
        :rule-classes :congruence)

Theorem: cutinfo-of-bool-fix-valid

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

Theorem: cutinfo-iff-congruence-on-valid

(defthm cutinfo-iff-congruence-on-valid
        (implies (iff valid valid-equiv)
                 (equal (cutinfo truth size valid score)
                        (cutinfo truth size valid-equiv score)))
        :rule-classes :congruence)

Theorem: cutinfo-of-cutscore-fix-score

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

Theorem: cutinfo-cutscore-equiv-congruence-on-score

(defthm cutinfo-cutscore-equiv-congruence-on-score
        (implies (cutscore-equiv score score-equiv)
                 (equal (cutinfo truth size valid score)
                        (cutinfo truth size valid score-equiv)))
        :rule-classes :congruence)

Function: cutinfo-equiv-under-mask

(defun cutinfo-equiv-under-mask (x x1 mask)
       (declare (xargs :guard (and (cutinfo-p x)
                                   (cutinfo-p x1)
                                   (integerp mask))))
       (let ((__function__ 'cutinfo-equiv-under-mask))
            (declare (ignorable __function__))
            (fty::int-equiv-under-mask (cutinfo-fix x)
                                       (cutinfo-fix x1)
                                       mask)))

Theorem: cutinfo-equiv-under-mask-of-cutinfo-fix-x

(defthm cutinfo-equiv-under-mask-of-cutinfo-fix-x
        (equal (cutinfo-equiv-under-mask (cutinfo-fix x)
                                         x1 mask)
               (cutinfo-equiv-under-mask x x1 mask)))

Theorem: cutinfo-equiv-under-mask-cutinfo-equiv-congruence-on-x

(defthm cutinfo-equiv-under-mask-cutinfo-equiv-congruence-on-x
        (implies (cutinfo-equiv x x-equiv)
                 (equal (cutinfo-equiv-under-mask x x1 mask)
                        (cutinfo-equiv-under-mask x-equiv x1 mask)))
        :rule-classes :congruence)

Theorem: cutinfo-equiv-under-mask-of-cutinfo-fix-x1

(defthm cutinfo-equiv-under-mask-of-cutinfo-fix-x1
        (equal (cutinfo-equiv-under-mask x (cutinfo-fix x1)
                                         mask)
               (cutinfo-equiv-under-mask x x1 mask)))

Theorem: cutinfo-equiv-under-mask-cutinfo-equiv-congruence-on-x1

(defthm cutinfo-equiv-under-mask-cutinfo-equiv-congruence-on-x1
        (implies (cutinfo-equiv x1 x1-equiv)
                 (equal (cutinfo-equiv-under-mask x x1 mask)
                        (cutinfo-equiv-under-mask x x1-equiv mask)))
        :rule-classes :congruence)

Theorem: cutinfo-equiv-under-mask-of-ifix-mask

(defthm cutinfo-equiv-under-mask-of-ifix-mask
        (equal (cutinfo-equiv-under-mask x x1 (ifix mask))
               (cutinfo-equiv-under-mask x x1 mask)))

Theorem: cutinfo-equiv-under-mask-int-equiv-congruence-on-mask

(defthm cutinfo-equiv-under-mask-int-equiv-congruence-on-mask
        (implies (int-equiv mask mask-equiv)
                 (equal (cutinfo-equiv-under-mask x x1 mask)
                        (cutinfo-equiv-under-mask x x1 mask-equiv)))
        :rule-classes :congruence)

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))))

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))))

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))))

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))))

Theorem: cutinfo-fix-in-terms-of-cutinfo

(defthm cutinfo-fix-in-terms-of-cutinfo
        (equal (cutinfo-fix x)
               (change-cutinfo x)))

Function: !cutinfo->truth

(defun
 !cutinfo->truth (truth x)
 (declare (xargs :guard (and (truth::truth4-p truth)
                             (cutinfo-p x))))
 (mbe
     :logic (b* ((truth (mbe :logic (truth::truth4-fix$ truth)
                             :exec truth))
                 (x (cutinfo-fix x)))
                (part-install truth x :width 16 :low 0))
     :exec (the (unsigned-byte 32)
                (logior (the (unsigned-byte 32)
                             (logand (the (unsigned-byte 32) x)
                                     (the (signed-byte 17) -65536)))
                        (the (unsigned-byte 16) truth)))))

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

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

Theorem: !cutinfo->truth-of-truth4-fix$-truth

(defthm !cutinfo->truth-of-truth4-fix$-truth
        (equal (!cutinfo->truth (truth::truth4-fix$ truth)
                                x)
               (!cutinfo->truth truth x)))

Theorem: !cutinfo->truth-truth4-equiv-congruence-on-truth

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

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

(defthm !cutinfo->truth-of-cutinfo-fix-x
        (equal (!cutinfo->truth truth (cutinfo-fix x))
               (!cutinfo->truth 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 truth x)
                        (!cutinfo->truth truth x-equiv)))
        :rule-classes :congruence)

Theorem: !cutinfo->truth-is-cutinfo

(defthm !cutinfo->truth-is-cutinfo
        (equal (!cutinfo->truth truth x)
               (change-cutinfo x :truth truth)))

Theorem: cutinfo->truth-of-!cutinfo->truth

(defthm cutinfo->truth-of-!cutinfo->truth
        (b* ((?new-x (!cutinfo->truth truth x)))
            (equal (cutinfo->truth new-x)
                   (truth::truth4-fix$ truth))))

Theorem: !cutinfo->truth-equiv-under-mask

(defthm !cutinfo->truth-equiv-under-mask
        (b* ((?new-x (!cutinfo->truth truth x)))
            (cutinfo-equiv-under-mask new-x x -65536)))

Function: !cutinfo->size

(defun
 !cutinfo->size (size x)
 (declare (xargs :guard (and (cutsize-p size) (cutinfo-p x))))
 (mbe
    :logic (b* ((size (mbe :logic (cutsize-fix size)
                           :exec size))
                (x (cutinfo-fix x)))
               (part-install size x :width 3 :low 16))
    :exec (the (unsigned-byte 32)
               (logior (the (unsigned-byte 32)
                            (logand (the (unsigned-byte 32) x)
                                    (the (signed-byte 20) -458753)))
                       (the (unsigned-byte 19)
                            (ash (the (unsigned-byte 3) size)
                                 16))))))

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

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

Theorem: !cutinfo->size-of-cutsize-fix-size

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

Theorem: !cutinfo->size-cutsize-equiv-congruence-on-size

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

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

(defthm !cutinfo->size-of-cutinfo-fix-x
        (equal (!cutinfo->size size (cutinfo-fix x))
               (!cutinfo->size 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 size x)
                        (!cutinfo->size size x-equiv)))
        :rule-classes :congruence)

Theorem: !cutinfo->size-is-cutinfo

(defthm !cutinfo->size-is-cutinfo
        (equal (!cutinfo->size size x)
               (change-cutinfo x :size size)))

Theorem: cutinfo->size-of-!cutinfo->size

(defthm cutinfo->size-of-!cutinfo->size
        (b* ((?new-x (!cutinfo->size size x)))
            (equal (cutinfo->size new-x)
                   (cutsize-fix size))))

Theorem: !cutinfo->size-equiv-under-mask

(defthm !cutinfo->size-equiv-under-mask
        (b* ((?new-x (!cutinfo->size size x)))
            (cutinfo-equiv-under-mask new-x x -458753)))

Function: !cutinfo->valid

(defun
 !cutinfo->valid (valid x)
 (declare (xargs :guard (and (booleanp valid) (cutinfo-p x))))
 (mbe
    :logic (b* ((valid (bool->bit valid))
                (x (cutinfo-fix x)))
               (part-install valid x :width 1 :low 19))
    :exec (the (unsigned-byte 32)
               (logior (the (unsigned-byte 32)
                            (logand (the (unsigned-byte 32) x)
                                    (the (signed-byte 21) -524289)))
                       (the (unsigned-byte 20)
                            (ash (the (unsigned-byte 1)
                                      (bool->bit valid))
                                 19))))))

Theorem: cutinfo-p-of-!cutinfo->valid

(defthm cutinfo-p-of-!cutinfo->valid
        (b* ((new-x (!cutinfo->valid valid x)))
            (cutinfo-p new-x))
        :rule-classes :rewrite)

Theorem: !cutinfo->valid-of-bool-fix-valid

(defthm !cutinfo->valid-of-bool-fix-valid
        (equal (!cutinfo->valid (acl2::bool-fix valid)
                                x)
               (!cutinfo->valid valid x)))

Theorem: !cutinfo->valid-iff-congruence-on-valid

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

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

(defthm !cutinfo->valid-of-cutinfo-fix-x
        (equal (!cutinfo->valid valid (cutinfo-fix x))
               (!cutinfo->valid 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 valid x)
                        (!cutinfo->valid valid x-equiv)))
        :rule-classes :congruence)

Theorem: !cutinfo->valid-is-cutinfo

(defthm !cutinfo->valid-is-cutinfo
        (equal (!cutinfo->valid valid x)
               (change-cutinfo x :valid valid)))

Theorem: cutinfo->valid-of-!cutinfo->valid

(defthm cutinfo->valid-of-!cutinfo->valid
        (b* ((?new-x (!cutinfo->valid valid x)))
            (equal (cutinfo->valid new-x)
                   (acl2::bool-fix valid))))

Theorem: !cutinfo->valid-equiv-under-mask

(defthm !cutinfo->valid-equiv-under-mask
        (b* ((?new-x (!cutinfo->valid valid x)))
            (cutinfo-equiv-under-mask new-x x -524289)))

Function: !cutinfo->score

(defun
 !cutinfo->score (score x)
 (declare (xargs :guard (and (cutscore-p score) (cutinfo-p x))))
 (mbe :logic (b* ((score (mbe :logic (cutscore-fix score)
                              :exec score))
                  (x (cutinfo-fix x)))
                 (part-install score x
                               :width 12
                               :low 20))
      :exec
      (the (unsigned-byte 32)
           (logior (the (unsigned-byte 32)
                        (logand (the (unsigned-byte 32) x)
                                (the (signed-byte 33) -4293918721)))
                   (the (unsigned-byte 32)
                        (ash (the (unsigned-byte 12) score)
                             20))))))

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

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

Theorem: !cutinfo->score-of-cutscore-fix-score

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

Theorem: !cutinfo->score-cutscore-equiv-congruence-on-score

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

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

(defthm !cutinfo->score-of-cutinfo-fix-x
        (equal (!cutinfo->score score (cutinfo-fix x))
               (!cutinfo->score 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 score x)
                        (!cutinfo->score score x-equiv)))
        :rule-classes :congruence)

Theorem: !cutinfo->score-is-cutinfo

(defthm !cutinfo->score-is-cutinfo
        (equal (!cutinfo->score score x)
               (change-cutinfo x :score score)))

Theorem: cutinfo->score-of-!cutinfo->score

(defthm cutinfo->score-of-!cutinfo->score
        (b* ((?new-x (!cutinfo->score score x)))
            (equal (cutinfo->score new-x)
                   (cutscore-fix score))))

Theorem: !cutinfo->score-equiv-under-mask

(defthm !cutinfo->score-equiv-under-mask
        (b* ((?new-x (!cutinfo->score score x)))
            (cutinfo-equiv-under-mask new-x x 1048575)))

Function: cutinfo-debug

(defun
   cutinfo-debug (x)
   (declare (xargs :guard (cutinfo-p x)))
   (let ((__function__ 'cutinfo-debug))
        (declare (ignorable __function__))
        (b* (((cutinfo x)))
            (cons (cons 'truth x.truth)
                  (cons (cons 'size x.size)
                        (cons (cons 'valid x.valid)
                              (cons (cons 'score x.score) nil)))))))

Theorem: cutinfo-debug-of-cutinfo-fix-x

(defthm cutinfo-debug-of-cutinfo-fix-x
        (equal (cutinfo-debug (cutinfo-fix x))
               (cutinfo-debug x)))

Theorem: cutinfo-debug-cutinfo-equiv-congruence-on-x

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

Subtopics

!cutinfo->score: Update the |AIGNET|::|SCORE| field of a cutinfo bit structure.
!cutinfo->valid: Update the |AIGNET|::|VALID| field of a cutinfo bit structure.
!cutinfo->truth: Update the |AIGNET|::|TRUTH| field of a cutinfo bit structure.
!cutinfo->size: Update the |AIGNET|::|SIZE| field of a cutinfo bit structure.
Cutinfo-fix: Fixing function for cutinfo bit structures.
Cutinfo-p: Recognizer for cutinfo bit structures.
Cutinfo->valid: Access the |AIGNET|::|VALID| field of a cutinfo bit structure.
Cutinfo->truth: Access the |AIGNET|::|TRUTH| field of a cutinfo bit structure.
Cutinfo->size: Access the |AIGNET|::|SIZE| field of a cutinfo bit structure.
Cutinfo->score: Access the |AIGNET|::|SCORE| field of a cutinfo bit structure.