		Search-engine friendly clone of the ACL2 documentation.

Bit-blasting

Svex-maskbits-for-vars

Signature
(svex-maskbits-for-vars vars masks boolmasks) → incr
Arguments: vars — Guard (svarlist-p vars).; masks — Guard (svex-mask-alist-p masks).; boolmasks — Guard (svar-boolmasks-p boolmasks).
Returns: incr — Type (natp incr).

Definitions and Theorems

Function: svex-maskbits-for-vars

(defun svex-maskbits-for-vars (vars masks boolmasks)
  (declare (xargs :guard (and (svarlist-p vars)
                              (svex-mask-alist-p masks)
                              (svar-boolmasks-p boolmasks))))
  (let ((__function__ 'svex-maskbits-for-vars))
    (declare (ignorable __function__))
    (b* (((when (atom vars)) 0)
         (mask (svex-mask-lookup (svex-var (car vars))
                                 masks))
         (boolmask (svar-boolmasks-lookup (car vars)
                                          boolmasks))
         ((when (sparseint-< mask 0)) 0))
      (+ (4vmask-to-a4vec-varcount mask boolmask)
         (svex-maskbits-for-vars (cdr vars)
                                 masks boolmasks)))))

Theorem: natp-of-svex-maskbits-for-vars

(defthm natp-of-svex-maskbits-for-vars
  (b* ((incr (svex-maskbits-for-vars vars masks boolmasks)))
    (natp incr))
  :rule-classes :type-prescription)

Theorem: svex-maskbits-for-vars-of-svarlist-fix-vars

(defthm svex-maskbits-for-vars-of-svarlist-fix-vars
  (equal (svex-maskbits-for-vars (svarlist-fix vars)
                                 masks boolmasks)
         (svex-maskbits-for-vars vars masks boolmasks)))

Theorem: svex-maskbits-for-vars-svarlist-equiv-congruence-on-vars

(defthm svex-maskbits-for-vars-svarlist-equiv-congruence-on-vars
  (implies
       (svarlist-equiv vars vars-equiv)
       (equal (svex-maskbits-for-vars vars masks boolmasks)
              (svex-maskbits-for-vars vars-equiv masks boolmasks)))
  :rule-classes :congruence)

Theorem: svex-maskbits-for-vars-of-svex-mask-alist-fix-masks

(defthm svex-maskbits-for-vars-of-svex-mask-alist-fix-masks
  (equal (svex-maskbits-for-vars vars (svex-mask-alist-fix masks)
                                 boolmasks)
         (svex-maskbits-for-vars vars masks boolmasks)))

Theorem: svex-maskbits-for-vars-svex-mask-alist-equiv-congruence-on-masks

(defthm
   svex-maskbits-for-vars-svex-mask-alist-equiv-congruence-on-masks
  (implies
       (svex-mask-alist-equiv masks masks-equiv)
       (equal (svex-maskbits-for-vars vars masks boolmasks)
              (svex-maskbits-for-vars vars masks-equiv boolmasks)))
  :rule-classes :congruence)

Theorem: svex-maskbits-for-vars-of-svar-boolmasks-fix-boolmasks

(defthm svex-maskbits-for-vars-of-svar-boolmasks-fix-boolmasks
  (equal
       (svex-maskbits-for-vars vars
                               masks (svar-boolmasks-fix boolmasks))
       (svex-maskbits-for-vars vars masks boolmasks)))

Theorem: svex-maskbits-for-vars-svar-boolmasks-equiv-congruence-on-boolmasks

(defthm
 svex-maskbits-for-vars-svar-boolmasks-equiv-congruence-on-boolmasks
 (implies
      (svar-boolmasks-equiv boolmasks boolmasks-equiv)
      (equal (svex-maskbits-for-vars vars masks boolmasks)
             (svex-maskbits-for-vars vars masks boolmasks-equiv)))
 :rule-classes :congruence)