		Search-engine friendly clone of the ACL2 documentation.

Process.lisp

Svtv-phase-inputs

Signature
(svtv-phase-inputs phase ins overrides invars) → inalist
Arguments: phase — Guard (natp phase).; ins — Guard (svtv-lines-p ins).; overrides — Guard (svtv-overridelines-p overrides).; invars — Guard (svarlist-p invars).
Returns: inalist — Type (svex-alist-p inalist).

Definitions and Theorems

Function: svtv-phase-inputs

(defun svtv-phase-inputs (phase ins overrides invars)
 (declare (xargs :guard (and (natp phase)
                             (svtv-lines-p ins)
                             (svtv-overridelines-p overrides)
                             (svarlist-p invars))))
 (let ((__function__ 'svtv-phase-inputs))
  (declare (ignorable __function__))
  (b*
   ((in-assigns (svtv-inputs->assigns ins phase))
    (ov-assigns (svtv-overrides->assigns overrides phase))
    (netassigns (assigns->segment-drivers in-assigns))
    (inalist (segment-driver-map-resolve netassigns))
    ((mv masks conflicts)
     (assigns-check-masks in-assigns nil nil))
    (- (and (consp conflicts)
            (raise "Conflicting assignments. Masks: ~x0~%"
                   (fast-alist-free (fast-alist-clean conflicts)))))
    (- (fast-alist-free conflicts))
    (final-ins
         (svtv-inalist-resolve-unassigned inalist masks phase))
    (- (fast-alist-free masks)))
   (append ov-assigns final-ins
           (svtv-phase-var-assigns invars phase)))))

Theorem: svex-alist-p-of-svtv-phase-inputs

(defthm svex-alist-p-of-svtv-phase-inputs
  (b* ((inalist (svtv-phase-inputs phase ins overrides invars)))
    (svex-alist-p inalist))
  :rule-classes :rewrite)

Theorem: svtv-phase-inputs-of-nfix-phase

(defthm svtv-phase-inputs-of-nfix-phase
  (equal (svtv-phase-inputs (nfix phase)
                            ins overrides invars)
         (svtv-phase-inputs phase ins overrides invars)))

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

(defthm svtv-phase-inputs-nat-equiv-congruence-on-phase
  (implies
       (nat-equiv phase phase-equiv)
       (equal (svtv-phase-inputs phase ins overrides invars)
              (svtv-phase-inputs phase-equiv ins overrides invars)))
  :rule-classes :congruence)

Theorem: svtv-phase-inputs-of-svtv-lines-fix-ins

(defthm svtv-phase-inputs-of-svtv-lines-fix-ins
  (equal (svtv-phase-inputs phase (svtv-lines-fix ins)
                            overrides invars)
         (svtv-phase-inputs phase ins overrides invars)))

Theorem: svtv-phase-inputs-svtv-lines-equiv-congruence-on-ins

(defthm svtv-phase-inputs-svtv-lines-equiv-congruence-on-ins
  (implies
       (svtv-lines-equiv ins ins-equiv)
       (equal (svtv-phase-inputs phase ins overrides invars)
              (svtv-phase-inputs phase ins-equiv overrides invars)))
  :rule-classes :congruence)

Theorem: svtv-phase-inputs-of-svtv-overridelines-fix-overrides

(defthm svtv-phase-inputs-of-svtv-overridelines-fix-overrides
  (equal (svtv-phase-inputs phase
                            ins (svtv-overridelines-fix overrides)
                            invars)
         (svtv-phase-inputs phase ins overrides invars)))

Theorem: svtv-phase-inputs-svtv-overridelines-equiv-congruence-on-overrides

(defthm
 svtv-phase-inputs-svtv-overridelines-equiv-congruence-on-overrides
 (implies
      (svtv-overridelines-equiv overrides overrides-equiv)
      (equal (svtv-phase-inputs phase ins overrides invars)
             (svtv-phase-inputs phase ins overrides-equiv invars)))
 :rule-classes :congruence)

Theorem: svtv-phase-inputs-of-svarlist-fix-invars

(defthm svtv-phase-inputs-of-svarlist-fix-invars
  (equal (svtv-phase-inputs phase
                            ins overrides (svarlist-fix invars))
         (svtv-phase-inputs phase ins overrides invars)))

Theorem: svtv-phase-inputs-svarlist-equiv-congruence-on-invars

(defthm svtv-phase-inputs-svarlist-equiv-congruence-on-invars
  (implies
       (svarlist-equiv invars invars-equiv)
       (equal (svtv-phase-inputs phase ins overrides invars)
              (svtv-phase-inputs phase ins overrides invars-equiv)))
  :rule-classes :congruence)