Apply onehot-rewriting to a sexpr alist.
(4v-onehot-rw-sexpr-alist vars sexpr-alist) is given:
We return a new, ordinary (slow) sexpr-alist which is a (possibly simpler)
conservative approximation of the original. The basic idea is to apply 4v-onehot-rw-sexpr to any sexprs that mention any of the
Function:
(defun 4v-onehot-rw-sexpr-alist (vars sexpr-alist) (declare (xargs :guard (and (atom-listp vars) (not (member-equal nil vars))))) (b* ((- (or (uniquep vars) (er hard? '4v-onehot-rw-sexpr-alist "You really want to use unique variables for onehot ~ rewriting. Duplicated variables are: ~&0.~%" (duplicated-members vars)))) (sexpr-alist (fast-alist-free (hons-shrink-alist sexpr-alist nil))) (vars-fal (make-fast-alist (pairlis$ vars nil))) ((mv relevant-part irrelevant-part) (4v-onehot-filter sexpr-alist vars-fal nil nil)) (- (fast-alist-free vars-fal)) (- (clear-memoize-table '4v-sexpr-mentions)) ((unless relevant-part) sexpr-alist)) (append (4v-onehot-rw-sexpr-alist-aux vars relevant-part) irrelevant-part)))
Theorem:
(defthm 4v-sexpr-alist-<=-of-4v-onehot-rw-sexpr-alist (implies (and (atom-listp vars) (not (member-equal nil vars))) (4v-sexpr-alist-<= (4v-onehot-rw-sexpr-alist vars sexpr-alist) sexpr-alist)))
Theorem:
(defthm alist-keys-of-4v-onehot-rw-sexpr-alist (set-equiv (alist-keys (4v-onehot-rw-sexpr-alist vars sexpr-alist)) (alist-keys sexpr-alist)))
Theorem:
(defthm 4v-sexpr-vars-of-4v-onehot-rw-sexpr-alist (let ((new-alist (4v-onehot-rw-sexpr-alist vars sexpr-alist))) (implies (atom-listp vars) (subsetp-equal (4v-sexpr-vars-list (alist-vals new-alist)) (append vars (4v-sexpr-vars-list (alist-vals sexpr-alist)))))))