		Search-engine friendly clone of the ACL2 documentation.

Cutinfo

!cutinfo->score

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

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

Definitions and Theorems

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