|
|
|---|
|
|
|
|---|
Raw constructor for honsed glcp-config-p structures.
Syntax:
(honsed-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 identical to glcp-config, except that we hons the structure we are creating.
This is an ordinary honsing constructor introduced by std::defaggregate.
Function:
(defun honsed-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)))) (mbe :logic (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) :exec (hons :glcp-config (hons (hons 'abort-indeterminate abort-indeterminate) (hons (hons 'abort-ctrex abort-ctrex) (hons (hons 'exec-ctrex exec-ctrex) (hons (hons 'ctrex-transform ctrex-transform) (hons (hons 'abort-vacuous abort-vacuous) (hons (hons 'check-vacuous check-vacuous) (hons (hons 'n-counterexamples n-counterexamples) (hons (hons 'hyp-clk hyp-clk) (hons (hons 'concl-clk concl-clk) (hons (hons 'clause-proc clause-proc) (hons (hons 'overrides overrides) (hons (hons 'param-bfr param-bfr) (hons (hons 'term-level-counterexample-scheme term-level-counterexample-scheme) (hons (hons 'top-level-term top-level-term) (hons (hons 'shape-spec-alist shape-spec-alist) (hons (hons 'run-before-cases run-before-cases) (hons (hons 'run-after-cases run-after-cases) (hons (hons 'case-split-override case-split-override) (hons (hons 'split-conses split-conses) (hons (hons 'split-fncalls split-fncalls) (hons (hons 'lift-ifsp lift-ifsp) (hons (hons 'prof-enabledp prof-enabledp) (hons (hons 'rewrite-rule-table rewrite-rule-table) (hons (hons 'branch-merge-rules branch-merge-rules) nil)))))))))))))))))))))))))))