		Search-engine friendly clone of the ACL2 documentation.

Rewriting

Svexlist-rewrite-under-masks

Rewrite the list of expressions under the provided mask alist, which should already be complete.

Signature
(svexlist-rewrite-under-masks x masks &key (verbosep 'nil)) → xx
Arguments: x — Guard (svexlist-p x).; masks — Guard (svex-mask-alist-p masks).
Returns: xx — Type (svexlist-p xx).

Definitions and Theorems

Function: svexlist-rewrite-under-masks-fn

(defun svexlist-rewrite-under-masks-fn (x masks verbosep)
 (declare (xargs :guard (and (svexlist-p x)
                             (svex-mask-alist-p masks))))
 (let ((__function__ 'svexlist-rewrite-under-masks))
  (declare (ignorable __function__))
  (b*
   ((multirefs (svexlist-multirefs-top x))
    (-
     (and
        verbosep
        (cw "opcount before rewrite: ~x0 multiply-referenced: ~x1~%"
            (cwtime (svexlist-opcount x))
            (len multirefs))))
    ((mv new-x out-multirefs memo)
     (cwtime (svexlist-rewrite x masks multirefs nil nil)
             :mintime 1))
    (- (clear-memoize-table 'svex-rewrite)
       (fast-alist-free memo)
       (fast-alist-free out-multirefs)
       (fast-alist-free multirefs)
       (and verbosep
            (cw "opcount after rewrite: ~x0~%"
                (cwtime (svexlist-opcount new-x))))))
   new-x)))

Theorem: svexlist-p-of-svexlist-rewrite-under-masks

(defthm svexlist-p-of-svexlist-rewrite-under-masks
  (b* ((xx (svexlist-rewrite-under-masks-fn x masks verbosep)))
    (svexlist-p xx))
  :rule-classes :rewrite)

Theorem: svexlist-rewrite-under-masks-fn-of-svexlist-fix-x

(defthm svexlist-rewrite-under-masks-fn-of-svexlist-fix-x
  (equal (svexlist-rewrite-under-masks-fn (svexlist-fix x)
                                          masks verbosep)
         (svexlist-rewrite-under-masks-fn x masks verbosep)))

Theorem: svexlist-rewrite-under-masks-fn-svexlist-equiv-congruence-on-x

(defthm
     svexlist-rewrite-under-masks-fn-svexlist-equiv-congruence-on-x
 (implies
   (svexlist-equiv x x-equiv)
   (equal (svexlist-rewrite-under-masks-fn x masks verbosep)
          (svexlist-rewrite-under-masks-fn x-equiv masks verbosep)))
 :rule-classes :congruence)

Theorem: svexlist-rewrite-under-masks-fn-of-svex-mask-alist-fix-masks

(defthm svexlist-rewrite-under-masks-fn-of-svex-mask-alist-fix-masks
 (equal
      (svexlist-rewrite-under-masks-fn x (svex-mask-alist-fix masks)
                                       verbosep)
      (svexlist-rewrite-under-masks-fn x masks verbosep)))

Theorem: svexlist-rewrite-under-masks-fn-svex-mask-alist-equiv-congruence-on-masks

(defthm
 svexlist-rewrite-under-masks-fn-svex-mask-alist-equiv-congruence-on-masks
 (implies
   (svex-mask-alist-equiv masks masks-equiv)
   (equal (svexlist-rewrite-under-masks-fn x masks verbosep)
          (svexlist-rewrite-under-masks-fn x masks-equiv verbosep)))
 :rule-classes :congruence)

Theorem: svexlist-rewrite-under-masks-correct

(defthm svexlist-rewrite-under-masks-correct
 (implies
  (svex-mask-alist-complete masks)
  (equal
   (4veclist-mask
    (svex-argmasks-lookup x masks)
    (svexlist-eval (svexlist-rewrite-under-masks x masks
                                                 :verbosep verbosep)
                   env))
   (4veclist-mask (svex-argmasks-lookup x masks)
                  (svexlist-eval x env)))))

Theorem: len-of-svexlist-rewrite-under-masks

(defthm len-of-svexlist-rewrite-under-masks
  (equal (len (svexlist-rewrite-under-masks x masks
                                            :verbosep verbosep))
         (len x)))

Theorem: vars-of-svexlist-rewrite-under-masks

(defthm vars-of-svexlist-rewrite-under-masks
 (implies
  (not (member v (svexlist-vars x)))
  (not
    (member
         v
         (svexlist-vars
              (svexlist-rewrite-under-masks x masks
                                            :verbosep verbosep))))))