		Search-engine friendly clone of the ACL2 documentation.

4vec-operations

4vec-override

Resolution for when one signal is stronger than the other.

Signature
(4vec-override stronger weaker) → res
Arguments: stronger — Guard (4vec-p stronger).; weaker — Guard (4vec-p weaker).
Returns: res — Type (4vec-p res).

(4vec-override stronger weaker) takes the value of stronger for each of its non-Z bits, and the value of weaker for bits where stronger is Z.

Definitions and Theorems

Function: 4vec-override

(defun 4vec-override (stronger weaker)
  (declare (xargs :guard (and (4vec-p stronger)
                              (4vec-p weaker))))
  (let ((__function__ '4vec-override))
    (declare (ignorable __function__))
    (b* (((4vec stronger)) ((4vec weaker)))
      (mbe :logic
           (b* ((stronger-z (logand stronger.lower
                                    (lognot stronger.upper))))
             (4vec (logior (logand stronger-z weaker.upper)
                           (logand (lognot stronger-z)
                                   stronger.upper))
                   (logior (logand stronger-z weaker.lower)
                           (logand (lognot stronger-z)
                                   stronger.lower))))
           :exec (4vec (logior (logand stronger.lower weaker.upper)
                               stronger.upper)
                       (logand (logior stronger.upper weaker.lower)
                               stronger.lower))))))

Theorem: 4vec-p-of-4vec-override

(defthm 4vec-p-of-4vec-override
  (b* ((res (4vec-override stronger weaker)))
    (4vec-p res))
  :rule-classes :rewrite)

Theorem: 4vec-override-associative

(defthm 4vec-override-associative
  (equal (4vec-override (4vec-override x y) z)
         (4vec-override x (4vec-override y z))))

Theorem: 4vec-override-of-4vec-fix-stronger

(defthm 4vec-override-of-4vec-fix-stronger
  (equal (4vec-override (4vec-fix stronger)
                        weaker)
         (4vec-override stronger weaker)))

Theorem: 4vec-override-4vec-equiv-congruence-on-stronger

(defthm 4vec-override-4vec-equiv-congruence-on-stronger
  (implies (4vec-equiv stronger stronger-equiv)
           (equal (4vec-override stronger weaker)
                  (4vec-override stronger-equiv weaker)))
  :rule-classes :congruence)

Theorem: 4vec-override-of-4vec-fix-weaker

(defthm 4vec-override-of-4vec-fix-weaker
  (equal (4vec-override stronger (4vec-fix weaker))
         (4vec-override stronger weaker)))

Theorem: 4vec-override-4vec-equiv-congruence-on-weaker

(defthm 4vec-override-4vec-equiv-congruence-on-weaker
  (implies (4vec-equiv weaker weaker-equiv)
           (equal (4vec-override stronger weaker)
                  (4vec-override stronger weaker-equiv)))
  :rule-classes :congruence)