(fraig-create-aignet-node-mask aignet output-map level-limit mark) → new-mark
Function:
(defun fraig-create-aignet-node-mask (aignet output-map level-limit mark) (declare (xargs :stobjs (aignet mark))) (declare (xargs :guard (and (fraig-output-map-p output-map) (natp level-limit)))) (declare (xargs :guard (non-exec (equal mark (acl2::create-bitarr))))) (let ((__function__ 'fraig-create-aignet-node-mask)) (declare (ignorable __function__)) (b* ((mark (mbe :logic (non-exec (acl2::create-bitarr)) :exec mark)) ((local-stobjs mark2) (mv mark2 mark)) (mark (resize-bits (num-fanins aignet) mark)) (mark2 (resize-bits (num-fanins aignet) mark2)) (mark (fraig-output-map-mark-simplified output-map 0 aignet mark)) (mark2 (fraig-output-map-mark-non-simplified output-map 0 aignet mark2)) (mark2 (aignet-mark-fanout-cones-of-marked 0 mark2 aignet)) (mark (bitarr-remove-marked 0 (num-fanins aignet) mark mark2)) ((when (eql (lnfix level-limit) 0)) (b* ((mark (set-bit 0 1 mark))) (mv mark2 mark))) ((local-stobjs aignet-levels) (mv mark2 aignet-levels mark)) (aignet-levels (aignet-record-levels aignet aignet-levels)) (mark (aignet-unmark-higher-levels 0 level-limit aignet-levels mark)) (mark (set-bit 0 1 mark))) (mv mark2 aignet-levels mark))))
Theorem:
(defthm len-of-fraig-create-aignet-node-mask (b* ((?new-mark (fraig-create-aignet-node-mask aignet output-map level-limit mark))) (<= (num-fanins aignet) (len new-mark))) :rule-classes :linear)
Theorem:
(defthm normalize-mark-of-fraig-create-aignet-node-mask (b* nil (implies (syntaxp (not (equal mark ''nil))) (equal (fraig-create-aignet-node-mask aignet output-map level-limit mark) (fraig-create-aignet-node-mask aignet output-map level-limit nil)))))
Theorem:
(defthm fraig-create-aignet-node-mask-of-fraig-output-map-fix-output-map (equal (fraig-create-aignet-node-mask aignet (fraig-output-map-fix output-map) level-limit mark) (fraig-create-aignet-node-mask aignet output-map level-limit mark)))
Theorem:
(defthm fraig-create-aignet-node-mask-fraig-output-map-equiv-congruence-on-output-map (implies (fraig-output-map-equiv output-map output-map-equiv) (equal (fraig-create-aignet-node-mask aignet output-map level-limit mark) (fraig-create-aignet-node-mask aignet output-map-equiv level-limit mark))) :rule-classes :congruence)
Theorem:
(defthm fraig-create-aignet-node-mask-of-nfix-level-limit (equal (fraig-create-aignet-node-mask aignet output-map (nfix level-limit) mark) (fraig-create-aignet-node-mask aignet output-map level-limit mark)))
Theorem:
(defthm fraig-create-aignet-node-mask-nat-equiv-congruence-on-level-limit (implies (nat-equiv level-limit level-limit-equiv) (equal (fraig-create-aignet-node-mask aignet output-map level-limit mark) (fraig-create-aignet-node-mask aignet output-map level-limit-equiv mark))) :rule-classes :congruence)