		Search-engine friendly clone of the ACL2 documentation.

Rewrite-config

Make-rewrite-config

Basic constructor macro for rewrite-config structures.

Syntax

(make-rewrite-config [:cuts4-config <cuts4-config>] 
                     [:cut-tries-limit <cut-tries-limit>] 
                     [:zero-cost-replace <zero-cost-replace>] 
                     [:evaluation-method <evaluation-method>] 
                     [:gatesimp <gatesimp>])

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

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

Definition

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

Macro: make-rewrite-config

(defmacro make-rewrite-config (&rest args)
  (std::make-aggregate 'rewrite-config
                       args
                       '((:cuts4-config make-cuts4-config)
                         (:cut-tries-limit . 5)
                         (:zero-cost-replace)
                         (:evaluation-method . :nobuild)
                         (:gatesimp default-gatesimp))
                       'make-rewrite-config
                       nil))

Function: rewrite-config

(defun rewrite-config
       (cuts4-config cut-tries-limit zero-cost-replace
                     evaluation-method gatesimp)
 (declare
      (xargs :guard (and (cuts4-config-p cuts4-config)
                         (acl2::maybe-natp cut-tries-limit)
                         (booleanp zero-cost-replace)
                         (rewrite-eval-method-p evaluation-method)
                         (gatesimp-p gatesimp))))
 (declare (xargs :guard t))
 (let ((__function__ 'rewrite-config))
  (declare (ignorable __function__))
  (b* ((cuts4-config (mbe :logic (cuts4-config-fix cuts4-config)
                          :exec cuts4-config))
       (cut-tries-limit
            (mbe :logic (acl2::maybe-natp-fix cut-tries-limit)
                 :exec cut-tries-limit))
       (zero-cost-replace
            (mbe :logic (acl2::bool-fix zero-cost-replace)
                 :exec zero-cost-replace))
       (evaluation-method
            (mbe :logic (rewrite-eval-method-fix evaluation-method)
                 :exec evaluation-method))
       (gatesimp (mbe :logic (gatesimp-fix gatesimp)
                      :exec gatesimp)))
   (cons
       :rewrite-config (list (cons 'cuts4-config cuts4-config)
                             (cons 'cut-tries-limit cut-tries-limit)
                             (cons 'zero-cost-replace
                                   zero-cost-replace)
                             (cons 'evaluation-method
                                   evaluation-method)
                             (cons 'gatesimp gatesimp))))))