		Search-engine friendly clone of the ACL2 documentation.

Svstmt-compile.lisp

Svstmt-lhs-check-masks

Signature
(svstmt-lhs-check-masks blk-masks nonblk-masks full-lhs blockingp stack) → (mv new-blk-masks new-nonblk-masks conflicts)
Arguments: blk-masks — Guard (4vmask-alist-p blk-masks).; nonblk-masks — Guard (4vmask-alist-p nonblk-masks).; full-lhs — Guard (lhs-p full-lhs).; stack — Guard (svstack-p stack).
Returns: new-blk-masks — Type (4vmask-alist-p new-blk-masks).; new-nonblk-masks — Type (4vmask-alist-p new-nonblk-masks).; conflicts — Type (4vmask-alist-p conflicts).

Definitions and Theorems

Function: svstmt-lhs-check-masks

(defun svstmt-lhs-check-masks
       (blk-masks nonblk-masks full-lhs blockingp stack)
 (declare (xargs :guard (and (4vmask-alist-p blk-masks)
                             (4vmask-alist-p nonblk-masks)
                             (lhs-p full-lhs)
                             (svstack-p stack))))
 (declare (xargs :guard (consp stack)))
 (let ((__function__ 'svstmt-lhs-check-masks))
   (declare (ignorable __function__))
   (b*
     (((mv masks1 conflicts)
       (lhs-check-masks full-lhs nil nil))
      (- (fast-alist-free masks1))
      (filtered-lhs (svstack-filter-global-lhs-vars full-lhs stack))
      ((mv new-masks confs1)
       (lhs-check-masks filtered-lhs
                        (if blockingp blk-masks nonblk-masks)
                        nil)))
     (fast-alist-free confs1)
     (if blockingp (mv new-masks
                       (4vmask-alist-fix nonblk-masks)
                       conflicts)
       (mv (4vmask-alist-fix blk-masks)
           new-masks conflicts)))))

Theorem: 4vmask-alist-p-of-svstmt-lhs-check-masks.new-blk-masks

(defthm 4vmask-alist-p-of-svstmt-lhs-check-masks.new-blk-masks
 (b*
  (((mv ?new-blk-masks
        ?new-nonblk-masks ?conflicts)
    (svstmt-lhs-check-masks blk-masks
                            nonblk-masks full-lhs blockingp stack)))
  (4vmask-alist-p new-blk-masks))
 :rule-classes :rewrite)

Theorem: 4vmask-alist-p-of-svstmt-lhs-check-masks.new-nonblk-masks

(defthm 4vmask-alist-p-of-svstmt-lhs-check-masks.new-nonblk-masks
 (b*
  (((mv ?new-blk-masks
        ?new-nonblk-masks ?conflicts)
    (svstmt-lhs-check-masks blk-masks
                            nonblk-masks full-lhs blockingp stack)))
  (4vmask-alist-p new-nonblk-masks))
 :rule-classes :rewrite)

Theorem: 4vmask-alist-p-of-svstmt-lhs-check-masks.conflicts

(defthm 4vmask-alist-p-of-svstmt-lhs-check-masks.conflicts
 (b*
  (((mv ?new-blk-masks
        ?new-nonblk-masks ?conflicts)
    (svstmt-lhs-check-masks blk-masks
                            nonblk-masks full-lhs blockingp stack)))
  (4vmask-alist-p conflicts))
 :rule-classes :rewrite)

Theorem: svstmt-lhs-check-masks-of-4vmask-alist-fix-blk-masks

(defthm svstmt-lhs-check-masks-of-4vmask-alist-fix-blk-masks
 (equal
    (svstmt-lhs-check-masks (4vmask-alist-fix blk-masks)
                            nonblk-masks full-lhs blockingp stack)
    (svstmt-lhs-check-masks blk-masks
                            nonblk-masks full-lhs blockingp stack)))

Theorem: svstmt-lhs-check-masks-4vmask-alist-equiv-congruence-on-blk-masks

(defthm
  svstmt-lhs-check-masks-4vmask-alist-equiv-congruence-on-blk-masks
 (implies
  (4vmask-alist-equiv blk-masks blk-masks-equiv)
  (equal
    (svstmt-lhs-check-masks blk-masks
                            nonblk-masks full-lhs blockingp stack)
    (svstmt-lhs-check-masks blk-masks-equiv
                            nonblk-masks full-lhs blockingp stack)))
 :rule-classes :congruence)

Theorem: svstmt-lhs-check-masks-of-4vmask-alist-fix-nonblk-masks

(defthm svstmt-lhs-check-masks-of-4vmask-alist-fix-nonblk-masks
 (equal
    (svstmt-lhs-check-masks blk-masks
                            (4vmask-alist-fix nonblk-masks)
                            full-lhs blockingp stack)
    (svstmt-lhs-check-masks blk-masks
                            nonblk-masks full-lhs blockingp stack)))

Theorem: svstmt-lhs-check-masks-4vmask-alist-equiv-congruence-on-nonblk-masks

(defthm
 svstmt-lhs-check-masks-4vmask-alist-equiv-congruence-on-nonblk-masks
 (implies
  (4vmask-alist-equiv nonblk-masks nonblk-masks-equiv)
  (equal
      (svstmt-lhs-check-masks blk-masks
                              nonblk-masks full-lhs blockingp stack)
      (svstmt-lhs-check-masks blk-masks nonblk-masks-equiv
                              full-lhs blockingp stack)))
 :rule-classes :congruence)

Theorem: svstmt-lhs-check-masks-of-lhs-fix-full-lhs

(defthm svstmt-lhs-check-masks-of-lhs-fix-full-lhs
 (equal
    (svstmt-lhs-check-masks blk-masks
                            nonblk-masks (lhs-fix full-lhs)
                            blockingp stack)
    (svstmt-lhs-check-masks blk-masks
                            nonblk-masks full-lhs blockingp stack)))

Theorem: svstmt-lhs-check-masks-lhs-equiv-congruence-on-full-lhs

(defthm svstmt-lhs-check-masks-lhs-equiv-congruence-on-full-lhs
 (implies
  (lhs-equiv full-lhs full-lhs-equiv)
  (equal
      (svstmt-lhs-check-masks blk-masks
                              nonblk-masks full-lhs blockingp stack)
      (svstmt-lhs-check-masks blk-masks nonblk-masks
                              full-lhs-equiv blockingp stack)))
 :rule-classes :congruence)

Theorem: svstmt-lhs-check-masks-of-svstack-fix-stack

(defthm svstmt-lhs-check-masks-of-svstack-fix-stack
 (equal
    (svstmt-lhs-check-masks blk-masks nonblk-masks
                            full-lhs blockingp (svstack-fix stack))
    (svstmt-lhs-check-masks blk-masks
                            nonblk-masks full-lhs blockingp stack)))

Theorem: svstmt-lhs-check-masks-svstack-equiv-congruence-on-stack

(defthm svstmt-lhs-check-masks-svstack-equiv-congruence-on-stack
 (implies
  (svstack-equiv stack stack-equiv)
  (equal
      (svstmt-lhs-check-masks blk-masks
                              nonblk-masks full-lhs blockingp stack)
      (svstmt-lhs-check-masks blk-masks nonblk-masks
                              full-lhs blockingp stack-equiv)))
 :rule-classes :congruence)