		Search-engine friendly clone of the ACL2 documentation.

Propagate

Remove-simple-assigns-to

Remove all assignments to these wires (we do this after we've propagated the assignments.

Signature
(remove-simple-assigns-to names assigns) → new-assigns
Arguments: names — Guard (string-listp names).; assigns — Guard (vl-assignlist-p assigns).
Returns: new-assigns — Type (vl-assignlist-p new-assigns), given the guard.

Definitions and Theorems

Function: remove-simple-assigns-to

(defun remove-simple-assigns-to (names assigns)
  (declare (xargs :guard (and (string-listp names)
                              (vl-assignlist-p assigns))))
  (let ((__function__ 'remove-simple-assigns-to))
    (declare (ignorable __function__))
    (b* (((when (atom assigns)) nil)
         (x1 (car assigns))
         ((vl-assign x1) x1)
         ((when (and (vl-idexpr-p x1.lvalue)
                     (member-equal (vl-idexpr->name x1.lvalue)
                                   names)))
          (remove-simple-assigns-to names (cdr assigns))))
      (cons (car assigns)
            (remove-simple-assigns-to names (cdr assigns))))))

Theorem: vl-assignlist-p-of-remove-simple-assigns-to

(defthm vl-assignlist-p-of-remove-simple-assigns-to
  (implies
       (and (force (string-listp names))
            (force (vl-assignlist-p assigns)))
       (b* ((new-assigns (remove-simple-assigns-to names assigns)))
         (vl-assignlist-p new-assigns)))
  :rule-classes :rewrite)