		Search-engine friendly clone of the ACL2 documentation.

Symbolic-test-vectors

Stv-number-of-phases

Maximum length of any line of an STV (i.e., how many phases we are going to simulate.

Signature
(stv-number-of-phases stv) → num-phases
Arguments: stv — Guard (stvdata-p stv).
Returns: num-phases — Type (natp num-phases).

Definitions and Theorems

Function: stv-number-of-phases

(defun
 stv-number-of-phases (stv)
 (declare (xargs :guard (stvdata-p stv)))
 (let
    ((__function__ 'stv-number-of-phases))
    (declare (ignorable __function__))
    (b* (((stvdata stv) stv))
        (max (stv-max-phases-in-lines stv.inputs)
             (max (stv-max-phases-in-lines stv.outputs)
                  (max (stv-max-phases-in-lines stv.internals)
                       (stv-max-phases-in-lines stv.overrides)))))))

Theorem: natp-of-stv-number-of-phases

(defthm natp-of-stv-number-of-phases
        (b* ((num-phases (stv-number-of-phases stv)))
            (natp num-phases))
        :rule-classes :type-prescription)

Subtopics

Stv-max-phases-in-lines