Widen the input/output/internals lines so that they all agree on how many phases there are.
This is an STV preprocessing step which can be run before or after stv-expand. We generally expect that all the lines have been widened before any compilation is performed.
(defun stv-widen (stv) (declare (xargs :guard (stvdata-p stv))) (let ((__function__ 'stv-widen)) (declare (ignorable __function__)) (b* (((stvdata stv) stv) (number-of-phases (stv-number-of-phases stv)) (new-inputs (stv-widen-lines stv.inputs number-of-phases nil)) (new-outputs (stv-widen-lines stv.outputs number-of-phases t)) (new-internals (stv-widen-lines stv.internals number-of-phases t)) (new-overrides (stv-widen-lines stv.overrides number-of-phases t))) (change-stvdata stv :inputs new-inputs :outputs new-outputs :internals new-internals :overrides new-overrides))))
(defthm stvdata-p-of-stv-widen (implies (and (stvdata-p stv)) (b* ((widened-stv (stv-widen stv))) (stvdata-p widened-stv))) :rule-classes :rewrite)