(fraig-output-map-mark-simplified output-map prev-count aignet mark) → new-mark
Function:
(defun fraig-output-map-mark-simplified (output-map prev-count aignet mark) (declare (xargs :stobjs (aignet mark))) (declare (xargs :guard (and (fraig-output-map-p output-map) (natp prev-count)))) (declare (xargs :guard (<= (num-fanins aignet) (bits-length mark)))) (let ((__function__ 'fraig-output-map-mark-simplified)) (declare (ignorable __function__)) (b* (((when (<= (num-outs aignet) (lnfix prev-count))) (and (consp output-map) (cw "Warning: extra entries in the output map; only ~x0 outputs in the AIG~%" (num-outs aignet))) mark) ((when (atom output-map)) (aignet-mark-dfs-outs-range prev-count (num-outs aignet) mark aignet)) ((fraig-output-map-entry ent) (car output-map)) (mark (if (fraig-output-type-case ent.type :simplify) (aignet-mark-dfs-outs-range prev-count (min (+ (lnfix prev-count) ent.count) (num-outs aignet)) mark aignet) mark))) (fraig-output-map-mark-simplified (cdr output-map) (+ (lnfix prev-count) ent.count) aignet mark))))
Theorem:
(defthm len-of-fraig-output-map-mark-simplified-nondecreasing (b* ((?new-mark (fraig-output-map-mark-simplified output-map prev-count aignet mark))) (>= (len new-mark) (len mark))) :rule-classes :linear)
Theorem:
(defthm fraig-output-map-mark-simplified-of-fraig-output-map-fix-output-map (equal (fraig-output-map-mark-simplified (fraig-output-map-fix output-map) prev-count aignet mark) (fraig-output-map-mark-simplified output-map prev-count aignet mark)))
Theorem:
(defthm fraig-output-map-mark-simplified-fraig-output-map-equiv-congruence-on-output-map (implies (fraig-output-map-equiv output-map output-map-equiv) (equal (fraig-output-map-mark-simplified output-map prev-count aignet mark) (fraig-output-map-mark-simplified output-map-equiv prev-count aignet mark))) :rule-classes :congruence)
Theorem:
(defthm fraig-output-map-mark-simplified-of-nfix-prev-count (equal (fraig-output-map-mark-simplified output-map (nfix prev-count) aignet mark) (fraig-output-map-mark-simplified output-map prev-count aignet mark)))
Theorem:
(defthm fraig-output-map-mark-simplified-nat-equiv-congruence-on-prev-count (implies (nat-equiv prev-count prev-count-equiv) (equal (fraig-output-map-mark-simplified output-map prev-count aignet mark) (fraig-output-map-mark-simplified output-map prev-count-equiv aignet mark))) :rule-classes :congruence)