Function:
(defun vl-consteval-unary-reduxop (op aval width) (declare (xargs :guard (and (member op '(:vl-unary-bitand :vl-unary-nand :vl-unary-bitor :vl-unary-nor :vl-unary-xor :vl-unary-xnor :vl-unary-lognot)) (natp aval) (posp width)))) (let ((__function__ 'vl-consteval-unary-reduxop)) (declare (ignorable __function__)) (b* ((aval (lnfix aval)) (width (lposfix width))) (case op (:vl-unary-bitand (if (equal (acl2::loghead width aval) (1- (expt 2 width))) 1 0)) (:vl-unary-nand (if (equal (acl2::loghead width aval) (1- (expt 2 width))) 0 1)) (:vl-unary-bitor (if (posp aval) 1 0)) (:vl-unary-nor (if (posp aval) 0 1)) (:vl-unary-xor (if (oddp aval) 1 0)) (:vl-unary-xnor (if (oddp aval) 0 1)) (:vl-unary-lognot (if (posp aval) 0 1)) (otherwise (progn$ (impossible) 0))))))
Theorem:
(defthm bitp-of-vl-consteval-unary-reduxop (b* ((ans (vl-consteval-unary-reduxop op aval width))) (bitp ans)) :rule-classes :rewrite)
Theorem:
(defthm vl-consteval-unary-reduxop-of-nfix-aval (equal (vl-consteval-unary-reduxop op (nfix aval) width) (vl-consteval-unary-reduxop op aval width)))
Theorem:
(defthm vl-consteval-unary-reduxop-nat-equiv-congruence-on-aval (implies (acl2::nat-equiv aval aval-equiv) (equal (vl-consteval-unary-reduxop op aval width) (vl-consteval-unary-reduxop op aval-equiv width))) :rule-classes :congruence)
Theorem:
(defthm vl-consteval-unary-reduxop-of-pos-fix-width (equal (vl-consteval-unary-reduxop op aval (pos-fix width)) (vl-consteval-unary-reduxop op aval width)))
Theorem:
(defthm vl-consteval-unary-reduxop-pos-equiv-congruence-on-width (implies (acl2::pos-equiv width width-equiv) (equal (vl-consteval-unary-reduxop op aval width) (vl-consteval-unary-reduxop op aval width-equiv))) :rule-classes :congruence)