(apply-n-output-comb-transform-default n aignet aignet2 transform output-ranges state) → (mv new-aignet2 new-output-ranges new-state)
Function:
(defun apply-n-output-comb-transform-default (n aignet aignet2 transform output-ranges state) (declare (xargs :stobjs (aignet aignet2 state))) (declare (xargs :guard (and (natp n) (aignet-output-range-map-p output-ranges)))) (declare (xargs :guard (<= n (num-outs aignet)))) (let ((__function__ 'apply-n-output-comb-transform-default)) (declare (ignorable __function__)) (b* ((output-ranges (aignet-output-range-map-fix output-ranges)) ((unless (n-output-comb-transform-p transform)) (raise "Bad transform config object; should satisfy ~x1: ~x0~%" transform 'n-output-comb-transform-p) (b* ((aignet2 (aignet-raw-copy aignet aignet2))) (mv aignet2 output-ranges state))) (name (n-output-comb-transform->name transform))) (time$ (b* (((mv aignet2 output-ranges state) (case (tag transform) (:balance-config (aignet2-return aignet2 (balance aignet aignet2 transform))) (:fraig-config (fraig (lnfix n) aignet aignet2 transform output-ranges state)) (:rewrite-config (aignet2-return aignet2 (rewrite aignet aignet2 transform))) (:obs-constprop-config (aignet2-return (mv aignet2 state) (obs-constprop aignet aignet2 transform state))) (:observability-config (aignet2-return (mv aignet2 state) (observability-fix aignet aignet2 transform state))) (:constprop-config (aignet2-return aignet2 (constprop aignet aignet2 transform))) (:snapshot-config (b* ((state (aignet-write-aiger (snapshot-config->filename transform) aignet state)) (aignet2 (aignet-raw-copy aignet aignet2))) (mv aignet2 output-ranges state))) (:prune-config (aignet2-return aignet2 (prune aignet aignet2 transform))) (:unreachability-config (aignet2-return aignet2 (unreachability aignet aignet2 transform))) (:dom-supergates-sweep-config (aignet2-return aignet2 (dom-supergates-sweep aignet aignet2 transform))) (:n-outputs-unreachability-config (aignet2-return aignet2 (n-outputs-unreachability n aignet aignet2 transform))) (:n-outputs-dom-supergates-sweep-config (aignet2-return aignet2 (n-outputs-dom-supergates-sweep n aignet aignet2 transform))) (otherwise (aignet2-return (mv aignet2 state) (abc-comb-simplify aignet aignet2 transform state))))) (- (print-aignet-stats name aignet2))) (mv aignet2 output-ranges state)) :msg "~s0 transform: ~st seconds, ~sa bytes.~%" :args (list name)))))
Theorem:
(defthm aignet-output-range-map-p-of-apply-n-output-comb-transform-default.new-output-ranges (b* (((mv ?new-aignet2 ?new-output-ranges ?new-state) (apply-n-output-comb-transform-default n aignet aignet2 transform output-ranges state))) (aignet-output-range-map-p new-output-ranges)) :rule-classes :rewrite)
Theorem:
(defthm normalize-inputs-of-apply-n-output-comb-transform-default (b* nil (implies (syntaxp (not (equal aignet2 ''nil))) (equal (apply-n-output-comb-transform-default n aignet aignet2 transform output-ranges state) (let ((aignet2 nil)) (apply-n-output-comb-transform-default n aignet aignet2 transform output-ranges state))))))
Theorem:
(defthm num-ins-of-apply-n-output-comb-transform-default (b* (((mv ?new-aignet2 ?new-output-ranges ?new-state) (apply-n-output-comb-transform-default n aignet aignet2 transform output-ranges state))) (equal (stype-count :pi new-aignet2) (stype-count :pi aignet))))
Theorem:
(defthm num-regs-of-apply-n-output-comb-transform-default (b* (((mv ?new-aignet2 ?new-output-ranges ?new-state) (apply-n-output-comb-transform-default n aignet aignet2 transform output-ranges state))) (equal (stype-count :reg new-aignet2) (stype-count :reg aignet))))
Theorem:
(defthm num-outs-of-apply-n-output-comb-transform-default (b* (((mv ?new-aignet2 ?new-output-ranges ?new-state) (apply-n-output-comb-transform-default n aignet aignet2 transform output-ranges state))) (implies (<= (nfix n) (stype-count :po aignet)) (<= (nfix n) (stype-count :po new-aignet2)))) :rule-classes ((:linear :trigger-terms ((stype-count :po (mv-nth 0 (apply-n-output-comb-transform-default n aignet aignet2 transform output-ranges state)))))))
Theorem:
(defthm num-outs-of-apply-n-output-comb-transform-default-relative-to-output-map-length (b* (((mv ?new-aignet2 ?new-output-ranges ?new-state) (apply-n-output-comb-transform-default n aignet aignet2 transform output-ranges state))) (implies (<= (aignet-output-range-map-length output-ranges) (stype-count :po aignet)) (<= (aignet-output-range-map-length new-output-ranges) (stype-count :po new-aignet2)))) :rule-classes ((:linear :trigger-terms ((aignet-output-range-map-length (mv-nth 1 (apply-n-output-comb-transform-default n aignet aignet2 transform output-ranges state))) (stype-count :po (mv-nth 0 (apply-n-output-comb-transform-default n aignet aignet2 transform output-ranges state)))))))
Theorem:
(defthm apply-n-output-comb-transform-default-outputs-equivalent (b* (((mv ?new-aignet2 ?new-output-ranges ?new-state) (apply-n-output-comb-transform-default n aignet aignet2 transform output-ranges state))) (implies (< (nfix i) (nfix n)) (equal (output-eval i invals regvals new-aignet2) (output-eval i invals regvals aignet)))))
Theorem:
(defthm w-state-of-apply-n-output-comb-transform-default (b* (((mv ?new-aignet2 ?new-output-ranges ?new-state) (apply-n-output-comb-transform-default n aignet aignet2 transform output-ranges state))) (equal (w new-state) (w state))))
Theorem:
(defthm list-of-outputs-of-apply-n-output-comb-transform-default (b* (((mv ?new-aignet2 ?new-output-ranges ?new-state) (apply-n-output-comb-transform-default n aignet aignet2 transform output-ranges state))) (equal (list new-aignet2 new-output-ranges new-state) (apply-n-output-comb-transform-default n aignet aignet2 transform output-ranges state))))