		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; uses else branch bits for any test bits not equal to 1 (non-monotonic semantics in this respect).

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 not 1.

This is used for conditionally overriding signals, as in:

(bit?! override-test override-val regular-val)

This way, if the override-test is left out of the environment (therefore its value is X), the regular value will go through.

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__))
    (4vec-bitmux (4vec-1mask 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-bit?!-of-4vec-fix-tests

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

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

(defthm 4vec-bit?!-4vec-equiv-congruence-on-tests
  (implies (4vec-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)