		Search-engine friendly clone of the ACL2 documentation.

3vec

3vec-fix

Coerces an arbitrary 4vec to a 3vec by ``unfloating'' it, i.e., by turning any Zs into Xes.

Signature
(3vec-fix x) → x-fix
Arguments: x — Guard (4vec-p x).
Returns: x-fix — Type (3vec-p! x-fix).

In most logic gates, e.g., AND gates, inputs that are Z are treated just the same as inputs that are X. So, when we define 4vec-operations like 4vec-bitand, we typically just:

Define a 3vec version of the operation, then
Invoke the 3vec version on the unfloats of the inputs.

Definitions and Theorems

Function: 3vec-fix

(defun 3vec-fix (x)
  (declare (xargs :guard (4vec-p x)))
  (let ((__function__ '3vec-fix))
    (declare (ignorable __function__))
    (if-2vec-p (x)
               (2vec (2vec->val x))
               (mbe :logic
                    (b* (((4vec x) x))
                      (4vec (logior x.upper x.lower)
                            (logand x.upper x.lower)))
                    :exec
                    (if (3vec-p x)
                        x
                      (b* (((4vec x) x))
                        (4vec (logior x.upper x.lower)
                              (logand x.upper x.lower))))))))

Theorem: 3vec-p!-of-3vec-fix

(defthm 3vec-p!-of-3vec-fix
  (b* ((x-fix (3vec-fix x)))
    (3vec-p! x-fix))
  :rule-classes :rewrite)

Theorem: 3vec-fix-of-3vec-p

(defthm 3vec-fix-of-3vec-p
  (implies (3vec-p x)
           (equal (3vec-fix x) (4vec-fix x))))

Theorem: 3vec-fix-of-4vec-fix-x

(defthm 3vec-fix-of-4vec-fix-x
  (equal (3vec-fix (4vec-fix x))
         (3vec-fix x)))

Theorem: 3vec-fix-4vec-equiv-congruence-on-x

(defthm 3vec-fix-4vec-equiv-congruence-on-x
  (implies (4vec-equiv x x-equiv)
           (equal (3vec-fix x) (3vec-fix x-equiv)))
  :rule-classes :congruence)

Theorem: 3vec-fix-idempotent

(defthm 3vec-fix-idempotent
  (equal (3vec-fix (3vec-fix x))
         (3vec-fix x)))