		Search-engine friendly clone of the ACL2 documentation.

Rewriting

Svexlist-rewrite-top

Signature
(svexlist-rewrite-top x &key (verbosep 'nil)) → xx
Arguments: x — Guard (svexlist-p x).
Returns: xx — Type (svexlist-p xx).

Definitions and Theorems

Function: svexlist-rewrite-top-fn

(defun svexlist-rewrite-top-fn (x verbosep)
 (declare (xargs :guard (svexlist-p x)))
 (let ((__function__ 'svexlist-rewrite-top))
  (declare (ignorable __function__))
  (b*
   (((mv masks toposort)
     (svexlist-mask-alist/toposort x))
    (multirefs (svexlist-multirefs-top x))
    (multiref-count (len multirefs))
    (-
     (and
        verbosep
        (cw "opcount before rewrite: ~x0 multiply-referenced: ~x1~%"
            (svexlist-count-calls toposort)
            multiref-count)))
    ((mv new-x out-multirefs memo)
     (mbe
      :logic
      (svexlist-rewrite x masks
                        multirefs multiref-count multiref-count)
      :exec
      (with-local-stobj
       acl2::nrev
       (mv-let
        (new-x out-multirefs memo acl2::nrev)
        (b*
         (((mv acl2::nrev out-multirefs memo)
           (cwtime
             (svexlist-rewrite-nrev x masks multirefs multiref-count
                                    multiref-count acl2::nrev)
             :mintime 1))
          ((mv new-x acl2::nrev)
           (acl2::nrev-finish acl2::nrev)))
         (mv new-x out-multirefs memo acl2::nrev))
        (mv new-x out-multirefs memo)))))
    (- (clear-memoize-table 'svex-rewrite)
       (fast-alist-free masks)
       (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-top

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

Theorem: svexlist-rewrite-top-fn-of-svexlist-fix-x

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

Theorem: svexlist-rewrite-top-fn-svexlist-equiv-congruence-on-x

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

Theorem: svexlist-rewrite-top-correct

(defthm svexlist-rewrite-top-correct
  (equal (svexlist-eval (svexlist-rewrite-top x
                                              :verbosep verbosep)
                        env)
         (svexlist-eval x env)))

Theorem: len-of-svexlist-rewrite-top

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

Theorem: vars-of-svexlist-rewrite-top

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