Write an aignet into a binary AIGER file.
(aignet-write-aiger fname aignet state) → new-state
(defun aignet-write-aiger (fname aignet state) (declare (xargs :stobjs (aignet state))) (declare (xargs :guard (stringp fname))) (let ((__function__ 'aignet-write-aiger)) (declare (ignorable __function__)) (b* (((mv channel state) (open-output-channel! fname :byte state)) ((unless channel) (er hard? 'aignet-write-aiger "Failed to open aiger output file ~x0~%" fname) state) (state (aignet-write-aiger-chan aignet channel state))) (close-output-channel channel state))))
(defthm state-p1-of-aignet-write-aiger (implies (and (stringp fname) (state-p1 state)) (state-p1 (aignet-write-aiger fname aignet state))))