Given a variable and a mask of bits, create an LHS that covers those bits.
(sv::svar->lhs-by-mask acl2::x sv::mask) → sv::lhs
Fails by returning an empty LHS if the mask is negative, i.e. an ~ infinite range of bits should be written.
Function:
(defun sv::svar->lhs-by-mask (acl2::x sv::mask) (declare (xargs :guard (and (sv::svar-p acl2::x) (sv::4vmask-p sv::mask)))) (let ((__function__ 'sv::svar->lhs-by-mask)) (declare (ignorable __function__)) (and (bitops::sparseint-< 0 (sv::4vmask-fix sv::mask)) (list (sv::make-lhrange :w (bitops::sparseint-length (sv::4vmask-fix sv::mask)) :atom (sv::make-lhatom-var :name acl2::x :rsh 0))))))
Theorem:
(defthm sv::lhs-p-of-svar->lhs-by-mask (b* ((sv::lhs (sv::svar->lhs-by-mask acl2::x sv::mask))) (sv::lhs-p sv::lhs)) :rule-classes :rewrite)
Theorem:
(defthm sv::vars-of-svar->lhs-by-mask (implies (not (equal sv::v (sv::svar-fix acl2::x))) (not (member sv::v (sv::lhs-vars (sv::svar->lhs-by-mask acl2::x sv::mask))))))
Theorem:
(defthm sv::svar->lhs-by-mask-of-svar-fix-x (equal (sv::svar->lhs-by-mask (sv::svar-fix acl2::x) sv::mask) (sv::svar->lhs-by-mask acl2::x sv::mask)))
Theorem:
(defthm sv::svar->lhs-by-mask-svar-equiv-congruence-on-x (implies (sv::svar-equiv acl2::x sv::x-equiv) (equal (sv::svar->lhs-by-mask acl2::x sv::mask) (sv::svar->lhs-by-mask sv::x-equiv sv::mask))) :rule-classes :congruence)
Theorem:
(defthm sv::svar->lhs-by-mask-of-4vmask-fix-mask (equal (sv::svar->lhs-by-mask acl2::x (sv::4vmask-fix sv::mask)) (sv::svar->lhs-by-mask acl2::x sv::mask)))
Theorem:
(defthm sv::svar->lhs-by-mask-4vmask-equiv-congruence-on-mask (implies (sv::4vmask-equiv sv::mask sv::mask-equiv) (equal (sv::svar->lhs-by-mask acl2::x sv::mask) (sv::svar->lhs-by-mask acl2::x sv::mask-equiv))) :rule-classes :congruence)