		Search-engine friendly clone of the ACL2 documentation.

Oprewrite

Vl-goofymux-rewrite

Annotate weird muxes with less conservative X behavior.

Signature
(vl-goofymux-rewrite x) → new-x
Arguments: x — Guard (vl-expr-p x).
Returns: new-x — Type (vl-expr-p new-x).

Definitions and Theorems

Function: vl-goofymux-rewrite

(defun vl-goofymux-rewrite (x)
  (declare (xargs :guard (vl-expr-p x)))
  (let ((__function__ 'vl-goofymux-rewrite))
    (declare (ignorable __function__))
    (b* (((mv sel i1 i2) (vl-goofymux-p x))
         ((unless sel) (vl-expr-fix x)))
      (make-vl-nonatom :op :vl-qmark
                       :args (list sel i1 i2)
                       :atts (acons "VL_X_SELECT"
                                    nil (vl-nonatom->atts x))))))

Theorem: vl-expr-p-of-vl-goofymux-rewrite

(defthm vl-expr-p-of-vl-goofymux-rewrite
  (b* ((new-x (vl-goofymux-rewrite x)))
    (vl-expr-p new-x))
  :rule-classes :rewrite)

Theorem: vl-goofymux-rewrite-count-weak

(defthm vl-goofymux-rewrite-count-weak
  (<= (vl-expr-count-noatts (vl-goofymux-rewrite x))
      (vl-expr-count-noatts x))
  :rule-classes ((:rewrite) (:linear)))

Theorem: vl-goofymux-rewrite-count-strong

(defthm vl-goofymux-rewrite-count-strong
  (implies (not (equal (vl-expr-kind x) :atom))
           (< (vl-exprlist-count-noatts
                   (vl-nonatom->args (vl-goofymux-rewrite x)))
              (vl-expr-count-noatts x))))

Theorem: vl-expr-kind-of-vl-goofymux-rewrite

(defthm vl-expr-kind-of-vl-goofymux-rewrite
  (equal (vl-expr-kind (vl-goofymux-rewrite x))
         (vl-expr-kind x)))

Theorem: vl-goofymux-rewrite-of-vl-expr-fix-x

(defthm vl-goofymux-rewrite-of-vl-expr-fix-x
  (equal (vl-goofymux-rewrite (vl-expr-fix x))
         (vl-goofymux-rewrite x)))

Theorem: vl-goofymux-rewrite-vl-expr-equiv-congruence-on-x

(defthm vl-goofymux-rewrite-vl-expr-equiv-congruence-on-x
  (implies (vl-expr-equiv x x-equiv)
           (equal (vl-goofymux-rewrite x)
                  (vl-goofymux-rewrite x-equiv)))
  :rule-classes :congruence)