		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