Access the |AIGNET|::|XOR-MODE| field of a gatesimp bit structure.
(gatesimp->xor-mode x) → xor-mode
Function:
(defun gatesimp->xor-mode (x) (declare (xargs :guard (gatesimp-p x))) (mbe :logic (let ((x (gatesimp-fix x))) (part-select x :low 4 :width 2)) :exec (the (unsigned-byte 2) (logand (the (unsigned-byte 2) 3) (the (unsigned-byte 2) (ash (the (unsigned-byte 6) x) -4))))))
Theorem:
(defthm gatesimp-xor-mode-p-of-gatesimp->xor-mode (b* ((xor-mode (gatesimp->xor-mode x))) (gatesimp-xor-mode-p xor-mode)) :rule-classes :rewrite)
Theorem:
(defthm gatesimp->xor-mode-of-gatesimp-fix-x (equal (gatesimp->xor-mode (gatesimp-fix x)) (gatesimp->xor-mode x)))
Theorem:
(defthm gatesimp->xor-mode-gatesimp-equiv-congruence-on-x (implies (gatesimp-equiv x x-equiv) (equal (gatesimp->xor-mode x) (gatesimp->xor-mode x-equiv))) :rule-classes :congruence)
Theorem:
(defthm gatesimp->xor-mode-of-gatesimp (equal (gatesimp->xor-mode (gatesimp hashp level xor-mode)) (gatesimp-xor-mode-fix xor-mode)))
Theorem:
(defthm gatesimp->xor-mode-of-write-with-mask (implies (and (fty::bitstruct-read-over-write-hyps x gatesimp-equiv-under-mask) (gatesimp-equiv-under-mask x acl2::y fty::mask) (equal (logand (lognot fty::mask) 48) 0)) (equal (gatesimp->xor-mode x) (gatesimp->xor-mode acl2::y))))