|
|
|---|
|
|
|
|---|
Raw constructor for honsed glmc-config-p structures.
Syntax:
(honsed-glmc-config glcp-config st-var in-vars
frame-ins rest-ins end-ins frame-in-vars
in-measure run st-hyp in-hyp bindings
bound-vars initstp nextst constr prop
st-hyp-method hints main-rewrite-rules
main-branch-merge-rules
extract-rewrite-rules
extract-branch-merge-rules)This is identical to glmc-config, except that we hons the structure we are creating.
This is an ordinary honsing constructor introduced by std::defaggregate.
Function:
(defun honsed-glmc-config (glcp-config st-var in-vars frame-ins rest-ins end-ins frame-in-vars in-measure run st-hyp in-hyp bindings bound-vars initstp nextst constr prop st-hyp-method hints main-rewrite-rules main-branch-merge-rules extract-rewrite-rules extract-branch-merge-rules) (declare (xargs :guard (and (glcp-config-p glcp-config) (variablep st-var) (variable-listp in-vars) (pseudo-term-listp frame-ins) (pseudo-term-listp rest-ins) (pseudo-termp end-ins) (variable-listp frame-in-vars) (pseudo-termp in-measure) (pseudo-termp run) (pseudo-termp st-hyp) (pseudo-termp in-hyp) (acl2::bindinglist-p bindings) (symbol-listp bound-vars) (pseudo-termp initstp) (pseudo-termp nextst) (pseudo-termp constr) (pseudo-termp prop) (st-hyp-method-p st-hyp-method)))) (mbe :logic (glmc-config glcp-config st-var in-vars frame-ins rest-ins end-ins frame-in-vars in-measure run st-hyp in-hyp bindings bound-vars initstp nextst constr prop st-hyp-method hints main-rewrite-rules main-branch-merge-rules extract-rewrite-rules extract-branch-merge-rules) :exec (hons (hons 'glcp-config glcp-config) (hons (hons 'st-var st-var) (hons (hons 'in-vars in-vars) (hons (hons 'frame-ins frame-ins) (hons (hons 'rest-ins rest-ins) (hons (hons 'end-ins end-ins) (hons (hons 'frame-in-vars frame-in-vars) (hons (hons 'in-measure in-measure) (hons (hons 'run run) (hons (hons 'st-hyp st-hyp) (hons (hons 'in-hyp in-hyp) (hons (hons 'bindings bindings) (hons (hons 'bound-vars bound-vars) (hons (hons 'initstp initstp) (hons (hons 'nextst nextst) (hons (hons 'constr constr) (hons (hons 'prop prop) (hons (hons 'st-hyp-method st-hyp-method) (hons (hons 'hints hints) (hons (hons 'main-rewrite-rules main-rewrite-rules) (hons (hons 'main-branch-merge-rules main-branch-merge-rules) (hons (hons 'extract-rewrite-rules extract-rewrite-rules) (hons (hons 'extract-branch-merge-rules extract-branch-merge-rules) nil)))))))))))))))))))))))))