		Search-engine friendly clone of the ACL2 documentation.

Svmask-for-?

Branches-same-under-mask-p

Checks whether then and else are statically known to agree, in which case we don't care about test at all.

Signature
(branches-same-under-mask-p mask then else) → *
Arguments: mask — Guard (4vmask-p mask).; then — Guard (svex-p then).; else — Guard (svex-p else).

Definitions and Theorems

Function: branches-same-under-mask-p

(defun branches-same-under-mask-p (mask then else)
  (declare (xargs :guard (and (4vmask-p mask)
                              (svex-p then)
                              (svex-p else))))
  (let ((__function__ 'branches-same-under-mask-p))
    (declare (ignorable __function__))
    (b* ((mask (4vmask-fix mask))
         ((s4vec thenval) (svex-s4xeval then))
         (then-bool (sparseint-biteqv thenval.upper thenval.lower))
         ((when (sparseint-test-bitandc2 mask then-bool))
          nil)
         ((s4vec elseval) (svex-s4xeval else))
         (else-bool (sparseint-biteqv elseval.upper elseval.lower))
         ((when (sparseint-test-bitandc2 mask else-bool))
          nil))
      (sparseint-equal (sparseint-bitand mask thenval.upper)
                       (sparseint-bitand mask elseval.upper)))))

Theorem: branches-same-under-mask-p-of-4vmask-fix-mask

(defthm branches-same-under-mask-p-of-4vmask-fix-mask
  (equal (branches-same-under-mask-p (4vmask-fix mask)
                                     then else)
         (branches-same-under-mask-p mask then else)))

Theorem: branches-same-under-mask-p-4vmask-equiv-congruence-on-mask

(defthm branches-same-under-mask-p-4vmask-equiv-congruence-on-mask
 (implies (4vmask-equiv mask mask-equiv)
          (equal (branches-same-under-mask-p mask then else)
                 (branches-same-under-mask-p mask-equiv then else)))
 :rule-classes :congruence)

Theorem: branches-same-under-mask-p-of-svex-fix-then

(defthm branches-same-under-mask-p-of-svex-fix-then
  (equal (branches-same-under-mask-p mask (svex-fix then)
                                     else)
         (branches-same-under-mask-p mask then else)))

Theorem: branches-same-under-mask-p-svex-equiv-congruence-on-then

(defthm branches-same-under-mask-p-svex-equiv-congruence-on-then
 (implies (svex-equiv then then-equiv)
          (equal (branches-same-under-mask-p mask then else)
                 (branches-same-under-mask-p mask then-equiv else)))
 :rule-classes :congruence)

Theorem: branches-same-under-mask-p-of-svex-fix-else

(defthm branches-same-under-mask-p-of-svex-fix-else
  (equal (branches-same-under-mask-p mask then (svex-fix else))
         (branches-same-under-mask-p mask then else)))

Theorem: branches-same-under-mask-p-svex-equiv-congruence-on-else

(defthm branches-same-under-mask-p-svex-equiv-congruence-on-else
 (implies (svex-equiv else else-equiv)
          (equal (branches-same-under-mask-p mask then else)
                 (branches-same-under-mask-p mask then else-equiv)))
 :rule-classes :congruence)