		Search-engine friendly clone of the ACL2 documentation.

Svex-argmasks

Svmask-for-==??

Implements svex-argmasks 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 are considering (==?? a b), i.e., 4vec-symwildeq. We want to compute the care masks for a and b, given some outer care mask for the whole expression.

We of course care about any bits ai and bi where neither ai or bi are known to be Z. However, if we can statically determine that, e.g., ai is Z, then there's no reason to care about the corresponding bi. Symmetrically, if we can determine that bi is Z, we (almost) don't need to care about ai. The only catch is that if both vectors share a Z, we can't ignore both bits simultaneously, but instead have to choose to keep one or the other. We make this decision following a strategy that is similar to svmask-for-bitand.

Definitions and Theorems

Function: svmask-for-==??

(defun svmask-for-==?? (mask args)
  (declare (xargs :guard (and (4vmask-p mask)
                              (svexlist-p args))))
  (let ((__function__ 'svmask-for-==??))
    (declare (ignorable __function__))
    (b* (((svex-nths a b) args)
         (mask (4vmask-fix mask)))
      (b* (((s4vec aval) (svex-s4xeval a))
           ((s4vec bval) (svex-s4xeval b))
           (a-is-not-z (sparseint-bitorc2 aval.upper aval.lower))
           (b-is-not-z (sparseint-bitorc2 bval.upper bval.lower))
           (both-are-z (sparseint-bitnor a-is-not-z b-is-not-z))
           ((when (sparseint-equal both-are-z 0))
            (list b-is-not-z a-is-not-z))
           (not-b-x (sparseint-test-bitandc2 bval.upper bval.lower))
           ((when (not not-b-x))
            (list b-is-not-z
                  (sparseint-bitnand a-is-not-z both-are-z))))
        (list (sparseint-bitnand b-is-not-z both-are-z)
              a-is-not-z)))))

Theorem: 4vmasklist-p-of-svmask-for-==??

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

Theorem: svmask-for-==??-of-4vmask-fix-mask

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

Theorem: svmask-for-==??-4vmask-equiv-congruence-on-mask

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

Theorem: svmask-for-==??-of-svexlist-fix-args

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

Theorem: svmask-for-==??-svexlist-equiv-congruence-on-args

(defthm svmask-for-==??-svexlist-equiv-congruence-on-args
  (implies (svexlist-equiv args args-equiv)
           (equal (svmask-for-==?? mask args)
                  (svmask-for-==?? 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))))))