		Search-engine friendly clone of the ACL2 documentation.

Aignet

Aignet-write-aiger

Write an aignet into a binary AIGER file.

Signature
(aignet-write-aiger fname aignet state) → new-state
Arguments: fname — the aiger file to be written.
Guard (stringp fname).; aignet — the network to write out.

Definitions and Theorems

Function: aignet-write-aiger

(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))))

Theorem: state-p1-of-aignet-write-aiger

(defthm
     state-p1-of-aignet-write-aiger
     (implies (and (stringp fname) (state-p1 state))
              (state-p1 (aignet-write-aiger fname aignet state))))

Theorem: w-state-of-aignet-write-aiger

(defthm w-state-of-aignet-write-aiger
        (b* ((?new-state (aignet-write-aiger fname aignet state)))
            (equal (w new-state) (w state))))