|
|
|---|
|
|
|
|---|
Raw constructor for glcp-config-p structures.
Syntax:
(glcp-config abort-indeterminate
abort-ctrex exec-ctrex ctrex-transform
abort-vacuous check-vacuous
n-counterexamples hyp-clk concl-clk
clause-proc overrides param-bfr
term-level-counterexample-scheme
top-level-term shape-spec-alist
run-before-cases run-after-cases
case-split-override split-conses
split-fncalls lift-ifsp prof-enabledp
rewrite-rule-table branch-merge-rules)This is the lowest-level constructor for glcp-config-p structures. It simply conses together a structure with the specified fields.
Note: It's generally better to use macros like make-glcp-config or change-glcp-config instead. These macros lead to more readable and robust code, because you don't have to remember the order of the fields.
The glcp-config-p structures we create here are just constructed with ordinary cons. If you want to create honsed structures, see honsed-glcp-config instead.
This is an ordinary constructor function introduced by std::defaggregate.
Function:
(defun glcp-config (abort-indeterminate abort-ctrex exec-ctrex ctrex-transform abort-vacuous check-vacuous n-counterexamples hyp-clk concl-clk clause-proc overrides param-bfr term-level-counterexample-scheme top-level-term shape-spec-alist run-before-cases run-after-cases case-split-override split-conses split-fncalls lift-ifsp prof-enabledp rewrite-rule-table branch-merge-rules) (declare (xargs :guard (and (booleanp abort-indeterminate) (booleanp abort-ctrex) (booleanp exec-ctrex) (booleanp abort-vacuous) (booleanp check-vacuous) (natp n-counterexamples) (posp hyp-clk) (posp concl-clk) (symbolp clause-proc) (symbolp term-level-counterexample-scheme) (shape-spec-bindingsp shape-spec-alist) (booleanp split-conses) (booleanp split-fncalls) (booleanp lift-ifsp) (booleanp prof-enabledp)))) (cons :glcp-config (cons (cons 'abort-indeterminate abort-indeterminate) (cons (cons 'abort-ctrex abort-ctrex) (cons (cons 'exec-ctrex exec-ctrex) (cons (cons 'ctrex-transform ctrex-transform) (cons (cons 'abort-vacuous abort-vacuous) (cons (cons 'check-vacuous check-vacuous) (cons (cons 'n-counterexamples n-counterexamples) (cons (cons 'hyp-clk hyp-clk) (cons (cons 'concl-clk concl-clk) (cons (cons 'clause-proc clause-proc) (cons (cons 'overrides overrides) (cons (cons 'param-bfr param-bfr) (cons (cons 'term-level-counterexample-scheme term-level-counterexample-scheme) (cons (cons 'top-level-term top-level-term) (cons (cons 'shape-spec-alist shape-spec-alist) (cons (cons 'run-before-cases run-before-cases) (cons (cons 'run-after-cases run-after-cases) (cons (cons 'case-split-override case-split-override) (cons (cons 'split-conses split-conses) (cons (cons 'split-fncalls split-fncalls) (cons (cons 'lift-ifsp lift-ifsp) (cons (cons 'prof-enabledp prof-enabledp) (cons (cons 'rewrite-rule-table rewrite-rule-table) (cons (cons 'branch-merge-rules branch-merge-rules) nil))))))))))))))))))))))))))