		Search-engine friendly clone of the ACL2 documentation.

Svex-argmasks

Svmask-for-bitor

Implements svex-argmasks for BITOR.

Signature
(svmask-for-bitor mask args) → argmasks
Arguments: mask — Care mask for the full expression.
Guard (4vmask-p mask).; args — Arguments to this BITOR operator.
Guard (svexlist-p args).
Returns: argmasks — The new care masks inferred for the args.
Type (4vmasklist-p argmasks).

See svmask-for-bitand. This is similar, except that since we are dealing with (bitor x y), the bits of x that are 1 (instead of 0) are the don't cares bits for y, and vice versa. Again we have to watch out for cases where both arguments have a 1 bit, and in such cases mark at least one or the other as a care bit.

Definitions and Theorems

Function: svmask-for-bitor

(defun svmask-for-bitor (mask args)
 (declare (xargs :guard (and (4vmask-p mask)
                             (svexlist-p args))))
 (let ((__function__ 'svmask-for-bitor))
  (declare (ignorable __function__))
  (b* (((svex-nths x y) args)
       (mask (4vmask-fix mask)))
    (b*
     (((s4vec xval) (svex-s4xeval x))
      ((s4vec yval) (svex-s4xeval y))
      (x-1 (sparseint-bitand xval.upper xval.lower))
      (y-1 (sparseint-bitand yval.upper yval.lower))
      (shared-1s (sparseint-bitand x-1 (sparseint-bitand y-1 mask)))
      (xm-non1 (sparseint-bitandc2 mask x-1))
      (ym-non1 (sparseint-bitandc2 mask y-1))
      ((when (sparseint-equal 0 shared-1s))
       (list ym-non1 xm-non1))
      (y-x (sparseint-bitandc2 yval.upper yval.lower))
      (ym-x (sparseint-test-bitand mask y-x))
      ((unless ym-x)
       (list ym-non1
             (sparseint-bitor xm-non1 shared-1s))))
     (list (sparseint-bitor ym-non1 shared-1s)
           xm-non1)))))

Theorem: 4vmasklist-p-of-svmask-for-bitor

(defthm 4vmasklist-p-of-svmask-for-bitor
  (b* ((argmasks (svmask-for-bitor mask args)))
    (4vmasklist-p argmasks))
  :rule-classes :rewrite)

Theorem: svmask-for-bitor-of-4vmask-fix-mask

(defthm svmask-for-bitor-of-4vmask-fix-mask
  (equal (svmask-for-bitor (4vmask-fix mask)
                           args)
         (svmask-for-bitor mask args)))

Theorem: svmask-for-bitor-4vmask-equiv-congruence-on-mask

(defthm svmask-for-bitor-4vmask-equiv-congruence-on-mask
  (implies (4vmask-equiv mask mask-equiv)
           (equal (svmask-for-bitor mask args)
                  (svmask-for-bitor mask-equiv args)))
  :rule-classes :congruence)

Theorem: svmask-for-bitor-of-svexlist-fix-args

(defthm svmask-for-bitor-of-svexlist-fix-args
  (equal (svmask-for-bitor mask (svexlist-fix args))
         (svmask-for-bitor mask args)))

Theorem: svmask-for-bitor-svexlist-equiv-congruence-on-args

(defthm svmask-for-bitor-svexlist-equiv-congruence-on-args
  (implies (svexlist-equiv args args-equiv)
           (equal (svmask-for-bitor mask args)
                  (svmask-for-bitor mask args-equiv)))
  :rule-classes :congruence)

Theorem: svmask-for-bitor-correct

(defthm svmask-for-bitor-correct
 (implies
    (and (equal (4veclist-mask (svmask-for-bitor mask args)
                               (svexlist-eval args env))
                (4veclist-mask (svmask-for-bitor mask args)
                               args1))
         (syntaxp (not (equal args1
                              (cons 'svexlist-eval
                                    (cons args (cons env 'nil)))))))
    (equal (4vec-mask mask (svex-apply 'bitor args1))
           (4vec-mask mask
                      (svex-apply 'bitor
                                  (svexlist-eval args env))))))