		Search-engine friendly clone of the ACL2 documentation.

Svex-argmasks

Svmask-for-bit?!

Implements svex-argmasks for BIT?!.

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

We are considering a (bit?! tests thens elses) expression and we know that we only care about the bits mentioned in mask. We want to figure out which bits of X and Y we care about.

As a starting point, since 4vec-bit?! operates in a bit-by-bit fashion, we certainly don't care about any bits that are don't cares in our outer mask.

For tests, for now we don't try to do anything smart—we just keep the outer mask. We might consider eventually extending this: if we can determine that thens[i] and elses[i] agree on some value, then we the test bit is irrelevant because of the way that 4vec-bit? does its merging. But it doesn't seem like this would help us very often, so for now it doesn't seem worth doing.

For thens, the main thing we want to take advantage of is that if we know that test[i] is not going to be 1, then we don't care about thens[i] because we're going to choose elses[i] instead. So, we improve the mask by excluding any bits of tests that are obviously false.

For elses, likewise we improve the mask by removing any bits of tests that are obviously 1.

Definitions and Theorems

Function: svmask-for-bit?!

(defun svmask-for-bit?! (mask args)
  (declare (xargs :guard (and (4vmask-p mask)
                              (svexlist-p args))))
  (let ((__function__ 'svmask-for-bit?!))
    (declare (ignorable __function__))
    (b* (((svex-nths tests) args)
         (mask (4vmask-fix mask)))
      (b* (((mv maybe-1 maybe-not1)
            (if (svex-case tests :quote)
                (b* (((4vec test) (svex-quote->val tests))
                     (known1 (logand test.upper test.lower)))
                  (mv (int-to-sparseint known1)
                      (int-to-sparseint (lognot known1))))
              (b* (((s4vec tval) (svex-s4xeval tests)))
                (mv tval.upper
                    (sparseint-bitnand tval.upper tval.lower))))))
        (list mask (sparseint-bitand mask maybe-1)
              (sparseint-bitand mask maybe-not1))))))

Theorem: 4vmasklist-p-of-svmask-for-bit?!

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

Theorem: svmask-for-bit?!-of-4vmask-fix-mask

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

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

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

Theorem: svmask-for-bit?!-of-svexlist-fix-args

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

Theorem: svmask-for-bit?!-svexlist-equiv-congruence-on-args

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

Theorem: svmask-for-bit?!-correct

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