		Search-engine friendly clone of the ACL2 documentation.

Rewrite-config

Change-rewrite-config

Modifying constructor for rewrite-config structures.

Syntax

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

This is an often useful alternative to make-rewrite-config.

We construct a new rewrite-config structure that is a copy of x, except that you can explicitly change some particular fields. Any fields you don't mention just keep their values from x.

Definition

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

Macro: change-rewrite-config

(defmacro change-rewrite-config (x &rest args)
  (std::change-aggregate
       'rewrite-config
       x args
       '((:cuts4-config . rewrite-config->cuts4-config)
         (:cut-tries-limit . rewrite-config->cut-tries-limit)
         (:zero-cost-replace . rewrite-config->zero-cost-replace)
         (:evaluation-method . rewrite-config->evaluation-method)
         (:gatesimp . rewrite-config->gatesimp))
       'change-rewrite-config
       'nil))