(apply-m-assumption-n-output-output-transform-default m n aignet aignet2 transform output-ranges state) → (mv new-aignet2 new-output-ranges new-state)
Function:
(defun apply-m-assumption-n-output-output-transform-default (m n aignet aignet2 transform output-ranges state) (declare (xargs :stobjs (aignet aignet2 state))) (declare (xargs :guard (and (natp m) (natp n) (aignet-output-range-map-p output-ranges)))) (declare (xargs :guard (<= (+ m n) (num-outs aignet)))) (let ((__function__ 'apply-m-assumption-n-output-output-transform-default)) (declare (ignorable __function__)) (b* ((output-ranges (aignet-output-range-map-fix output-ranges)) ((unless (m-assumption-n-output-comb-transform-p transform)) (raise "Bad transform config object; should satisfy ~x1: ~x0~%" transform 'm-assumption-n-output-comb-transform-p) (b* ((aignet2 (aignet-raw-copy aignet aignet2))) (mv aignet2 output-ranges state))) (name (m-assumption-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 m) (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 (+ (lnfix m) (lnfix n)) aignet aignet2 transform))) (:n-outputs-dom-supergates-sweep-config (aignet2-return aignet2 (n-outputs-dom-supergates-sweep (+ (lnfix m) (lnfix n)) aignet aignet2 transform))) (:m-assum-n-output-observability-config (aignet2-return (mv aignet2 state) (m-assum-n-output-observability m n aignet aignet2 transform state))) (:parametrize-config (aignet2-return aignet2 (aignet-parametrize-m-n m n aignet aignet2 transform output-ranges))) (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-m-assumption-n-output-output-transform-default.new-output-ranges (b* (((mv ?new-aignet2 ?new-output-ranges ?new-state) (apply-m-assumption-n-output-output-transform-default m n aignet aignet2 transform output-ranges state))) (aignet-output-range-map-p new-output-ranges)) :rule-classes :rewrite)
Theorem:
(defthm normalize-inputs-of-apply-m-assumption-n-output-output-transform-default (b* nil (implies (syntaxp (not (equal aignet2 ''nil))) (equal (apply-m-assumption-n-output-output-transform-default m n aignet aignet2 transform output-ranges state) (let ((aignet2 nil)) (apply-m-assumption-n-output-output-transform-default m n aignet aignet2 transform output-ranges state))))))
Theorem:
(defthm num-ins-of-apply-m-assumption-n-output-output-transform-default (b* (((mv ?new-aignet2 ?new-output-ranges ?new-state) (apply-m-assumption-n-output-output-transform-default m n aignet aignet2 transform output-ranges state))) (equal (stype-count :pi new-aignet2) (stype-count :pi aignet))))
Theorem:
(defthm num-regs-of-apply-m-assumption-n-output-output-transform-default (b* (((mv ?new-aignet2 ?new-output-ranges ?new-state) (apply-m-assumption-n-output-output-transform-default m n aignet aignet2 transform output-ranges state))) (equal (stype-count :reg new-aignet2) (stype-count :reg aignet))))
Theorem:
(defthm num-outs-of-apply-m-assumption-n-output-output-transform-default (b* (((mv ?new-aignet2 ?new-output-ranges ?new-state) (apply-m-assumption-n-output-output-transform-default m n aignet aignet2 transform output-ranges state))) (implies (<= (+ (nfix m) (nfix n)) (stype-count :po aignet)) (<= (+ (nfix m) (nfix n)) (stype-count :po new-aignet2)))) :rule-classes ((:linear :trigger-terms ((aignet-output-range-map-length (mv-nth 1 (apply-m-assumption-n-output-output-transform-default m n aignet aignet2 transform output-ranges state))) (stype-count :po (mv-nth 0 (apply-m-assumption-n-output-output-transform-default m n aignet aignet2 transform output-ranges state)))))))
Theorem:
(defthm num-outs-of-apply-m-assumption-n-output-output-transform-default-relative-to-output-map-length (b* (((mv ?new-aignet2 ?new-output-ranges ?new-state) (apply-m-assumption-n-output-output-transform-default m 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-m-assumption-n-output-output-transform-default m n aignet aignet2 transform output-ranges state))) (stype-count :po (mv-nth 0 (apply-m-assumption-n-output-output-transform-default m n aignet aignet2 transform output-ranges state)))))))
Theorem:
(defthm apply-m-assumption-n-output-output-transform-default-eval-assumptions (b* (((mv ?new-aignet2 ?new-output-ranges ?new-state) (apply-m-assumption-n-output-output-transform-default m n aignet aignet2 transform output-ranges state))) (implies (< (nfix i) (nfix m)) (equal (output-eval i invals regvals new-aignet2) (output-eval i invals regvals aignet)))))
Theorem:
(defthm apply-m-assumption-n-output-output-transform-default-eval-conclusion (b* (((mv ?new-aignet2 ?new-output-ranges ?new-state) (apply-m-assumption-n-output-output-transform-default m n aignet aignet2 transform output-ranges state))) (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-output-transform-default (b* (((mv ?new-aignet2 ?new-output-ranges ?new-state) (apply-m-assumption-n-output-output-transform-default m n aignet aignet2 transform output-ranges state))) (equal (w new-state) (w state))))
Theorem:
(defthm list-of-outputs-of-apply-m-assumption-n-output-output-transform-default (b* (((mv ?new-aignet2 ?new-output-ranges ?new-state) (apply-m-assumption-n-output-output-transform-default m n aignet aignet2 transform output-ranges state))) (equal (list new-aignet2 new-output-ranges new-state) (apply-m-assumption-n-output-output-transform-default m n aignet aignet2 transform output-ranges state))))