		Search-engine friendly clone of the ACL2 documentation.

Onehot-rewriting

4v-onehot-rw-sexpr-alist-aux

Apply one-hot rewriting to a sexpr-alist.

Logically this just walks over the alist and applies 4v-onehot-rw-sexpr to each value. But we actually use mbe to provide a more efficient implementation; see 4v-onehot-sexpr-list-prime for the basic idea and motivation.

This is only an -aux function because it applies the onehot rewrite to every sexpr in the alist. Our main function, 4v-onehot-rw-sexpr-alist, first filters the alist to avoid rewriting sexprs that don't mention any of the variables we are assuming to be one-hot.

Definitions and Theorems

Function: 4v-onehot-rw-sexpr-alist-fast

(defun 4v-onehot-rw-sexpr-alist-fast (vars sexpr-alist)
 (declare (xargs :guard (and (atom-listp vars)
                             (not (member-equal nil vars)))))
 (let*
  ((names (alist-keys sexpr-alist))
   (sexprs (alist-vals sexpr-alist))
   (new-sexprs
        (4vs-ite*-list-dumb (4vs-onehot vars)
                            (4v-onehot-sexpr-list-prime vars sexprs)
                            (replicate (len sexprs) (4vs-x)))))
  (pairlis$ names new-sexprs)))

Function: 4v-onehot-rw-sexpr-alist-aux

(defun 4v-onehot-rw-sexpr-alist-aux (vars sexpr-alist)
 (declare (xargs :guard (and (atom-listp vars)
                             (not (member-equal nil vars)))))
 (mbe
  :logic
  (cond
   ((atom sexpr-alist) nil)
   ((atom (car sexpr-alist))
    (4v-onehot-rw-sexpr-alist-aux vars (cdr sexpr-alist)))
   (t (cons (cons (caar sexpr-alist)
                  (4v-onehot-rw-sexpr vars (cdar sexpr-alist)))
            (4v-onehot-rw-sexpr-alist-aux vars (cdr sexpr-alist)))))
  :exec (4v-onehot-rw-sexpr-alist-fast vars sexpr-alist)))

Theorem: 4v-onehot-rw-sexpr-alist-fast-removal

(defthm 4v-onehot-rw-sexpr-alist-fast-removal
  (equal (4v-onehot-rw-sexpr-alist-fast vars sexpr-alist)
         (4v-onehot-rw-sexpr-alist-aux vars sexpr-alist)))

Theorem: hons-assoc-equal-of-4v-onehot-rw-sexpr-alist-aux

(defthm hons-assoc-equal-of-4v-onehot-rw-sexpr-alist-aux
 (equal
  (hons-assoc-equal name
                    (4v-onehot-rw-sexpr-alist-aux vars sexpr-alist))
  (if
   (hons-assoc-equal name sexpr-alist)
   (cons
     name
     (4v-onehot-rw-sexpr vars
                         (cdr (hons-assoc-equal name sexpr-alist))))
   nil)))

Theorem: 4v-sexpr-alist-<=-of-4v-onehot-rw-sexpr-alist-aux

(defthm 4v-sexpr-alist-<=-of-4v-onehot-rw-sexpr-alist-aux
 (implies
  (and (atom-listp vars)
       (not (member-equal nil vars)))
  (4v-sexpr-alist-<= (4v-onehot-rw-sexpr-alist-aux vars sexpr-alist)
                     sexpr-alist)))

Theorem: 4v-sexpr-vars-list-of-4v-onehot-rw-sexpr-alist-aux

(defthm 4v-sexpr-vars-list-of-4v-onehot-rw-sexpr-alist-aux
 (implies
  (atom-listp vars)
  (subsetp-equal
   (4v-sexpr-vars-list
       (alist-vals (4v-onehot-rw-sexpr-alist-aux vars sexpr-alist)))
   (append vars
           (4v-sexpr-vars-list (alist-vals sexpr-alist))))))