Like abc-comb-simplify, but overwrites the original network instead of returning a new one.
(abc-comb-simplify! aignet config state) → (mv new-aignet new-state)
Function:
(defun abc-comb-simplify! (aignet config state) (declare (xargs :stobjs (aignet state))) (declare (xargs :guard (abc-comb-simp-config-p config))) (let ((__function__ 'abc-comb-simplify!)) (declare (ignorable __function__)) (b* (((abc-comb-simp-config config)) ((mv input-filename state) (oslib::tempfile "abc-comb-simplify-input.aig")) ((mv output-filename state) (oslib::tempfile "abc-comb-simplify-output.aig")) ((mv script-filename state) (oslib::tempfile "abc-comb-simplify-script")) ((unless (and input-filename output-filename script-filename)) (cw "Error -- couldn't generate temp filenames.~%") (mv aignet state)) (script (str::cat "&r " input-filename "; " config.script "; &w " output-filename)) ((local-stobjs frames aignet2) (mv aignet state frames aignet2)) ((mv status aignet2 frames) (aignet-abc aignet aignet2 frames script :script-filename script-filename :input-filename input-filename :output-filename output-filename :axiom :comb-simp)) ((when (stringp status)) (cw "Error -- ABC failed: ~s0~%" status) (mv aignet state frames aignet2)) (aignet (aignet-raw-copy aignet2 aignet))) (mv aignet state frames aignet2))))
Theorem:
(defthm num-ins-of-abc-comb-simplify! (b* (((mv ?new-aignet ?new-state) (abc-comb-simplify! aignet config state))) (equal (stype-count :pi new-aignet) (stype-count :pi aignet))))
Theorem:
(defthm num-regs-of-abc-comb-simplify! (b* (((mv ?new-aignet ?new-state) (abc-comb-simplify! aignet config state))) (equal (stype-count :reg new-aignet) (stype-count :reg aignet))))
Theorem:
(defthm num-outs-of-abc-comb-simplify! (b* (((mv ?new-aignet ?new-state) (abc-comb-simplify! aignet config state))) (equal (stype-count :po new-aignet) (stype-count :po aignet))))
Theorem:
(defthm abc-comb-simplify!-comb-equivalent (b* (((mv ?new-aignet ?new-state) (abc-comb-simplify! aignet config state))) (comb-equiv new-aignet aignet)))
Theorem:
(defthm w-state-of-abc-comb-simplify! (b* (((mv ?new-aignet ?new-state) (abc-comb-simplify! aignet config state))) (equal (w new-state) (w state))))