Basic constructor macro for svex-scc-consts structures.
(make-svex-scc-consts [:final-masks <final-masks>] [:loop-vars <loop-vars>] [:compose-iter-limit <compose-iter-limit>] [:updates <updates>])
This is the usual way to construct svex-scc-consts structures. It simply conses together a structure with the specified fields.
This macro generates a new svex-scc-consts structure from scratch. See also change-svex-scc-consts, which can "change" an existing structure, instead.
This is an ordinary
Macro:
(defmacro make-svex-scc-consts (&rest args) (std::make-aggregate 'svex-scc-consts args '((:final-masks) (:loop-vars) (:compose-iter-limit) (:updates)) 'make-svex-scc-consts nil))
Function:
(defun svex-scc-consts (final-masks loop-vars compose-iter-limit updates) (declare (xargs :guard (and (svex-mask-alist-p final-masks) (svar-key-alist-p loop-vars) (maybe-natp compose-iter-limit) (svex-alist-p updates)))) (declare (xargs :guard t)) (let ((__function__ 'svex-scc-consts)) (declare (ignorable __function__)) (b* ((final-masks (mbe :logic (svex-mask-alist-fix final-masks) :exec final-masks)) (loop-vars (mbe :logic (svar-key-alist-fix loop-vars) :exec loop-vars)) (compose-iter-limit (mbe :logic (acl2::maybe-natp-fix compose-iter-limit) :exec compose-iter-limit)) (updates (mbe :logic (svex-alist-fix updates) :exec updates))) (std::prod-cons (std::prod-cons final-masks loop-vars) (std::prod-cons compose-iter-limit updates)))))