		Search-engine friendly clone of the ACL2 documentation.

Lhs.lisp

Lhs-check-masks

Signature
(lhs-check-masks x mask-acc conf-acc) → (mv mask-acc1 conf-acc1)
Arguments: x — Guard (lhs-p x).; mask-acc — Guard (4vmask-alist-p mask-acc).; conf-acc — Guard (4vmask-alist-p conf-acc).
Returns: mask-acc1 — Type (4vmask-alist-p mask-acc1).; conf-acc1 — Type (4vmask-alist-p conf-acc1).

Definitions and Theorems

Function: lhs-check-masks

(defun lhs-check-masks (x mask-acc conf-acc)
 (declare (xargs :guard (and (lhs-p x)
                             (4vmask-alist-p mask-acc)
                             (4vmask-alist-p conf-acc))))
 (let ((__function__ 'lhs-check-masks))
  (declare (ignorable __function__))
  (b*
   ((mask-acc (4vmask-alist-fix mask-acc))
    (conf-acc (4vmask-alist-fix conf-acc))
    ((mv first rest) (lhs-decomp x))
    ((unless first) (mv mask-acc conf-acc))
    ((lhrange first) first)
    ((when (eq (lhatom-kind first.atom) :z))
     (lhs-check-masks rest mask-acc conf-acc))
    ((lhatom-var first.atom) first.atom)
    (firstmask
     (sparseint-concatenate first.atom.rsh
                            0 (sparseint-concatenate first.w -1 0)))
    (varmask (or (cdr (hons-get first.atom.name mask-acc))
                 0))
    (conflict (sparseint-bitand varmask firstmask))
    (mask-acc (hons-acons first.atom.name
                          (sparseint-bitor firstmask varmask)
                          mask-acc))
    (conf-acc
     (if (sparseint-bit 0 conflict)
         conf-acc
      (hons-acons first.atom.name
                  (sparseint-bitor
                       conflict
                       (or (cdr (hons-get first.atom.name conf-acc))
                           0))
                  conf-acc))))
   (lhs-check-masks rest mask-acc conf-acc))))

Theorem: 4vmask-alist-p-of-lhs-check-masks.mask-acc1

(defthm 4vmask-alist-p-of-lhs-check-masks.mask-acc1
  (b* (((mv ?mask-acc1 ?conf-acc1)
        (lhs-check-masks x mask-acc conf-acc)))
    (4vmask-alist-p mask-acc1))
  :rule-classes :rewrite)

Theorem: 4vmask-alist-p-of-lhs-check-masks.conf-acc1

(defthm 4vmask-alist-p-of-lhs-check-masks.conf-acc1
  (b* (((mv ?mask-acc1 ?conf-acc1)
        (lhs-check-masks x mask-acc conf-acc)))
    (4vmask-alist-p conf-acc1))
  :rule-classes :rewrite)

Theorem: lhs-check-masks-of-lhs-fix-x

(defthm lhs-check-masks-of-lhs-fix-x
  (equal (lhs-check-masks (lhs-fix x)
                          mask-acc conf-acc)
         (lhs-check-masks x mask-acc conf-acc)))

Theorem: lhs-check-masks-lhs-equiv-congruence-on-x

(defthm lhs-check-masks-lhs-equiv-congruence-on-x
  (implies (lhs-equiv x x-equiv)
           (equal (lhs-check-masks x mask-acc conf-acc)
                  (lhs-check-masks x-equiv mask-acc conf-acc)))
  :rule-classes :congruence)

Theorem: lhs-check-masks-of-4vmask-alist-fix-mask-acc

(defthm lhs-check-masks-of-4vmask-alist-fix-mask-acc
  (equal (lhs-check-masks x (4vmask-alist-fix mask-acc)
                          conf-acc)
         (lhs-check-masks x mask-acc conf-acc)))

Theorem: lhs-check-masks-4vmask-alist-equiv-congruence-on-mask-acc

(defthm lhs-check-masks-4vmask-alist-equiv-congruence-on-mask-acc
  (implies (4vmask-alist-equiv mask-acc mask-acc-equiv)
           (equal (lhs-check-masks x mask-acc conf-acc)
                  (lhs-check-masks x mask-acc-equiv conf-acc)))
  :rule-classes :congruence)

Theorem: lhs-check-masks-of-4vmask-alist-fix-conf-acc

(defthm lhs-check-masks-of-4vmask-alist-fix-conf-acc
  (equal (lhs-check-masks x mask-acc (4vmask-alist-fix conf-acc))
         (lhs-check-masks x mask-acc conf-acc)))

Theorem: lhs-check-masks-4vmask-alist-equiv-congruence-on-conf-acc

(defthm lhs-check-masks-4vmask-alist-equiv-congruence-on-conf-acc
  (implies (4vmask-alist-equiv conf-acc conf-acc-equiv)
           (equal (lhs-check-masks x mask-acc conf-acc)
                  (lhs-check-masks x mask-acc conf-acc-equiv)))
  :rule-classes :congruence)