		Search-engine friendly clone of the ACL2 documentation.

Symbolic-test-vectors

Stv-widen

Widen the input/output/internals lines so that they all agree on how many phases there are.

Signature
(stv-widen stv) → widened-stv
Arguments: stv — Guard (stvdata-p stv).
Returns: widened-stv — Type (stvdata-p widened-stv), given the guard.

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.

Definitions and Theorems

Function: stv-widen

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

Theorem: stvdata-p-of-stv-widen

(defthm stvdata-p-of-stv-widen
        (implies (and (stvdata-p stv))
                 (b* ((widened-stv (stv-widen stv)))
                     (stvdata-p widened-stv)))
        :rule-classes :rewrite)

Subtopics

Stv-widen-lines: Rewrite lines of an STV, repeating the last entry in each line to extend it to the desired number of phases.