(svtv-inputs->assigns x phase) → assigns
Function:
(defun svtv-inputs->assigns (x phase) (declare (xargs :guard (and (svtv-lines-p x) (natp phase)))) (let ((__function__ 'svtv-inputs->assigns)) (declare (ignorable __function__)) (b* (((when (atom x)) nil) ((svtv-line xf) (car x)) (ent (or (nth phase xf.entries) '_)) ((when (svtv-dontcare-p ent)) (svtv-inputs->assigns (cdr x) phase)) ((unless (svtv-baseentry-p ent)) (er hard? 'svtv-inputs->assigns "SVTV entries such as ~x0 are only allowed in overrides." ent) (svtv-inputs->assigns (cdr x) phase)) (val (svtv-baseentry-svex ent))) (cons (cons xf.lhs (make-driver :value val :strength 10)) (svtv-inputs->assigns (cdr x) phase)))))
Theorem:
(defthm assigns-p-of-svtv-inputs->assigns (b* ((assigns (svtv-inputs->assigns x phase))) (assigns-p assigns)) :rule-classes :rewrite)
Theorem:
(defthm svtv-inputs->assigns-of-svtv-lines-fix-x (equal (svtv-inputs->assigns (svtv-lines-fix x) phase) (svtv-inputs->assigns x phase)))
Theorem:
(defthm svtv-inputs->assigns-svtv-lines-equiv-congruence-on-x (implies (svtv-lines-equiv x x-equiv) (equal (svtv-inputs->assigns x phase) (svtv-inputs->assigns x-equiv phase))) :rule-classes :congruence)
Theorem:
(defthm svtv-inputs->assigns-of-nfix-phase (equal (svtv-inputs->assigns x (nfix phase)) (svtv-inputs->assigns x phase)))
Theorem:
(defthm svtv-inputs->assigns-nat-equiv-congruence-on-phase (implies (nat-equiv phase phase-equiv) (equal (svtv-inputs->assigns x phase) (svtv-inputs->assigns x phase-equiv))) :rule-classes :congruence)