# Onehot-rewriting

Conservatively rewrite 4v-sexprs by assuming some variables
are one-hot.

### Introduction

Sometimes you know that certain inputs to a module are supposed to be
one-hot. Using this information, it may be possible to simplify the sexprs
produced during esim runs. For example, if we know that the variables
A1 and A2 are one-hot, we might like to rewrite a sexpr like:

(ITE A1 (AND A2 FOO) BAR)

Here, we can "see" that A2 has to be false in the true-branch since
to get there we must have that A1 is true. Accordingly, we would like to
replace the sexpr with something like:

(AND (NOT A1) BAR)

This sort of rewriting may occasionally help to avoid combinational loops
that are only broken when the inputs are truly one-hot, e.g., notice how the
variable FOO has dropped out of the expression above.

### The Basic Transformation

Our main function for onehot rewriting is 4v-onehot-rw-sexpr. Given
a list of variables A1...AN that we think are one-hot, and an s-expression
SEXPR to rewrite, it basically constructs:

(ITE* ONEHOT-P SEXPR' (X))

Where:

- ONEHOT-P is constructed by 4vs-onehot and evaluates to
T when the A1...N are one-hot, and
- SEXPR' is formed
from SEXPR by assuming A1...N are indeed one-hot; see 4v-onehot-sexpr-prime for details.

We prove this conservatively approximates SEXPR, but keep in mind that
this approximation is **not an equivalent** term! For instance, the
rewritten expression will always produce X if it turns out that the inputs
were not really one-hot. Accordingly, you should only use this rewrite when
you are really are certain the variables will be one-hot.

### The Alist Transformation

Our main use for onehot rewriting is in simplifiers for esim-simplify-update-fns, where the goal is to rewrite a whole alist binding
names to sexprs.

Our main function for this is 4v-onehot-rw-sexpr-alist, which
takes the list of one-hot variables and the alist to rewrite as arguments.
This function is reasonably clever: it avoids changing sexprs that don't
mention any of the onehot variables, and it has some other performance
optimizations that are geared toward reusing memoized results across
sexprs.

### Subtopics

- 4v-onehot-sexpr-list-prime
- Efficiently reduce a list of sexprs under the assumption that some
variables are one-hot.
- 4v-onehot-sexpr-prime
`(4v-onehot-sexpr-prime vars sexpr)` rewrites sexpr under the
assumption that vars are one-hot.- 4v-onehot-rw-sexpr-alist-aux
- Apply one-hot rewriting to a sexpr-alist.
- 4v-onehot-rw-sexpr-alist
- Apply onehot-rewriting to a sexpr alist.
- 4v-onehot-rw-sexpr
- Apply onehot-rewriting to a single s-expression.
- 4vs-onehot
`(4vs-onehot sexprs)` constructs an s-expression that is T when the
members of X are one-hot.- 4vs-ite*-list-dumb
`(4vs-ite*-list-dumb c as bs)` produces a list of sexprs, basically
(4V-ITE* C Ai Bi) for the corresponding elements of AS and BS.- 4v-onehot-filter
- Filter a sexpr-alist to avoid unnecessary onehot-rewriting.
- 4v-onehot-list-p
`(4v-onehot-list-p x)` determines if a list of 4vps has
exactly one member that is T while the rest are F.