(vl-expr-simp-binary-bitand x args) → new-x
Function:
(defun vl-expr-simp-binary-bitand (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-bitand) (equal (len args) 2)))) (let ((__function__ 'vl-expr-simp-binary-bitand)) (declare (ignorable __function__)) (b* (((list arg1 arg2) args) ((when (and (vl-expr-resolved-p arg2) (eql (vl-resolved->val arg2) 0))) (b* ((ans (change-vl-atom arg2 :finaltype (vl-expr->finaltype x) :finalwidth (vl-expr->finalwidth x)))) (vl-cw-ps-seq (vl-cw "AND0a rewrite ~a0 to ~a1~%" x ans)) ans)) ((when (and (vl-expr-resolved-p arg1) (eql (vl-resolved->val arg1) 0))) (b* ((ans (change-vl-atom arg1 :finaltype (vl-expr->finaltype x) :finalwidth (vl-expr->finalwidth x)))) (vl-cw-ps-seq (vl-cw "AND0b 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->finaltype x) :vl-unsigned) (equal (vl-expr->finalwidth arg1) 1) (equal (vl-expr->finaltype arg1) :vl-unsigned))) (b* ((ans (vl-expr-fix arg1))) (vl-cw-ps-seq (vl-cw "AND1a 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->finaltype x) :vl-unsigned) (equal (vl-expr->finalwidth arg2) 1) (equal (vl-expr->finaltype arg2) :vl-unsigned))) (b* ((ans (vl-expr-fix arg2))) (vl-cw-ps-seq (vl-cw "AND1b rewrite ~a0 to ~a1~%" x ans)) ans))) (change-vl-nonatom x :args args))))
Theorem:
(defthm vl-expr-p-of-vl-expr-simp-binary-bitand (b* ((new-x (vl-expr-simp-binary-bitand x args))) (vl-expr-p new-x)) :rule-classes :rewrite)
Theorem:
(defthm vl-expr-simp-binary-bitand-of-vl-expr-fix-x (equal (vl-expr-simp-binary-bitand (vl-expr-fix x) args) (vl-expr-simp-binary-bitand x args)))
Theorem:
(defthm vl-expr-simp-binary-bitand-vl-expr-equiv-congruence-on-x (implies (vl-expr-equiv x x-equiv) (equal (vl-expr-simp-binary-bitand x args) (vl-expr-simp-binary-bitand x-equiv args))) :rule-classes :congruence)
Theorem:
(defthm vl-expr-simp-binary-bitand-of-vl-exprlist-fix-args (equal (vl-expr-simp-binary-bitand x (vl-exprlist-fix args)) (vl-expr-simp-binary-bitand x args)))
Theorem:
(defthm vl-expr-simp-binary-bitand-vl-exprlist-equiv-congruence-on-args (implies (vl-exprlist-equiv args args-equiv) (equal (vl-expr-simp-binary-bitand x args) (vl-expr-simp-binary-bitand x args-equiv))) :rule-classes :congruence)