Normalized right-hand side of an assignment operator expression.
Given an expression like
Function:
(defun vl-assign-op-expr (var op rhs) (declare (xargs :guard (and (vl-expr-p var) (member op *vl-assignment-operators*) (vl-expr-p rhs)))) (let ((__function__ 'vl-assign-op-expr)) (declare (ignorable __function__)) (if (eq op :vl-equalsign) (vl-expr-fix rhs) (make-vl-binary :op (case op (:vl-pluseq :vl-binary-plus) (:vl-minuseq :vl-binary-minus) (:vl-timeseq :vl-binary-times) (:vl-diveq :vl-binary-div) (:vl-remeq :vl-binary-rem) (:vl-andeq :vl-binary-bitand) (:vl-oreq :vl-binary-bitor) (:vl-xoreq :vl-binary-xor) (:vl-shleq :vl-binary-shl) (:vl-shreq :vl-binary-shr) (:vl-ashleq :vl-binary-ashl) (:vl-ashreq :vl-binary-ashr)) :left var :right rhs))))
Theorem:
(defthm vl-expr-p-of-vl-assign-op-expr (b* ((expr (vl-assign-op-expr var op rhs))) (vl-expr-p expr)) :rule-classes :rewrite)