		Search-engine friendly clone of the ACL2 documentation.

Aig2c

Aig2c-epilogue

Create the assignments from AIG nodes to outputs.

Signature
(aig2c-epilogue aig-alist tempmap code) → new-code
Arguments: aig-alist — Alist binding names to AIGs.
Guard (string-listp (alist-keys aig-alist)).; tempmap — Binds each AIG to its temporary C variable name.
Guard (string-listp (alist-vals tempmap)).; code — Guard (character-listp code).
Returns: new-code — Type (character-listp new-code), given (force (character-listp code)).

Definitions and Theorems

Function: aig2c-epilogue

(defun aig2c-epilogue (aig-alist tempmap code)
  (declare (xargs :guard (and (string-listp (alist-keys aig-alist))
                              (string-listp (alist-vals tempmap))
                              (character-listp code))))
  (let ((__function__ 'aig2c-epilogue))
    (declare (ignorable __function__))
    (b* (((when (atom aig-alist)) code)
         ((when (atom (car aig-alist)))
          (aig2c-epilogue (cdr aig-alist)
                          tempmap code))
         ((cons c-out-name aig1) (car aig-alist))
         (c-temp-name (cdr (hons-get aig1 tempmap)))
         ((unless c-temp-name)
          (raise "AIG not bound in tempmap!")
          code)
         (code (list* #\Space #\Space code))
         (code (str::revappend-chars c-out-name code))
         (code (list* #\Space #\= #\Space code))
         (code (str::revappend-chars c-temp-name code))
         (code (list* #\Newline #\; code)))
      (aig2c-epilogue (cdr aig-alist)
                      tempmap code))))

Theorem: character-listp-of-aig2c-epilogue

(defthm character-listp-of-aig2c-epilogue
  (implies (force (character-listp code))
           (b* ((new-code (aig2c-epilogue aig-alist tempmap code)))
             (character-listp new-code)))
  :rule-classes :rewrite)