Zero out the don't-care bits from the right-hand side of a
(vl-msb-bits-zap-dontcares msb-bits care-bits) → new-bitlist
Note: If there is ever a case where Z is one of the care bits,
think about whether this does the right thing. Specifically: it is not the
case that if Z is among the care bits, then this function produces the same
bitlist value as
Function:
(defun vl-msb-bits-zap-dontcares (msb-bits care-bits) (declare (xargs :guard (and (vl-bitlist-p msb-bits) (vl-bitlist-p care-bits)))) (declare (xargs :guard (true-listp care-bits))) (let ((__function__ 'vl-msb-bits-zap-dontcares)) (declare (ignorable __function__)) (b* (((when (atom msb-bits)) nil) (bit1 (vl-bit-fix (car msb-bits))) (value (if (member-eq bit1 (vl-bitlist-fix care-bits)) bit1 :vl-0val))) (cons value (vl-msb-bits-zap-dontcares (cdr msb-bits) care-bits)))))
Theorem:
(defthm vl-bitlist-p-of-vl-msb-bits-zap-dontcares (b* ((new-bitlist (vl-msb-bits-zap-dontcares msb-bits care-bits))) (vl-bitlist-p new-bitlist)) :rule-classes :rewrite)
Theorem:
(defthm len-of-vl-msb-bits-zap-dontcares (equal (len (vl-msb-bits-zap-dontcares msb-bits cares)) (len msb-bits)))
Theorem:
(defthm vl-msb-bits-zap-dontcares-under-iff (iff (vl-msb-bits-zap-dontcares msb-bits cares) (consp msb-bits)))
Theorem:
(defthm vl-msb-bits-zap-dontcares-of-vl-bitlist-fix-msb-bits (equal (vl-msb-bits-zap-dontcares (vl-bitlist-fix msb-bits) care-bits) (vl-msb-bits-zap-dontcares msb-bits care-bits)))
Theorem:
(defthm vl-msb-bits-zap-dontcares-vl-bitlist-equiv-congruence-on-msb-bits (implies (vl-bitlist-equiv msb-bits msb-bits-equiv) (equal (vl-msb-bits-zap-dontcares msb-bits care-bits) (vl-msb-bits-zap-dontcares msb-bits-equiv care-bits))) :rule-classes :congruence)
Theorem:
(defthm vl-msb-bits-zap-dontcares-of-vl-bitlist-fix-care-bits (equal (vl-msb-bits-zap-dontcares msb-bits (vl-bitlist-fix care-bits)) (vl-msb-bits-zap-dontcares msb-bits care-bits)))
Theorem:
(defthm vl-msb-bits-zap-dontcares-vl-bitlist-equiv-congruence-on-care-bits (implies (vl-bitlist-equiv care-bits care-bits-equiv) (equal (vl-msb-bits-zap-dontcares msb-bits care-bits) (vl-msb-bits-zap-dontcares msb-bits care-bits-equiv))) :rule-classes :congruence)