Efficiently reduce a list of sexprs under the assumption that some variables are one-hot.
Logically, this function does nothing more than compute 4v-onehot-sexpr-prime for each sexpr in a list.
With mbe we do something tricky for better performance. The real function we execute is basically a wide version of 4v-onehot-sexpr-prime's auxilliary function.
What is this performance hack all about? Our main goal in onehot rewriting
is to simplify the update functions of modules that have one-hot inputs. In
this context, we have some particular set of variables that we think are
one-hot, say
We want to apply our onehot rewrite on on each of these expressions. The simplest thing to do would be to call 4v-onehot-rw-sexpr on each expression and just cons together the results, as in the logical definition. But if we do this, then we are likely going to miss out on many opportunities to reuse memoized results.
Why? The problem is that each sexpr needs to be restrict/rewritten with a number of alists. Recall that we effectively replace each sexpr with:
(ITE* A1 SEXPR|_{A1=T,A2=NIL,A3=NIL,...AN=NIL) (ITE* A2 SEXPR|_{A1=NIL,A2=T,A3=NIL,...AN=NIL} ... (ITE* AN SEXPR|_{A1=NIL,A2=NIL,A3=NIL,...,AN=T} (X)) ...))
But these alists only depend on the variables
Function:
(defun 4v-onehot-sexpr-list-prime-exec (vars false-bindings sexprs) "Returns SEXPRS'" (declare (xargs :guard t)) (b* (((when (atom vars)) (fast-alist-free false-bindings) (replicate (len sexprs) (4vs-x))) (var (car vars)) (bindings (hons-acons var (4vs-t) false-bindings)) (sexprs/bindings (4v-sexpr-restrict-with-rw-list sexprs bindings)) (- (clear-memoize-table '4v-sexpr-restrict-with-rw)) (false-bindings (hons-acons var (4vs-f) bindings))) (4vs-ite*-list-dumb (car vars) sexprs/bindings (4v-onehot-sexpr-list-prime-exec (cdr vars) false-bindings sexprs))))
Theorem:
(defthm alist-equiv-implies-equal-4v-onehot-sexpr-list-prime-exec-2 (implies (alist-equiv false-bindings false-bindings-equiv) (equal (4v-onehot-sexpr-list-prime-exec vars false-bindings sexprs) (4v-onehot-sexpr-list-prime-exec vars false-bindings-equiv sexprs))) :rule-classes (:congruence))
Theorem:
(defthm len-of-4v-onehot-sexpr-list-prime-exec (equal (len (4v-onehot-sexpr-list-prime-exec vars false-bindings sexprs)) (len sexprs)))
Function:
(defun 4v-onehot-sexpr-list-prime-aux (vars false-bindings sexprs) (declare (xargs :guard t)) (mbe :logic (if (atom sexprs) nil (cons (4v-onehot-sexpr-prime-aux vars false-bindings (car sexprs)) (4v-onehot-sexpr-list-prime-aux vars false-bindings (cdr sexprs)))) :exec (4v-onehot-sexpr-list-prime-exec vars false-bindings sexprs)))
Theorem:
(defthm 4v-onehot-sexpr-list-prime-exec-removal (equal (4v-onehot-sexpr-list-prime-exec vars false-bindings sexprs) (4v-onehot-sexpr-list-prime-aux vars false-bindings sexprs)))
Function:
(defun 4v-onehot-sexpr-list-prime (vars sexprs) (declare (xargs :guard (and (atom-listp vars) (not (member-equal nil vars))))) (mbe :logic (if (atom sexprs) nil (cons (4v-onehot-sexpr-prime vars (car sexprs)) (4v-onehot-sexpr-list-prime vars (cdr sexprs)))) :exec (4v-onehot-sexpr-list-prime-aux vars (make-fast-alist (4v-onehot-false-bindings vars)) sexprs)))
Theorem:
(defthm 4v-onehot-sexpr-list-prime-of-take (implies (<= (nfix n) (len x)) (equal (4v-onehot-sexpr-list-prime vars (take n x)) (take n (4v-onehot-sexpr-list-prime vars x)))) :rule-classes ((:rewrite)))
Theorem:
(defthm set-equiv-congruence-over-4v-onehot-sexpr-list-prime (implies (set-equiv x y) (set-equiv (4v-onehot-sexpr-list-prime vars x) (4v-onehot-sexpr-list-prime vars y))) :rule-classes ((:congruence)))
Theorem:
(defthm subsetp-of-4v-onehot-sexpr-list-prime-when-subsetp (implies (subsetp x y) (subsetp (4v-onehot-sexpr-list-prime vars x) (4v-onehot-sexpr-list-prime vars y))) :rule-classes ((:rewrite)))
Theorem:
(defthm member-of-4v-onehot-sexpr-prime-in-4v-onehot-sexpr-list-prime (implies (member k x) (member (4v-onehot-sexpr-prime vars k) (4v-onehot-sexpr-list-prime vars x))) :rule-classes ((:rewrite)))
Theorem:
(defthm 4v-onehot-sexpr-list-prime-of-rev (equal (4v-onehot-sexpr-list-prime vars (rev x)) (rev (4v-onehot-sexpr-list-prime vars x))) :rule-classes ((:rewrite)))
Theorem:
(defthm 4v-onehot-sexpr-list-prime-of-list-fix (equal (4v-onehot-sexpr-list-prime vars (list-fix x)) (4v-onehot-sexpr-list-prime vars x)) :rule-classes ((:rewrite)))
Theorem:
(defthm 4v-onehot-sexpr-list-prime-of-append (equal (4v-onehot-sexpr-list-prime vars (append a b)) (append (4v-onehot-sexpr-list-prime vars a) (4v-onehot-sexpr-list-prime vars b))) :rule-classes ((:rewrite)))
Theorem:
(defthm cdr-of-4v-onehot-sexpr-list-prime (equal (cdr (4v-onehot-sexpr-list-prime vars x)) (4v-onehot-sexpr-list-prime vars (cdr x))) :rule-classes ((:rewrite)))
Theorem:
(defthm car-of-4v-onehot-sexpr-list-prime (equal (car (4v-onehot-sexpr-list-prime vars x)) (and (consp x) (4v-onehot-sexpr-prime vars (car x)))) :rule-classes ((:rewrite)))
Theorem:
(defthm 4v-onehot-sexpr-list-prime-under-iff (iff (4v-onehot-sexpr-list-prime vars x) (consp x)) :rule-classes ((:rewrite)))
Theorem:
(defthm consp-of-4v-onehot-sexpr-list-prime (equal (consp (4v-onehot-sexpr-list-prime vars x)) (consp x)) :rule-classes ((:rewrite)))
Theorem:
(defthm len-of-4v-onehot-sexpr-list-prime (equal (len (4v-onehot-sexpr-list-prime vars x)) (len x)) :rule-classes ((:rewrite)))
Theorem:
(defthm true-listp-of-4v-onehot-sexpr-list-prime (true-listp (4v-onehot-sexpr-list-prime vars x)) :rule-classes :type-prescription)
Theorem:
(defthm 4v-onehot-sexpr-list-prime-when-not-consp (implies (not (consp x)) (equal (4v-onehot-sexpr-list-prime vars x) nil)) :rule-classes ((:rewrite)))
Theorem:
(defthm 4v-onehot-sexpr-list-prime-of-cons (equal (4v-onehot-sexpr-list-prime vars (cons a b)) (cons (4v-onehot-sexpr-prime vars a) (4v-onehot-sexpr-list-prime vars b))) :rule-classes ((:rewrite)))
Theorem:
(defthm 4v-sexpr-vars-list-of-4v-onehot-sexpr-list-prime (implies (atom-listp vars) (subsetp-equal (4v-sexpr-vars-list (4v-onehot-sexpr-list-prime vars sexprs)) (append vars (4v-sexpr-vars-list sexprs)))))