		Search-engine friendly clone of the ACL2 documentation.

Svtv-cyclephase

Make-svtv-cyclephase

Basic constructor macro for svtv-cyclephase structures.

Syntax

(make-svtv-cyclephase [:constants <constants>] 
                      [:inputs-free <inputs-free>] 
                      [:outputs-captured <outputs-captured>])

This is the usual way to construct svtv-cyclephase structures. It simply conses together a structure with the specified fields.

This macro generates a new svtv-cyclephase structure from scratch. See also change-svtv-cyclephase, which can "change" an existing structure, instead.

Definition

This is an ordinary make- macro introduced by defprod.

Macro: make-svtv-cyclephase

(defmacro make-svtv-cyclephase (&rest args)
  (std::make-aggregate 'svtv-cyclephase
                       args
                       '((:constants)
                         (:inputs-free)
                         (:outputs-captured))
                       'make-svtv-cyclephase
                       nil))

Function: svtv-cyclephase

(defun svtv-cyclephase (constants inputs-free outputs-captured)
  (declare (xargs :guard (and (svex-env-p constants)
                              (booleanp inputs-free)
                              (booleanp outputs-captured))))
  (declare (xargs :guard t))
  (let ((__function__ 'svtv-cyclephase))
    (declare (ignorable __function__))
    (b* ((constants (mbe :logic (svex-env-fix constants)
                         :exec constants))
         (inputs-free (mbe :logic (bool-fix inputs-free)
                           :exec inputs-free))
         (outputs-captured (mbe :logic (bool-fix outputs-captured)
                                :exec outputs-captured)))
      (cons constants
            (cons inputs-free outputs-captured)))))