Function:
(defun apply-m-assumption-n-output-output-transform-default (m n aignet aignet2 transform 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-output-transform-default)) (declare (ignorable __function__)) (b* (((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 state))) (name (m-assumption-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 (+ (lnfix m) (lnfix n)) aignet aignet2 transform))) (mv aignet2 state))) (:n-outputs-dom-supergates-sweep-config (b* ((aignet2 (n-outputs-dom-supergates-sweep (+ (lnfix m) (lnfix n)) aignet aignet2 transform))) (mv aignet2 state))) (:m-assum-n-output-observability-config (m-assum-n-output-observability m n aignet aignet2 transform 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-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 state) (let ((aignet2 nil)) (apply-m-assumption-n-output-output-transform-default m n aignet aignet2 transform state))))))
Theorem:
(defthm num-ins-of-apply-m-assumption-n-output-output-transform-default (b* (((mv ?new-aignet2 ?new-state) (apply-m-assumption-n-output-output-transform-default m n aignet aignet2 transform 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-state) (apply-m-assumption-n-output-output-transform-default m n aignet aignet2 transform 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-state) (apply-m-assumption-n-output-output-transform-default m n aignet aignet2 transform state))) (equal (stype-count :po new-aignet2) (stype-count :po aignet))))
Theorem:
(defthm apply-m-assumption-n-output-output-transform-default-eval-assumptions (b* (((mv ?new-aignet2 ?new-state) (apply-m-assumption-n-output-output-transform-default m n aignet aignet2 transform 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-state) (apply-m-assumption-n-output-output-transform-default m n aignet aignet2 transform 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-state) (apply-m-assumption-n-output-output-transform-default m n aignet aignet2 transform 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-state) (apply-m-assumption-n-output-output-transform-default m n aignet aignet2 transform state))) (equal (list new-aignet2 new-state) (apply-m-assumption-n-output-output-transform-default m n aignet aignet2 transform state))))