(apply-n-output-comb-transform-default n aignet aignet2 transform state) → (mv new-aignet2 new-state)
Function:
(defun apply-n-output-comb-transform-default (n aignet aignet2 transform state) (declare (xargs :stobjs (aignet aignet2 state))) (declare (xargs :guard (natp n))) (declare (xargs :guard (<= n (num-outs aignet)))) (let ((__function__ 'apply-n-output-comb-transform-default)) (declare (ignorable __function__)) (b* (((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 state))) (name (n-output-comb-transform->name transform))) (time$ (b* (((mv aignet2 state) (case (tag transform) (:balance-config (b* ((aignet2 (balance aignet aignet2 transform))) (mv aignet2 state))) (:fraig-config (fraig aignet aignet2 transform state)) (:rewrite-config (b* ((aignet2 (rewrite aignet aignet2 transform))) (mv aignet2 state))) (:obs-constprop-config (obs-constprop aignet aignet2 transform state)) (:observability-config (observability-fix aignet aignet2 transform state)) (:constprop-config (b* ((aignet2 (constprop aignet aignet2 transform))) (mv aignet2 state))) (:snapshot-config (b* ((state (aignet-write-aiger (snapshot-config->filename transform) aignet state)) (aignet2 (aignet-raw-copy aignet aignet2))) (mv aignet2 state))) (:prune-config (b* ((aignet2 (prune aignet aignet2 transform))) (mv aignet2 state))) (:unreachability-config (b* ((aignet2 (unreachability aignet aignet2 transform))) (mv aignet2 state))) (:dom-supergates-sweep-config (b* ((aignet2 (dom-supergates-sweep aignet aignet2 transform))) (mv aignet2 state))) (:n-outputs-unreachability-config (b* ((aignet2 (n-outputs-unreachability n aignet aignet2 transform))) (mv aignet2 state))) (:n-outputs-dom-supergates-sweep-config (b* ((aignet2 (n-outputs-dom-supergates-sweep n aignet aignet2 transform))) (mv aignet2 state))) (otherwise (abc-comb-simplify aignet aignet2 transform state)))) (- (print-aignet-stats name aignet2))) (mv aignet2 state)) :msg "~s0 transform: ~st seconds, ~sa bytes.~%" :args (list name)))))
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 state) (let ((aignet2 nil)) (apply-n-output-comb-transform-default n aignet aignet2 transform state))))))
Theorem:
(defthm num-ins-of-apply-n-output-comb-transform-default (b* (((mv ?new-aignet2 ?new-state) (apply-n-output-comb-transform-default n aignet aignet2 transform 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-state) (apply-n-output-comb-transform-default n aignet aignet2 transform 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-state) (apply-n-output-comb-transform-default n aignet aignet2 transform state))) (equal (stype-count :po new-aignet2) (stype-count :po aignet))))
Theorem:
(defthm apply-n-output-comb-transform-default-outputs-equivalent (b* (((mv ?new-aignet2 ?new-state) (apply-n-output-comb-transform-default n aignet aignet2 transform 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-state) (apply-n-output-comb-transform-default n aignet aignet2 transform state))) (equal (w new-state) (w state))))
Theorem:
(defthm list-of-outputs-of-apply-n-output-comb-transform-default (b* (((mv ?new-aignet2 ?new-state) (apply-n-output-comb-transform-default n aignet aignet2 transform state))) (equal (list new-aignet2 new-state) (apply-n-output-comb-transform-default n aignet aignet2 transform state))))