		Search-engine friendly clone of the ACL2 documentation.

Lucid

Vl-lucid-pp-multibits

Signature
(vl-lucid-pp-multibits badbits occs &key (ps 'ps)) → ps
Arguments: badbits — The set of multiply driven bits.
Guard (setp badbits).; occs — Occs which may or may not drive these bits.
Guard (vl-lucidocclist-p occs).

Definitions and Theorems

Function: vl-lucid-pp-multibits-fn

(defun vl-lucid-pp-multibits-fn (badbits occs ps)
 (declare (xargs :stobjs (ps)))
 (declare (xargs :guard (and (setp badbits)
                             (vl-lucidocclist-p occs))))
 (declare
      (xargs :guard (and (nat-listp badbits)
                         (vl-lucid-all-slices-p occs)
                         (vl-lucid-all-slices-resolved-p occs))))
 (let ((__function__ 'vl-lucid-pp-multibits))
  (declare (ignorable __function__))
  (b* (((when (atom occs)) ps)
       (occbits (vl-lucid-resolved-slice->bits (car occs)))
       (overlap (intersect occbits badbits))
       ((unless overlap)
        (vl-lucid-pp-multibits badbits (cdr occs))))
   (vl-ps-seq (vl-indent 4)
              (if (vl-plural-p overlap)
                  (vl-print " - Bits ")
                (vl-print " - Bit "))
              (vl-lucid-pp-bits overlap)
              (vl-print ": ")
              (vl-pp-ctxelement-summary
                   (vl-context1->elem (vl-lucidocc->ctx (car occs)))
                   :withloc t)
              (vl-println "")
              (vl-lucid-pp-multibits badbits (cdr occs))))))

Theorem: vl-lucid-pp-multibits-fn-of-vl-lucidocclist-fix-occs

(defthm vl-lucid-pp-multibits-fn-of-vl-lucidocclist-fix-occs
 (equal (vl-lucid-pp-multibits-fn badbits (vl-lucidocclist-fix occs)
                                  ps)
        (vl-lucid-pp-multibits-fn badbits occs ps)))

Theorem: vl-lucid-pp-multibits-fn-vl-lucidocclist-equiv-congruence-on-occs

(defthm
  vl-lucid-pp-multibits-fn-vl-lucidocclist-equiv-congruence-on-occs
  (implies (vl-lucidocclist-equiv occs occs-equiv)
           (equal (vl-lucid-pp-multibits-fn badbits occs ps)
                  (vl-lucid-pp-multibits-fn badbits occs-equiv ps)))
  :rule-classes :congruence)