		Search-engine friendly clone of the ACL2 documentation.

Duplicate-detect

Vl-duplicate-gateinst-locations

Signature
(vl-duplicate-gateinst-locations dupe fixed orig) → matches
Arguments: dupe — Some gateinst that was duplicated (fixed).
Guard (vl-gateinst-p dupe).; fixed — Fixed versions of orig.
Guard (vl-gateinstlist-p fixed).; orig — Original gate instances, i.e., before fixing.
Guard (vl-gateinstlist-p orig).
Returns: matches — Locations of gates matching dupe.
Type (vl-locationlist-p matches), given the guard.

Definitions and Theorems

Function: vl-duplicate-gateinst-locations

(defun vl-duplicate-gateinst-locations (dupe fixed orig)
  (declare (xargs :guard (and (vl-gateinst-p dupe)
                              (vl-gateinstlist-p fixed)
                              (vl-gateinstlist-p orig))))
  (declare (xargs :guard (same-lengthp fixed orig)))
  (let ((__function__ 'vl-duplicate-gateinst-locations))
    (declare (ignorable __function__))
    (b* (((when (atom fixed)) nil)
         (rest (vl-duplicate-gateinst-locations dupe (cdr fixed)
                                                (cdr orig)))
         ((when (equal dupe (car fixed)))
          (cons (vl-gateinst->loc (car orig))
                rest)))
      rest)))

Theorem: vl-locationlist-p-of-vl-duplicate-gateinst-locations

(defthm vl-locationlist-p-of-vl-duplicate-gateinst-locations
 (implies
   (and (force (vl-gateinst-p dupe))
        (force (vl-gateinstlist-p fixed))
        (force (vl-gateinstlist-p orig))
        (force (same-lengthp fixed orig)))
   (b* ((matches (vl-duplicate-gateinst-locations dupe fixed orig)))
     (vl-locationlist-p matches)))
 :rule-classes :rewrite)