		Search-engine friendly clone of the ACL2 documentation.

Bit-blasting

Svexlist->a4vecs-for-varlist

Creates a symbolic bit-level representation for x, assuming that vars are the only vars relevant to x and that the bits of vars given in boolmasks are Boolean-valued.

Signature
(svexlist->a4vecs-for-varlist x vars boolmasks) → (mv err a4vecs)
Arguments: x — Guard (svexlist-p x).; vars — Guard (svarlist-p vars).; boolmasks — Guard (svar-boolmasks-p boolmasks).
Returns: err — Type (iff err (not (svex-maskbits-ok vars (svexlist-mask-alist x)))).; a4vecs — Type (a4veclist-p a4vecs).

Steps: First creates a symbolic environment mapping the variables to a4vec structures, each bit of which is a free variable. (For bits constrained to be Boolean by boolmasks, the same variable is shared for upper/lower.) Then uses svexlist->a4vec-top to generate a4vecs corresponding to the svexes.

Definitions and Theorems

Function: svexlist->a4vecs-for-varlist

(defun svexlist->a4vecs-for-varlist (x vars boolmasks)
  (declare (xargs :guard (and (svexlist-p x)
                              (svarlist-p vars)
                              (svar-boolmasks-p boolmasks))))
  (let ((__function__ 'svexlist->a4vecs-for-varlist))
    (declare (ignorable __function__))
    (b* ((masks (svexlist-mask-alist-memo x))
         ((mv err a4env)
          (svex-varmasks->a4env vars masks boolmasks))
         ((when err) (mv err nil))
         (a4env (make-fast-alist a4env))
         (res (svexlist->a4vec-top x a4env masks))
         (?ign (fast-alist-free a4env)))
      (mv nil res))))

Theorem: return-type-of-svexlist->a4vecs-for-varlist.err

(defthm return-type-of-svexlist->a4vecs-for-varlist.err
  (b* (((mv ?err ?a4vecs)
        (svexlist->a4vecs-for-varlist x vars boolmasks)))
    (iff err
         (not (svex-maskbits-ok vars (svexlist-mask-alist x)))))
  :rule-classes :rewrite)

Theorem: a4veclist-p-of-svexlist->a4vecs-for-varlist.a4vecs

(defthm a4veclist-p-of-svexlist->a4vecs-for-varlist.a4vecs
  (b* (((mv ?err ?a4vecs)
        (svexlist->a4vecs-for-varlist x vars boolmasks)))
    (a4veclist-p a4vecs))
  :rule-classes :rewrite)

Theorem: svexlist->a4vecs-for-varlist-of-svexlist-fix-x

(defthm svexlist->a4vecs-for-varlist-of-svexlist-fix-x
  (equal (svexlist->a4vecs-for-varlist (svexlist-fix x)
                                       vars boolmasks)
         (svexlist->a4vecs-for-varlist x vars boolmasks)))

Theorem: svexlist->a4vecs-for-varlist-svexlist-equiv-congruence-on-x

(defthm svexlist->a4vecs-for-varlist-svexlist-equiv-congruence-on-x
 (implies
      (svexlist-equiv x x-equiv)
      (equal (svexlist->a4vecs-for-varlist x vars boolmasks)
             (svexlist->a4vecs-for-varlist x-equiv vars boolmasks)))
 :rule-classes :congruence)

Theorem: svexlist->a4vecs-for-varlist-of-svarlist-fix-vars

(defthm svexlist->a4vecs-for-varlist-of-svarlist-fix-vars
  (equal (svexlist->a4vecs-for-varlist x (svarlist-fix vars)
                                       boolmasks)
         (svexlist->a4vecs-for-varlist x vars boolmasks)))

Theorem: svexlist->a4vecs-for-varlist-svarlist-equiv-congruence-on-vars

(defthm
     svexlist->a4vecs-for-varlist-svarlist-equiv-congruence-on-vars
 (implies
      (svarlist-equiv vars vars-equiv)
      (equal (svexlist->a4vecs-for-varlist x vars boolmasks)
             (svexlist->a4vecs-for-varlist x vars-equiv boolmasks)))
 :rule-classes :congruence)

Theorem: svexlist->a4vecs-for-varlist-of-svar-boolmasks-fix-boolmasks

(defthm svexlist->a4vecs-for-varlist-of-svar-boolmasks-fix-boolmasks
  (equal (svexlist->a4vecs-for-varlist
              x vars (svar-boolmasks-fix boolmasks))
         (svexlist->a4vecs-for-varlist x vars boolmasks)))

Theorem: svexlist->a4vecs-for-varlist-svar-boolmasks-equiv-congruence-on-boolmasks

(defthm
 svexlist->a4vecs-for-varlist-svar-boolmasks-equiv-congruence-on-boolmasks
 (implies
      (svar-boolmasks-equiv boolmasks boolmasks-equiv)
      (equal (svexlist->a4vecs-for-varlist x vars boolmasks)
             (svexlist->a4vecs-for-varlist x vars boolmasks-equiv)))
 :rule-classes :congruence)