		Search-engine friendly clone of the ACL2 documentation.

Aig-other

Aiger-write

Write out a collection of AIGs into an AIGER file, directly, without going through aignet.

Signature
(aiger-write fname &optional latch-aigs out-aigs bad-aigs cnstr-aigs (state 'state)) → (mv pis state)
Arguments: fname — The file name to use.
Guard (stringp fname).; latch-aigs — Alist mapping latch names to their update functions.
Guard (true-listp latch-aigs).; out-aigs — List of primary output AIGs.
Guard (true-listp out-aigs).; bad-aigs — List of bad-state AIGs.
Guard (true-listp bad-aigs).; cnstr-aigs — List of constraint AIGs.
Guard (true-listp cnstr-aigs).
Returns: pis — The ordering of primary inputs that we use in the resulting AIGER file, derived from variables within the input AIGs.

See also aignet::aiger-write for an aignet-based alternative. We generally prefer to use aignet::aiger-write and may eventually move to deprecate this function.

Definitions and Theorems

Function: aiger-write-fn

(defun aiger-write-fn (fname latch-aigs
                             out-aigs bad-aigs cnstr-aigs state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (and (stringp fname)
                             (true-listp latch-aigs)
                             (true-listp out-aigs)
                             (true-listp bad-aigs)
                             (true-listp cnstr-aigs))))
 (let ((__function__ 'aiger-write))
   (declare (ignorable __function__))
   (b*
     (((mv channel state)
       (open-output-channel! fname
                             :byte state))
      ((unless channel)
       (ec-call
            (aiger-write-binary latch-aigs out-aigs
                                bad-aigs cnstr-aigs channel state)))
      ((mv pis state)
       (aiger-write-binary latch-aigs out-aigs
                           bad-aigs cnstr-aigs channel state))
      (state (close-output-channel channel state)))
     (mv pis state))))