Convert the bit-level bindings from after 4v-sexpr-eval into user-level bindings of the output simulation variables to naturals or X.
(stv-assemble-output-alist bit-out-alist out-usersyms) → *
We recur down
Function:
(defun stv-assemble-output-alist (bit-out-alist out-usersyms) (declare (xargs :guard t)) (let ((__function__ 'stv-assemble-output-alist)) (declare (ignorable __function__)) (b* (((when (atom out-usersyms)) nil) (rest (stv-assemble-output-alist bit-out-alist (cdr out-usersyms))) ((when (atom (car out-usersyms))) (raise "out-usersyms should be an alist.") rest) ((cons user-name bits) (car out-usersyms)) (vals (vl2014::look-up-each-fast bits bit-out-alist)) (true-val (4v-to-nat vals)) (- (and (eq true-val 'x) (cw "Bits bound to X in ~x0: ~x1~%" user-name (collect-bits-bound-to-x bits bit-out-alist))))) (cons (cons user-name true-val) rest))))