		Search-engine friendly clone of the ACL2 documentation.

Vl-emodwire-p

Vl-emodwirelist-highest

(vl-emodwirelist-highest basename x) returns a number n that is at least as large as the index of any wire with this basename in x.

We use this in a few places during e-conversion to generate new, fresh E wires.

The scheme is basically similar to that of a vl-namedb-p or vl-namefactory-p: we first find an n that is larger than any foo[k] currently in use, then start generating foo[n], foo[n+1], etc. We don't use a namedb or namefactory because we need to generate vl-emodwire-ps instead of strings.

Definitions and Theorems

Function: vl-emodwirelist-highest

(defun vl-emodwirelist-highest (basename x)
  (declare (xargs :guard (and (stringp basename)
                              (vl-emodwirelist-p x))))
  (cond ((atom x) 0)
        ((equal (vl-emodwire->basename (car x))
                basename)
         (max (nfix (vl-emodwire->index (car x)))
              (vl-emodwirelist-highest basename (cdr x))))
        (t (vl-emodwirelist-highest basename (cdr x)))))

Theorem: natp-of-vl-emodwirelist-highest

(defthm natp-of-vl-emodwirelist-highest
  (natp (vl-emodwirelist-highest basename x))
  :rule-classes :type-prescription)

Theorem: vl-emodwirelist-highest-correct

(defthm vl-emodwirelist-highest-correct
  (implies (and (member-equal w x)
                (equal (vl-emodwire->basename w)
                       basename))
           (<= (nfix (vl-emodwire->index w))
               (vl-emodwirelist-highest basename x))))