		Search-engine friendly clone of the ACL2 documentation.

Incremental-extremize-config-p

Change-incremental-extremize-config

A copying macro that lets you create new incremental-extremize-config-p structures, based on existing structures.

Syntax:

(change-incremental-extremize-config x 
                                     [:numerator <numerator>] 
                                     [:denominator <denominator>] 
                                     [:direction <direction>] 
                                     [:sat-config <sat-config>] 
                                     [:obj <obj>] 
                                     [:progress-term <progress-term>] 
                                     [:final-term <final-term>] 
                                     [:unsat-term <unsat-term>] 
                                     [:sat-term <sat-term>] 
                                     [:error-term <error-term>] 
                                     [:bad-ctrex-term <bad-ctrex-term>] 
                                     [:interpolate-factor <interpolate-factor>])

This is a sometimes useful alternative to make-incremental-extremize-config. It constructs a new incremental-extremize-config-p 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 defaggregate.

Macro: change-incremental-extremize-config

(defmacro change-incremental-extremize-config (x &rest args)
 (std::change-aggregate
    'incremental-extremize-config
    x args
    '((:numerator .
                  incremental-extremize-config->numerator)
      (:denominator .
                    incremental-extremize-config->denominator)
      (:direction .
                  incremental-extremize-config->direction)
      (:sat-config .
                   incremental-extremize-config->sat-config)
      (:obj . incremental-extremize-config->obj)
      (:progress-term .
                      incremental-extremize-config->progress-term)
      (:final-term .
                   incremental-extremize-config->final-term)
      (:unsat-term .
                   incremental-extremize-config->unsat-term)
      (:sat-term .
                 incremental-extremize-config->sat-term)
      (:error-term .
                   incremental-extremize-config->error-term)
      (:bad-ctrex-term .
                       incremental-extremize-config->bad-ctrex-term)
      (:interpolate-factor
           .
           incremental-extremize-config->interpolate-factor))
    'change-incremental-extremize-config
    'nil))