		Search-engine friendly clone of the ACL2 documentation.

Vl-svstmt.lisp

Sv::svex-alist->assigns

Given an svex alist, return an assignment alist, i.e. transform the bound variables into LHSes based on the given masks, which represent the bits of the variables that are supposed to be written.

Signature
(sv::svex-alist->assigns acl2::x sv::sizes sv::masks) → sv::assigns
Arguments: acl2::x — Guard (sv::svex-alist-p acl2::x).; sv::sizes — Guard (sv::svar-size-alist-p sv::sizes).; sv::masks — Guard (sv::4vmask-alist-p sv::masks).
Returns: sv::assigns — Type (sv::assigns-p sv::assigns).

Definitions and Theorems

Function: svex-alist->assigns

(defun sv::svex-alist->assigns (acl2::x sv::sizes sv::masks)
 (declare (xargs :guard (and (sv::svex-alist-p acl2::x)
                             (sv::svar-size-alist-p sv::sizes)
                             (sv::4vmask-alist-p sv::masks))))
 (let ((__function__ 'sv::svex-alist->assigns))
  (declare (ignorable __function__))
  (b* ((acl2::x (sv::svex-alist-fix acl2::x))
       (sv::masks (sv::4vmask-alist-fix sv::masks))
       (sv::sizes (sv::svar-size-alist-fix sv::sizes))
       ((when (atom acl2::x)) nil)
       ((cons sv::var sv::rhs) (car acl2::x))
       (sv::mask (or (cdr (hons-get sv::var sv::masks))
                     0))
       (sv::size (cdr (hons-get sv::var sv::sizes)))
       (- (or sv::size
              (raise "error: expected all sizes to be bound")))
       (sv::size (or sv::size 0))
       (sv::lhs (sv::svar->lhs-by-size sv::var sv::size))
       (sv::fullmaskp
            (bitops::sparseint-equal
                 sv::mask
                 (bitops::sparseint-concatenate sv::size -1 0)))
       ((when sv::fullmaskp)
        (cons (cons sv::lhs
                    (sv::make-driver :value sv::rhs))
              (sv::svex-alist->assigns (cdr acl2::x)
                                       sv::sizes sv::masks))))
   (list*
    (cons
     sv::lhs
     (sv::make-driver
      :value
      (sv::make-svex-call
       :fn 'sv::bit?
       :args
       (list
        (sv::svex-quote (sv::2vec (bitops::sparseint-val sv::mask)))
        sv::rhs (sv::svex-z)))))
    (sv::svex-alist->assigns (cdr acl2::x)
                             sv::sizes sv::masks)))))

Theorem: assigns-p-of-svex-alist->assigns

(defthm sv::assigns-p-of-svex-alist->assigns
  (b* ((sv::assigns
            (sv::svex-alist->assigns acl2::x sv::sizes sv::masks)))
    (sv::assigns-p sv::assigns))
  :rule-classes :rewrite)

Theorem: vars-of-svex-alist->assigns

(defthm sv::vars-of-svex-alist->assigns
 (implies
  (and (not (member sv::v (sv::svex-alist-keys acl2::x)))
       (not (member sv::v (sv::svex-alist-vars acl2::x))))
  (not
   (member
     sv::v
     (sv::assigns-vars
          (sv::svex-alist->assigns acl2::x sv::sizes sv::masks))))))

Theorem: svex-alist->assigns-of-svex-alist-fix-x

(defthm sv::svex-alist->assigns-of-svex-alist-fix-x
  (equal (sv::svex-alist->assigns (sv::svex-alist-fix acl2::x)
                                  sv::sizes sv::masks)
         (sv::svex-alist->assigns acl2::x sv::sizes sv::masks)))

Theorem: svex-alist->assigns-svex-alist-equiv-congruence-on-x

(defthm sv::svex-alist->assigns-svex-alist-equiv-congruence-on-x
 (implies
  (sv::svex-alist-equiv acl2::x sv::x-equiv)
  (equal (sv::svex-alist->assigns acl2::x sv::sizes sv::masks)
         (sv::svex-alist->assigns sv::x-equiv sv::sizes sv::masks)))
 :rule-classes :congruence)

Theorem: svex-alist->assigns-of-svar-size-alist-fix-sizes

(defthm sv::svex-alist->assigns-of-svar-size-alist-fix-sizes
 (equal (sv::svex-alist->assigns acl2::x
                                 (sv::svar-size-alist-fix sv::sizes)
                                 sv::masks)
        (sv::svex-alist->assigns acl2::x sv::sizes sv::masks)))

Theorem: svex-alist->assigns-svar-size-alist-equiv-congruence-on-sizes

(defthm
  sv::svex-alist->assigns-svar-size-alist-equiv-congruence-on-sizes
 (implies
  (sv::svar-size-alist-equiv sv::sizes sv::sizes-equiv)
  (equal
       (sv::svex-alist->assigns acl2::x sv::sizes sv::masks)
       (sv::svex-alist->assigns acl2::x sv::sizes-equiv sv::masks)))
 :rule-classes :congruence)

Theorem: svex-alist->assigns-of-4vmask-alist-fix-masks

(defthm sv::svex-alist->assigns-of-4vmask-alist-fix-masks
  (equal (sv::svex-alist->assigns acl2::x sv::sizes
                                  (sv::4vmask-alist-fix sv::masks))
         (sv::svex-alist->assigns acl2::x sv::sizes sv::masks)))

Theorem: svex-alist->assigns-4vmask-alist-equiv-congruence-on-masks

(defthm
     sv::svex-alist->assigns-4vmask-alist-equiv-congruence-on-masks
 (implies
  (sv::4vmask-alist-equiv sv::masks sv::masks-equiv)
  (equal
       (sv::svex-alist->assigns acl2::x sv::sizes sv::masks)
       (sv::svex-alist->assigns acl2::x sv::sizes sv::masks-equiv)))
 :rule-classes :congruence)