		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 are considering a (?! test then else) expression and we know that we only care about the bits mentioned in mask. We need to figure out which bits of test, then, and else we care about.

We will almost always need to care about the entire test expression. The only exceptions to this would be when either:

We don't care about any bits at all, i.e., the outer mask is empty.
For all bits we care about, the corresponding bits of then and else branches are known to agree. For instance, (?! test 5 5) is going to be 5 regardless of test. (This is pretty obscure).

More obvious and probably more useful mask improvements:

When we know that some bit of test is 1, we can completely don't care else;
When we know that all bits of test are not 1, we can completely don't care then. We don't really have a good way to check this other than checking that the xeval is 0, though.

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 test then else) args)
         (mask (4vmask-fix mask)))
      (b* (((when (4vmask-empty mask))
            (list 0 0 0))
           ((s4vec testval) (svex-s4xeval test))
           (test-1s (sparseint-bitand testval.upper testval.lower))
           ((unless (sparseint-equal test-1s 0))
            (list test-1s mask 0))
           ((when (and (sparseint-equal testval.upper 0)
                       (sparseint-equal testval.lower 0)))
            (list -1 0 mask)))
        (if (or (equal then else)
                (branches-same-under-mask-p mask then else))
            (list 0 mask mask)
          (list -1 mask mask))))))

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))))))