Function:
(defun apply-m-assumption-n-output-transforms (m n aignet aignet2 transforms state) (declare (xargs :stobjs (aignet aignet2 state))) (declare (xargs :guard (and (natp m) (natp n)))) (declare (xargs :guard (<= (+ m n) (num-outs aignet)))) (let ((__function__ 'apply-m-assumption-n-output-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-m-assumption-n-output-transforms!-core m n aignet transforms state)) :exec (b* (((mv aignet2 state) (apply-m-assumption-n-output-transform m n aignet aignet2 (car transforms) state)) ((local-stobjs aignet3) (mv aignet2 aignet3 state))) (apply-m-assumption-n-output-transforms-in-place m n aignet2 aignet3 (cdr transforms) state)))) :msg "All transforms: ~st seconds, ~sa bytes.~%"))))
Theorem:
(defthm normalize-inputs-of-apply-m-assumption-n-output-transforms (b* nil (implies (syntaxp (not (equal aignet2 ''nil))) (equal (apply-m-assumption-n-output-transforms m n aignet aignet2 transforms state) (let ((aignet2 nil)) (apply-m-assumption-n-output-transforms m n aignet aignet2 transforms state))))))
Theorem:
(defthm num-ins-of-apply-m-assumption-n-output-transforms (b* (((mv ?new-aignet2 ?new-state) (apply-m-assumption-n-output-transforms m n aignet aignet2 transforms state))) (equal (stype-count :pi new-aignet2) (stype-count :pi aignet))))
Theorem:
(defthm num-regs-of-apply-m-assumption-n-output-transforms (b* (((mv ?new-aignet2 ?new-state) (apply-m-assumption-n-output-transforms m n aignet aignet2 transforms state))) (equal (stype-count :reg new-aignet2) (stype-count :reg aignet))))
Theorem:
(defthm num-outs-of-apply-m-assumption-n-output-transforms (b* (((mv ?new-aignet2 ?new-state) (apply-m-assumption-n-output-transforms m n aignet aignet2 transforms state))) (equal (stype-count :po new-aignet2) (stype-count :po aignet))))
Theorem:
(defthm apply-m-assumption-n-output-transforms-correct (b* (((mv ?new-aignet2 ?new-state) (apply-m-assumption-n-output-transforms m n aignet aignet2 transforms state))) (and (implies (< (nfix i) (nfix m)) (equal (output-eval i invals regvals new-aignet2) (output-eval i invals regvals aignet))) (implies (and (< (nfix i) (+ (nfix m) (nfix n))) (equal (conjoin-output-range 0 m invals regvals aignet) 1)) (equal (output-eval i invals regvals new-aignet2) (output-eval i invals regvals aignet))))))
Theorem:
(defthm w-state-of-apply-m-assumption-n-output-transforms (b* (((mv ?new-aignet2 ?new-state) (apply-m-assumption-n-output-transforms m n aignet aignet2 transforms state))) (equal (w new-state) (w state))))
Theorem:
(defthm list-of-outputs-of-apply-m-assumption-n-output-transforms (b* (((mv ?new-aignet2 ?new-state) (apply-m-assumption-n-output-transforms m n aignet aignet2 transforms state))) (equal (list new-aignet2 new-state) (apply-m-assumption-n-output-transforms m n aignet aignet2 transforms state))))