(apply-comb-transforms aignet aignet2 transforms state) → (mv new-aignet2 new-state)
Function:
(defun apply-comb-transforms (aignet aignet2 transforms state) (declare (xargs :stobjs (aignet aignet2 state))) (declare (xargs :guard t)) (let ((__function__ 'apply-comb-transforms)) (declare (ignorable __function__)) (prog2$ (print-aignet-stats "Input" aignet) (time$ (b* (((unless (consp transforms)) (b* ((aignet2 (aignet-raw-copy aignet aignet2))) (mv aignet2 state)))) (mbe :logic (non-exec (apply-comb-transforms!-core aignet transforms state)) :exec (b* (((mv aignet2 state) (apply-comb-transform aignet aignet2 (car transforms) state)) ((local-stobjs aignet3) (mv aignet2 aignet3 state))) (apply-comb-transforms-in-place aignet2 aignet3 (cdr transforms) state)))) :msg "All transforms: ~st seconds, ~sa bytes.~%"))))
Theorem:
(defthm normalize-inputs-of-apply-comb-transforms (b* nil (implies (syntaxp (not (equal aignet2 ''nil))) (equal (apply-comb-transforms aignet aignet2 transforms state) (let ((aignet2 nil)) (apply-comb-transforms aignet aignet2 transforms state))))))
Theorem:
(defthm num-ins-of-apply-comb-transforms (b* (((mv ?new-aignet2 ?new-state) (apply-comb-transforms aignet aignet2 transforms state))) (equal (stype-count :pi new-aignet2) (stype-count :pi aignet))))
Theorem:
(defthm num-regs-of-apply-comb-transforms (b* (((mv ?new-aignet2 ?new-state) (apply-comb-transforms aignet aignet2 transforms state))) (equal (stype-count :reg new-aignet2) (stype-count :reg aignet))))
Theorem:
(defthm num-outs-of-apply-comb-transforms (b* (((mv ?new-aignet2 ?new-state) (apply-comb-transforms aignet aignet2 transforms state))) (equal (stype-count :po new-aignet2) (stype-count :po aignet))))
Theorem:
(defthm apply-comb-transforms-correct (b* (((mv ?new-aignet2 ?new-state) (apply-comb-transforms aignet aignet2 transforms state))) (comb-equiv new-aignet2 aignet)))
Theorem:
(defthm w-state-of-apply-comb-transforms (b* (((mv ?new-aignet2 ?new-state) (apply-comb-transforms aignet aignet2 transforms state))) (equal (w new-state) (w state))))
Theorem:
(defthm list-of-outputs-of-apply-comb-transforms (b* (((mv ?new-aignet2 ?new-state) (apply-comb-transforms aignet aignet2 transforms state))) (equal (list new-aignet2 new-state) (apply-comb-transforms aignet aignet2 transforms state))))