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.
(sv::svex-alist->assigns acl2::x sv::sizes sv::masks) → sv::assigns
Function:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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)