		Search-engine friendly clone of the ACL2 documentation.

Aignet

Aignet-read-aiger

Read an aignet from a binary AIGER file.

Signature
(aignet-read-aiger fname aignet state) → (mv err new-aignet new-state)
Arguments: fname — the name of the aiger file to be read.
Guard (stringp fname).; aignet — will be emptied and replaced with the contents of the aiger file.

Definitions and Theorems

Function: aignet-read-aiger

(defun aignet-read-aiger (fname aignet state)
  (declare (xargs :stobjs (aignet state)))
  (declare (xargs :guard (stringp fname)))
  (let ((__function__ 'aignet-read-aiger))
    (declare (ignorable __function__))
    (b* (((mv channel state)
          (open-input-channel fname :byte state))
         ((when (not channel))
          (mv "Could not open input file"
              aignet state))
         ((mv err aignet state)
          (aignet-read-aiger-chan aignet channel state))
         (state (close-input-channel channel state)))
      (mv err aignet state))))

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

(defthm state-p1-of-aignet-read-aiger
  (implies
       (and (state-p1 state) (stringp fname))
       (state-p1 (mv-nth 2
                         (aignet-read-aiger fname aignet state)))))

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

(defthm w-state-of-aignet-read-aiger
  (b* (((mv ?err ?new-aignet ?new-state)
        (aignet-read-aiger fname aignet state)))
    (equal (w new-state) (w state))))