		Search-engine friendly clone of the ACL2 documentation.

Glcp-config-p

Change-glcp-config

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

Syntax:

(change-glcp-config x 
                    [:abort-indeterminate <abort-indeterminate>] 
                    [:abort-ctrex <abort-ctrex>] 
                    [:exec-ctrex <exec-ctrex>] 
                    [:ctrex-transform <ctrex-transform>] 
                    [:abort-vacuous <abort-vacuous>] 
                    [:check-vacuous <check-vacuous>] 
                    [:n-counterexamples <n-counterexamples>] 
                    [:hyp-clk <hyp-clk>] 
                    [:concl-clk <concl-clk>] 
                    [:clause-proc <clause-proc>] 
                    [:overrides <overrides>] 
                    [:param-bfr <param-bfr>] 
                    [:term-level-counterexample-scheme <term-level-counterexample-scheme>] 
                    [:top-level-term <top-level-term>] 
                    [:shape-spec-alist <shape-spec-alist>] 
                    [:run-before-cases <run-before-cases>] 
                    [:run-after-cases <run-after-cases>] 
                    [:case-split-override <case-split-override>] 
                    [:split-conses <split-conses>] 
                    [:split-fncalls <split-fncalls>] 
                    [:lift-ifsp <lift-ifsp>] 
                    [:prof-enabledp <prof-enabledp>] 
                    [:rewrite-rule-table <rewrite-rule-table>] 
                    [:branch-merge-rules <branch-merge-rules>])

This is a sometimes useful alternative to make-glcp-config. It constructs a new glcp-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 std::defaggregate.

Macro: change-glcp-config

(defmacro change-glcp-config (x &rest args)
  (std::change-aggregate
       'glcp-config
       x args
       '((:abort-indeterminate . glcp-config->abort-indeterminate)
         (:abort-ctrex . glcp-config->abort-ctrex)
         (:exec-ctrex . glcp-config->exec-ctrex)
         (:ctrex-transform . glcp-config->ctrex-transform)
         (:abort-vacuous . glcp-config->abort-vacuous)
         (:check-vacuous . glcp-config->check-vacuous)
         (:n-counterexamples . glcp-config->n-counterexamples)
         (:hyp-clk . glcp-config->hyp-clk)
         (:concl-clk . glcp-config->concl-clk)
         (:clause-proc . glcp-config->clause-proc)
         (:overrides . glcp-config->overrides)
         (:param-bfr . glcp-config->param-bfr)
         (:term-level-counterexample-scheme
              .
              glcp-config->term-level-counterexample-scheme)
         (:top-level-term . glcp-config->top-level-term)
         (:shape-spec-alist . glcp-config->shape-spec-alist)
         (:run-before-cases . glcp-config->run-before-cases)
         (:run-after-cases . glcp-config->run-after-cases)
         (:case-split-override . glcp-config->case-split-override)
         (:split-conses . glcp-config->split-conses)
         (:split-fncalls . glcp-config->split-fncalls)
         (:lift-ifsp . glcp-config->lift-ifsp)
         (:prof-enabledp . glcp-config->prof-enabledp)
         (:rewrite-rule-table . glcp-config->rewrite-rule-table)
         (:branch-merge-rules . glcp-config->branch-merge-rules))
       'change-glcp-config
       'nil))