Basic constructor macro for phase-fsm-params structures.
(make-phase-fsm-params [:scc-selfcompose-limit <scc-selfcompose-limit>] [:rewrite <rewrite>])
This is the usual way to construct phase-fsm-params structures. It simply conses together a structure with the specified fields.
This macro generates a new phase-fsm-params structure from scratch. See also change-phase-fsm-params, which can "change" an existing structure, instead.
This is an ordinary
Macro:
(defmacro make-phase-fsm-params (&rest args) (std::make-aggregate 'phase-fsm-params args '((:scc-selfcompose-limit) (:rewrite . t)) 'make-phase-fsm-params nil))
Function:
(defun phase-fsm-params (scc-selfcompose-limit rewrite) (declare (xargs :guard (and (maybe-natp scc-selfcompose-limit) (booleanp rewrite)))) (declare (xargs :guard t)) (let ((__function__ 'phase-fsm-params)) (declare (ignorable __function__)) (b* ((scc-selfcompose-limit (mbe :logic (acl2::maybe-natp-fix scc-selfcompose-limit) :exec scc-selfcompose-limit)) (rewrite (mbe :logic (bool-fix rewrite) :exec rewrite))) (list (cons 'scc-selfcompose-limit scc-selfcompose-limit) (cons 'rewrite rewrite)))))