(fraig-debug-output-ranges output-ranges aignet) → *
Function:
(defun fraig-debug-output-ranges (output-ranges aignet) (declare (xargs :stobjs (aignet))) (declare (xargs :guard (aignet-output-range-map-p output-ranges))) (let ((__function__ 'fraig-debug-output-ranges)) (declare (ignorable __function__)) (progn$ (cw "----- Debug output ranges:~%") (cw "Number of outputs: ~x0~%" (num-outs aignet)) (cw "Output-ranges length: ~x0~%" (aignet-output-range-map-length output-ranges)) (cw "output-ranges: ~x0~%" output-ranges) (cw "----- End debug output ranges~%"))))
Theorem:
(defthm fraig-debug-output-ranges-of-aignet-output-range-map-fix-output-ranges (equal (fraig-debug-output-ranges (aignet-output-range-map-fix output-ranges) aignet) (fraig-debug-output-ranges output-ranges aignet)))
Theorem:
(defthm fraig-debug-output-ranges-aignet-output-range-map-equiv-congruence-on-output-ranges (implies (aignet-output-range-map-equiv output-ranges output-ranges-equiv) (equal (fraig-debug-output-ranges output-ranges aignet) (fraig-debug-output-ranges output-ranges-equiv aignet))) :rule-classes :congruence)