		Search-engine friendly clone of the ACL2 documentation.

Svex-argmasks

Svmask-for-+

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

We can't do anything smart here. Since (+ x y) returns pure Xes whenever there are any X/Z bits in x or y, we always have to consider all of the bits of both arguments, unless we truly don't care about any bits of the result at all.

It would be possible to improve the mask in the case that we knew some bit of some argument was z, because in that case we would know that the whole answer was definitely Xes. However, since Z values are pretty uncommon, it probably isn't worth doing this.

Definitions and Theorems

Function: svmask-for-+$inline

(defun svmask-for-+$inline (mask args)
  (declare (xargs :guard (and (4vmask-p mask)
                              (svexlist-p args))))
  (let ((__function__ 'svmask-for-+))
    (declare (ignorable __function__))
    (b* ((mask (4vmask-fix mask)))
      (b* ((argmask (4vmask-all-or-none mask)))
        (list argmask argmask)))))

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

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

Theorem: svmask-for-+$inline-of-4vmask-fix-mask

(defthm svmask-for-+$inline-of-4vmask-fix-mask
  (equal (svmask-for-+$inline (4vmask-fix mask)
                              args)
         (svmask-for-+$inline mask args)))

Theorem: svmask-for-+$inline-4vmask-equiv-congruence-on-mask

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

Theorem: svmask-for-+$inline-of-svexlist-fix-args

(defthm svmask-for-+$inline-of-svexlist-fix-args
  (equal (svmask-for-+$inline mask (svexlist-fix args))
         (svmask-for-+$inline mask args)))

Theorem: svmask-for-+$inline-svexlist-equiv-congruence-on-args

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

Theorem: svmask-for-+-correct

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