		Search-engine friendly clone of the ACL2 documentation.

Rewriting

Svex-rewrite-top

Signature
(svex-rewrite-top x) → xx
Arguments: x — Guard (svex-p x).
Returns: xx — Type (svex-p xx).

Definitions and Theorems

Function: svex-rewrite-top

(defun svex-rewrite-top (x)
  (declare (xargs :guard (svex-p x)))
  (let ((__function__ 'svex-rewrite-top))
    (declare (ignorable __function__))
    (b* ((list (list x))
         (masks (svexlist-mask-alist list))
         (multirefs (svexlist-multirefs-top list))
         ((mv res out-multirefs memo)
          (svex-rewrite x masks multirefs nil nil)))
      (fast-alist-free out-multirefs)
      (fast-alist-free memo)
      (fast-alist-free masks)
      (fast-alist-free multirefs)
      res)))

Theorem: svex-p-of-svex-rewrite-top

(defthm svex-p-of-svex-rewrite-top
  (b* ((xx (svex-rewrite-top x)))
    (svex-p xx))
  :rule-classes :rewrite)

Theorem: svex-rewrite-top-of-svex-fix-x

(defthm svex-rewrite-top-of-svex-fix-x
  (equal (svex-rewrite-top (svex-fix x))
         (svex-rewrite-top x)))

Theorem: svex-rewrite-top-svex-equiv-congruence-on-x

(defthm svex-rewrite-top-svex-equiv-congruence-on-x
  (implies (svex-equiv x x-equiv)
           (equal (svex-rewrite-top x)
                  (svex-rewrite-top x-equiv)))
  :rule-classes :congruence)

Theorem: svex-rewrite-top-correct

(defthm svex-rewrite-top-correct
  (equal (svex-eval (svex-rewrite-top x) env)
         (svex-eval x env)))

Theorem: vars-of-svex-rewrite-top

(defthm vars-of-svex-rewrite-top
  (implies (not (member v (svex-vars x)))
           (not (member v (svex-vars (svex-rewrite-top x))))))