Raw constructor for honsed glcp-bit-ctrex-p structures.
Syntax:
(honsed-glcp-bit-ctrex descrip env gvar-alist dont-care-spec)
This is identical to glcp-bit-ctrex, except that we hons the structure we are creating.
This is an ordinary honsing constructor introduced by std::defaggregate.
Function:
(defun honsed-glcp-bit-ctrex (descrip env gvar-alist dont-care-spec) (declare (xargs :guard (and))) (mbe :logic (glcp-bit-ctrex descrip env gvar-alist dont-care-spec) :exec (hons (hons descrip env) (hons gvar-alist dont-care-spec))))