(vl-expr-simp-binary-bitor x args) → new-x
Function:
(defun vl-expr-simp-binary-bitor (x args) (declare (xargs :guard (and (vl-expr-p x) (vl-exprlist-p args)))) (declare (xargs :guard (and (not (vl-atom-p x)) (equal (vl-nonatom->op x) :vl-binary-bitor) (equal (len args) 2)))) (let ((__function__ 'vl-expr-simp-binary-bitor)) (declare (ignorable __function__)) (b* (((list arg1 arg2) args) ((when (and (vl-expr-resolved-p arg2) (eql (vl-resolved->val arg2) 0) (equal (vl-expr->finalwidth x) (vl-expr->finalwidth arg1)) (equal (vl-expr->finaltype x) (vl-expr->finaltype arg1)))) (b* ((ans (vl-expr-fix arg1))) (vl-cw-ps-seq (vl-cw "ORa0 rewrite ~a0 to ~a1~%" x ans)) ans)) ((when (and (vl-expr-resolved-p arg1) (eql (vl-resolved->val arg1) 0) (equal (vl-expr->finalwidth x) (vl-expr->finalwidth arg2)) (equal (vl-expr->finaltype x) (vl-expr->finaltype arg2)))) (b* ((ans (vl-expr-fix arg2))) (vl-cw-ps-seq (vl-cw "OR0a rewrite ~a0 to ~a1~%" x ans)) ans)) ((when (and (vl-expr-resolved-p arg2) (eql (vl-resolved->val arg2) 1) (equal (vl-expr->finalwidth x) 1) (equal (vl-expr->finalwidth arg1) 1) (equal (vl-expr->finalwidth arg2) 1) (eq (vl-expr->finaltype x) :vl-unsigned) (eq (vl-expr->finaltype arg1) :vl-unsigned) (eq (vl-expr->finaltype arg2) :vl-unsigned))) (b* ((ans (vl-expr-fix arg2))) (vl-cw-ps-seq (vl-cw "ORa1 rewrite ~a0 to ~a1~%" x ans)) ans)) ((when (and (vl-expr-resolved-p arg1) (eql (vl-resolved->val arg1) 1) (equal (vl-expr->finalwidth x) 1) (equal (vl-expr->finalwidth arg1) 1) (equal (vl-expr->finalwidth arg2) 1) (eq (vl-expr->finaltype x) :vl-unsigned) (eq (vl-expr->finaltype arg1) :vl-unsigned) (eq (vl-expr->finaltype arg2) :vl-unsigned))) (b* ((ans (vl-expr-fix arg1))) (vl-cw-ps-seq (vl-cw "OR1a rewrite ~a0 to ~a1~%" x ans)) ans))) (change-vl-nonatom x :args args))))
Theorem:
(defthm vl-expr-p-of-vl-expr-simp-binary-bitor (b* ((new-x (vl-expr-simp-binary-bitor x args))) (vl-expr-p new-x)) :rule-classes :rewrite)
Theorem:
(defthm vl-expr-simp-binary-bitor-of-vl-expr-fix-x (equal (vl-expr-simp-binary-bitor (vl-expr-fix x) args) (vl-expr-simp-binary-bitor x args)))
Theorem:
(defthm vl-expr-simp-binary-bitor-vl-expr-equiv-congruence-on-x (implies (vl-expr-equiv x x-equiv) (equal (vl-expr-simp-binary-bitor x args) (vl-expr-simp-binary-bitor x-equiv args))) :rule-classes :congruence)
Theorem:
(defthm vl-expr-simp-binary-bitor-of-vl-exprlist-fix-args (equal (vl-expr-simp-binary-bitor x (vl-exprlist-fix args)) (vl-expr-simp-binary-bitor x args)))
Theorem:
(defthm vl-expr-simp-binary-bitor-vl-exprlist-equiv-congruence-on-args (implies (vl-exprlist-equiv args args-equiv) (equal (vl-expr-simp-binary-bitor x args) (vl-expr-simp-binary-bitor x args-equiv))) :rule-classes :congruence)