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