Like fraig, but overwrites the original network instead of returning a new one.
(fraig! aignet config state) → (mv new-aignet new-state)
Function:
(defun fraig! (aignet config state) (declare (xargs :stobjs (aignet state))) (declare (xargs :guard (fraig-config-p config))) (let ((__function__ 'fraig!)) (declare (ignorable __function__)) (b* (((local-stobjs aignet-tmp) (mv aignet aignet-tmp state)) ((mv aignet-tmp state) (fraig-core aignet aignet-tmp config state)) (aignet (aignet-prune-comb aignet-tmp aignet (fraig-config->gatesimp config)))) (mv aignet aignet-tmp state))))
Theorem:
(defthm num-ins-of-fraig! (b* (((mv ?new-aignet ?new-state) (fraig! aignet config state))) (equal (stype-count :pi new-aignet) (stype-count :pi aignet))))
Theorem:
(defthm num-regs-of-fraig! (b* (((mv ?new-aignet ?new-state) (fraig! aignet config state))) (equal (stype-count :reg new-aignet) (stype-count :reg aignet))))
Theorem:
(defthm num-outs-of-fraig! (b* (((mv ?new-aignet ?new-state) (fraig! aignet config state))) (equal (stype-count :po new-aignet) (stype-count :po aignet))))
Theorem:
(defthm fraig!-comb-equivalent (b* (((mv ?new-aignet ?new-state) (fraig! aignet config state))) (comb-equiv new-aignet aignet)))
Theorem:
(defthm w-state-of-fraig! (b* (((mv ?new-aignet ?new-state) (fraig! aignet config state))) (equal (w new-state) (w state))))
Theorem:
(defthm fraig!-of-fraig-config-fix-config (equal (fraig! aignet (fraig-config-fix config) state) (fraig! aignet config state)))
Theorem:
(defthm fraig!-fraig-config-equiv-congruence-on-config (implies (fraig-config-equiv config config-equiv) (equal (fraig! aignet config state) (fraig! aignet config-equiv state))) :rule-classes :congruence)