		Search-engine friendly clone of the ACL2 documentation.

Glcp-config-p

Make-glcp-config

Constructor macro for glcp-config-p structures.

Syntax:

(make-glcp-config [: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 our preferred way to construct glcp-config-p structures. It simply conses together a structure with the specified fields.

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

The glcp-config-p structures we create here are just constructed with ordinary cons. If you want to create honsed structures, see make-honsed-glcp-config instead.

Definition

This is an ordinary make- macro introduced by std::defaggregate.

Macro: make-glcp-config

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