		Search-engine friendly clone of the ACL2 documentation.

Aig-other

Aiger-read

Read an AIGER file into a collection of AIGs.

Signature
(aiger-read fname innames latchnames state) → (mv err latch-aigs out-aigs bad-aigs cnstr-aigs state)
Arguments: fname — The file name to read.
Guard (stringp fname).; innames — A list of names to give the primary inputs.
Guard (true-listp innames).; latchnames — A list of names to use for the latches.
Guard (true-listp latchnames).
Returns: err — An error msg on any error.; latch-aigs — An alist of latch names to their update functions.; out-aigs — List of output aigs.; bad-aigs — List of bad-state aigs.; cnstr-aigs — List of constraint aigs.

Definitions and Theorems

Function: aiger-read

(defun
     aiger-read
     (fname innames latchnames state)
     (declare (xargs :stobjs (state)))
     (declare (xargs :guard (and (stringp fname)
                                 (true-listp innames)
                                 (true-listp latchnames))))
     (let ((__function__ 'aiger-read))
          (declare (ignorable __function__))
          (b* (((mv err latch-lits out-lits
                    bad-lits cnstr-lits gates state)
                (aiger-parse fname state))
               ((when err)
                (mv err nil nil nil nil state))
               (- (sneaky-save 'innames innames)
                  (sneaky-save 'latchnames latchnames)
                  (sneaky-save 'latch-lits latch-lits)
                  (sneaky-save 'out-lits out-lits)
                  (sneaky-save 'bad-lits bad-lits)
                  (sneaky-save 'cnstr-lits cnstr-lits)
                  (sneaky-save 'gates gates))
               ((mv latch-aigs out-aigs bad-aigs cnstr-aigs)
                (aiger-to-aigs innames latchnames latch-lits
                               out-lits bad-lits cnstr-lits gates)))
              (mv nil latch-aigs
                  out-aigs bad-aigs cnstr-aigs state))))