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