|
|
|---|
|
|
|
|---|
Raw constructor for honsed constraint-tuple-p structures.
Syntax:
(honsed-constraint-tuple rule existing-lits matching-lit
common-vars existing-vars sig-table)This is identical to constraint-tuple, except that we hons the structure we are creating.
This is an ordinary honsing constructor introduced by std::defaggregate.
Function:
(defun honsed-constraint-tuple (rule existing-lits matching-lit common-vars existing-vars sig-table) (declare (xargs :guard (and))) (mbe :logic (constraint-tuple rule existing-lits matching-lit common-vars existing-vars sig-table) :exec (hons (hons 'rule rule) (hons (hons 'existing-lits existing-lits) (hons (hons 'matching-lit matching-lit) (hons (hons 'common-vars common-vars) (hons (hons 'existing-vars existing-vars) (hons (hons 'sig-table sig-table) nil))))))))