		Search-engine friendly clone of the ACL2 documentation.

4vec-operations

4vec-bit?

Bitwise multiple if-then-elses of 4vecs; doesn't unfloat then/else values.

Signature
(4vec-bit? tests thens elses) → choices
Arguments: tests — Guard (4vec-p tests).; thens — Guard (4vec-p thens).; elses — Guard (4vec-p elses).
Returns: choices — Type (4vec-p choices).

We carry out an independent if-then-else for each bit of tests, thens, and elses, producing a new vector with all of the answers. This result is computed bit by bit, with result[i] being set to:

thens[i] if tests[i] is 1,
elses[i] if tests[i] is 0, or
the merger of thens[i] and elses[i], otherwise.

This merging is just x if the bits are different, or the agreed upon value otherwise.

BOZO. This operation is not very conservative. In particular, Z values are passed through without unfloating them, and can even be merged without unfloating. BOZO Consider how and whether Issue 384 (see 4vec-?) should affect this operation and update the docs accordingly once it's fixed.

Definitions and Theorems

Function: 4vec-bit?

(defun 4vec-bit? (tests thens elses)
  (declare (xargs :guard (and (4vec-p tests)
                              (4vec-p thens)
                              (4vec-p elses))))
  (let ((__function__ '4vec-bit?))
    (declare (ignorable __function__))
    (3vec-bit? (3vec-fix tests)
               thens elses)))

Theorem: 4vec-p-of-4vec-bit?

(defthm 4vec-p-of-4vec-bit?
  (b* ((choices (4vec-bit? tests thens elses)))
    (4vec-p choices))
  :rule-classes :rewrite)

Theorem: 4vec-?-in-terms-of-4vec-bit?

(defthm 4vec-?-in-terms-of-4vec-bit?
  (equal (4vec-bit? (4vec-sign-ext 1 (4vec-reduction-or tests))
                    thens elses)
         (4vec-? tests thens elses)))

Theorem: 4vec-bit?-of-3vec-fix-tests

(defthm 4vec-bit?-of-3vec-fix-tests
  (equal (4vec-bit? (3vec-fix tests) thens elses)
         (4vec-bit? tests thens elses)))

Theorem: 4vec-bit?-3vec-equiv-congruence-on-tests

(defthm 4vec-bit?-3vec-equiv-congruence-on-tests
  (implies (3vec-equiv tests tests-equiv)
           (equal (4vec-bit? tests thens elses)
                  (4vec-bit? tests-equiv thens elses)))
  :rule-classes :congruence)

Theorem: 4vec-bit?-of-4vec-fix-thens

(defthm 4vec-bit?-of-4vec-fix-thens
  (equal (4vec-bit? tests (4vec-fix thens) elses)
         (4vec-bit? tests thens elses)))

Theorem: 4vec-bit?-4vec-equiv-congruence-on-thens

(defthm 4vec-bit?-4vec-equiv-congruence-on-thens
  (implies (4vec-equiv thens thens-equiv)
           (equal (4vec-bit? tests thens elses)
                  (4vec-bit? tests thens-equiv elses)))
  :rule-classes :congruence)

Theorem: 4vec-bit?-of-4vec-fix-elses

(defthm 4vec-bit?-of-4vec-fix-elses
  (equal (4vec-bit? tests thens (4vec-fix elses))
         (4vec-bit? tests thens elses)))

Theorem: 4vec-bit?-4vec-equiv-congruence-on-elses

(defthm 4vec-bit?-4vec-equiv-congruence-on-elses
  (implies (4vec-equiv elses elses-equiv)
           (equal (4vec-bit? tests thens elses)
                  (4vec-bit? tests thens elses-equiv)))
  :rule-classes :congruence)