		Search-engine friendly clone of the ACL2 documentation.

Constprop-config

Make-constprop-config

Basic constructor macro for constprop-config structures.

Syntax

(make-constprop-config [:gatesimp <gatesimp>] 
                       [:iterations <iterations>])

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

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

Definition

This is an ordinary make- macro introduced by fty::defprod.

Macro: make-constprop-config

(defmacro make-constprop-config (&rest args)
  (std::make-aggregate 'constprop-config
                       args
                       '((:gatesimp default-gatesimp)
                         (:iterations . 1))
                       'make-constprop-config
                       nil))

Function: constprop-config

(defun constprop-config (gatesimp iterations)
 (declare (xargs :guard (and (gatesimp-p gatesimp)
                             (posp iterations))))
 (declare (xargs :guard t))
 (let ((__function__ 'constprop-config))
  (declare (ignorable __function__))
  (b* ((gatesimp (mbe :logic (gatesimp-fix gatesimp)
                      :exec gatesimp))
       (iterations (mbe :logic (pos-fix iterations)
                        :exec iterations)))
    (cons :constprop-config (list (cons 'gatesimp gatesimp)
                                  (cons 'iterations iterations))))))