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