		Search-engine friendly clone of the ACL2 documentation.

Process.lisp

Svtv-inputs->assigns

Signature
(svtv-inputs->assigns x phase) → assigns
Arguments: x — Guard (svtv-lines-p x).; phase — Guard (natp phase).
Returns: assigns — Type (assigns-p assigns).

Definitions and Theorems

Function: svtv-inputs->assigns

(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: assigns-p-of-svtv-inputs->assigns

(defthm assigns-p-of-svtv-inputs->assigns
  (b* ((assigns (svtv-inputs->assigns x phase)))
    (assigns-p assigns))
  :rule-classes :rewrite)

Theorem: svtv-inputs->assigns-of-svtv-lines-fix-x

(defthm svtv-inputs->assigns-of-svtv-lines-fix-x
  (equal (svtv-inputs->assigns (svtv-lines-fix x)
                               phase)
         (svtv-inputs->assigns x phase)))

Theorem: svtv-inputs->assigns-svtv-lines-equiv-congruence-on-x

(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: svtv-inputs->assigns-of-nfix-phase

(defthm svtv-inputs->assigns-of-nfix-phase
  (equal (svtv-inputs->assigns x (nfix phase))
         (svtv-inputs->assigns x phase)))

Theorem: svtv-inputs->assigns-nat-equiv-congruence-on-phase

(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)