		Search-engine friendly clone of the ACL2 documentation.

Lucid

Vl-lucid-pp-multibits

Signature
(vl-lucid-pp-multibits badbits occs ctx &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).; ctx — Guard (any-p ctx).

Definitions and Theorems

Function: vl-lucid-pp-multibits-fn

(defun vl-lucid-pp-multibits-fn (badbits occs ctx ps)
 (declare (xargs :stobjs (ps)))
 (declare (xargs :guard (and (setp badbits)
                             (vl-lucidocclist-p occs)
                             (any-p ctx))))
 (declare
      (xargs :guard (and (integer-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)
                                               ctx))
       (overlap (intersect occbits badbits))
       ((unless overlap)
        (vl-lucid-pp-multibits badbits (cdr occs)
                               ctx)))
   (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-lucidctx->elem (vl-lucidocc->ctx (car occs)))
                   :withloc t)
              (vl-println "")
              (vl-lucid-pp-multibits badbits (cdr occs)
                                     ctx)))))

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)
                                  ctx ps)
        (vl-lucid-pp-multibits-fn badbits occs ctx 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 ctx ps)
              (vl-lucid-pp-multibits-fn badbits occs-equiv ctx ps)))
  :rule-classes :congruence)

Theorem: vl-lucid-pp-multibits-fn-of-identity-ctx

(defthm vl-lucid-pp-multibits-fn-of-identity-ctx
  (equal (vl-lucid-pp-multibits-fn badbits occs (identity ctx)
                                   ps)
         (vl-lucid-pp-multibits-fn badbits occs ctx ps)))

Theorem: vl-lucid-pp-multibits-fn-equal-congruence-on-ctx

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