		Search-engine friendly clone of the ACL2 documentation.

Bit-blasting

4vmask-to-a4vec-rec-env

Signature
(4vmask-to-a4vec-rec-env mask boolmask upper lower nextvar) → env
Arguments: mask — Guard (4vmask-p mask).; boolmask — Guard (integerp boolmask).; upper — Guard (integerp upper).; lower — Guard (integerp lower).; nextvar — Guard (natp nextvar).
Returns: env — environment for the resulting 4vmask.

Definitions and Theorems

Function: 4vmask-to-a4vec-rec-env

(defun 4vmask-to-a4vec-rec-env (mask boolmask upper lower nextvar)
 (declare (xargs :guard (and (4vmask-p mask)
                             (integerp boolmask)
                             (integerp upper)
                             (integerp lower)
                             (natp nextvar))))
 (declare (xargs :guard (not (sparseint-< mask 0))))
 (let ((__function__ '4vmask-to-a4vec-rec-env))
  (declare (ignorable __function__))
  (b*
   ((mask (sparseint-nfix (4vmask-fix mask)))
    (nextvar (lnfix nextvar))
    ((when (sparseint-equal mask 0)) nil)
    (rest-env
         (4vmask-to-a4vec-rec-env (sparseint-rightshift 1 mask)
                                  (logcdr boolmask)
                                  (logcdr upper)
                                  (logcdr lower)
                                  (if (eql 1 (sparseint-bit 0 mask))
                                      (if (logbitp 0 boolmask)
                                          (+ 1 nextvar)
                                        (+ 2 nextvar))
                                    nextvar))))
   (if (eql 1 (sparseint-bit 0 mask))
       (cons (cons nextvar (logbitp 0 upper))
             (if (logbitp 0 boolmask)
                 rest-env
               (cons (cons (1+ nextvar) (logbitp 0 lower))
                     rest-env)))
     rest-env))))

Theorem: key-exists-in-4vmask-to-a4vec-rec-env

(defthm key-exists-in-4vmask-to-a4vec-rec-env
 (iff
   (hons-assoc-equal
        v
        (4vmask-to-a4vec-rec-env mask boolmask upper lower nextvar))
   (and (natp v)
        (<= (nfix nextvar) v)
        (< v
           (+ (nfix nextvar)
              (4vmask-to-a4vec-varcount mask boolmask))))))

Theorem: nat-bool-aig-list->s-of-cons-nonmember

(defthm nat-bool-aig-list->s-of-cons-nonmember
  (implies (and (nat-bool-listp x)
                (not (member n (nat-bool-list-nats x))))
           (equal (aig-list->s x (cons (cons n v) env))
                  (aig-list->s x env))))

Theorem: eval-4vmask-to-a4vec-rec-with-env

(defthm eval-4vmask-to-a4vec-rec-with-env
 (b*
  (((mv uppera lowera)
    (4vmask-to-a4vec-rec mask boolmask nextvar))
   (env
       (4vmask-to-a4vec-rec-env mask boolmask upper lower nextvar)))
  (and
    (equal (logand (nfix (sparseint-val (4vmask-fix mask)))
                   (aig-list->s uppera env))
           (logand (nfix (sparseint-val (4vmask-fix mask)))
                   upper))
    (implies (eql 0
                  (logand boolmask (logxor upper lower)))
             (equal (logand (nfix (sparseint-val (4vmask-fix mask)))
                            (aig-list->s lowera env))
                    (logand (nfix (sparseint-val (4vmask-fix mask)))
                            lower))))))

Theorem: 4vmask-to-a4vec-rec-env-of-4vmask-fix-mask

(defthm 4vmask-to-a4vec-rec-env-of-4vmask-fix-mask
  (equal
       (4vmask-to-a4vec-rec-env (4vmask-fix mask)
                                boolmask upper lower nextvar)
       (4vmask-to-a4vec-rec-env mask boolmask upper lower nextvar)))

Theorem: 4vmask-to-a4vec-rec-env-4vmask-equiv-congruence-on-mask

(defthm 4vmask-to-a4vec-rec-env-4vmask-equiv-congruence-on-mask
 (implies
  (4vmask-equiv mask mask-equiv)
  (equal (4vmask-to-a4vec-rec-env mask boolmask upper lower nextvar)
         (4vmask-to-a4vec-rec-env mask-equiv
                                  boolmask upper lower nextvar)))
 :rule-classes :congruence)

Theorem: 4vmask-to-a4vec-rec-env-of-ifix-boolmask

(defthm 4vmask-to-a4vec-rec-env-of-ifix-boolmask
  (equal
       (4vmask-to-a4vec-rec-env mask (ifix boolmask)
                                upper lower nextvar)
       (4vmask-to-a4vec-rec-env mask boolmask upper lower nextvar)))

Theorem: 4vmask-to-a4vec-rec-env-int-equiv-congruence-on-boolmask

(defthm 4vmask-to-a4vec-rec-env-int-equiv-congruence-on-boolmask
 (implies
  (int-equiv boolmask boolmask-equiv)
  (equal
      (4vmask-to-a4vec-rec-env mask boolmask upper lower nextvar)
      (4vmask-to-a4vec-rec-env mask
                               boolmask-equiv upper lower nextvar)))
 :rule-classes :congruence)

Theorem: 4vmask-to-a4vec-rec-env-of-ifix-upper

(defthm 4vmask-to-a4vec-rec-env-of-ifix-upper
  (equal
       (4vmask-to-a4vec-rec-env mask boolmask (ifix upper)
                                lower nextvar)
       (4vmask-to-a4vec-rec-env mask boolmask upper lower nextvar)))

Theorem: 4vmask-to-a4vec-rec-env-int-equiv-congruence-on-upper

(defthm 4vmask-to-a4vec-rec-env-int-equiv-congruence-on-upper
 (implies
  (int-equiv upper upper-equiv)
  (equal
      (4vmask-to-a4vec-rec-env mask boolmask upper lower nextvar)
      (4vmask-to-a4vec-rec-env mask
                               boolmask upper-equiv lower nextvar)))
 :rule-classes :congruence)

Theorem: 4vmask-to-a4vec-rec-env-of-ifix-lower

(defthm 4vmask-to-a4vec-rec-env-of-ifix-lower
  (equal
       (4vmask-to-a4vec-rec-env mask boolmask upper (ifix lower)
                                nextvar)
       (4vmask-to-a4vec-rec-env mask boolmask upper lower nextvar)))

Theorem: 4vmask-to-a4vec-rec-env-int-equiv-congruence-on-lower

(defthm 4vmask-to-a4vec-rec-env-int-equiv-congruence-on-lower
 (implies
  (int-equiv lower lower-equiv)
  (equal
      (4vmask-to-a4vec-rec-env mask boolmask upper lower nextvar)
      (4vmask-to-a4vec-rec-env mask
                               boolmask upper lower-equiv nextvar)))
 :rule-classes :congruence)

Theorem: 4vmask-to-a4vec-rec-env-of-nfix-nextvar

(defthm 4vmask-to-a4vec-rec-env-of-nfix-nextvar
  (equal
       (4vmask-to-a4vec-rec-env mask
                                boolmask upper lower (nfix nextvar))
       (4vmask-to-a4vec-rec-env mask boolmask upper lower nextvar)))

Theorem: 4vmask-to-a4vec-rec-env-nat-equiv-congruence-on-nextvar

(defthm 4vmask-to-a4vec-rec-env-nat-equiv-congruence-on-nextvar
 (implies
  (nat-equiv nextvar nextvar-equiv)
  (equal
      (4vmask-to-a4vec-rec-env mask boolmask upper lower nextvar)
      (4vmask-to-a4vec-rec-env mask
                               boolmask upper lower nextvar-equiv)))
 :rule-classes :congruence)