Combine together the writes to a variable that occur in the same always block.
(vl-lucidocclist-merge-blocks x) → merged
Function:
(defun vl-lucidocclist-merge-blocks (x) (declare (xargs :guard (vl-lucidocclist-p x))) (let ((__function__ 'vl-lucidocclist-merge-blocks)) (declare (ignorable __function__)) (b* (((mv merge-alist regular) (vl-lucid-filter-merges x nil nil)) (merge-alist (fast-alist-clean merge-alist))) (fast-alist-free merge-alist) (append (vl-lucid-do-merges merge-alist) regular))))
Theorem:
(defthm vl-lucidocclist-p-of-vl-lucidocclist-merge-blocks (b* ((merged (vl-lucidocclist-merge-blocks x))) (vl-lucidocclist-p merged)) :rule-classes :rewrite)
Theorem:
(defthm vl-lucidocclist-merge-blocks-of-vl-lucidocclist-fix-x (equal (vl-lucidocclist-merge-blocks (vl-lucidocclist-fix x)) (vl-lucidocclist-merge-blocks x)))
Theorem:
(defthm vl-lucidocclist-merge-blocks-vl-lucidocclist-equiv-congruence-on-x (implies (vl-lucidocclist-equiv x x-equiv) (equal (vl-lucidocclist-merge-blocks x) (vl-lucidocclist-merge-blocks x-equiv))) :rule-classes :congruence)