		Search-engine friendly clone of the ACL2 documentation.

Aig2c

Aig2c-maketemps

Create the temporary C code variable names that will be used for each each AIG node, for a single AIG.

Signature
(aig2c-maketemps x config tempmap db) → (mv new-map new-db)
Arguments: x — The AIG to process.; config — Guard (aig2c-config-p config).; tempmap — Answer we are accumulating. Fast alist assigning AIG nodes and variables to fresh, "temporary" names.
Guard (string-listp (alist-vals tempmap)).; db — Name database to make sure the names we are generating are really unique.
Guard (vl::vl-namedb-p db).
Returns: new-map — Fast alist mapping AIG nodes to their newly assigned names.; new-db — Updated name database.
Type (vl::vl-namedb-p new-db), given (and (force (vl::vl-namedb-p db)) (force (aig2c-config-p config))).

Definitions and Theorems

Function: aig2c-maketemps

(defun aig2c-maketemps (x config tempmap db)
  (declare (xargs :guard (and (aig2c-config-p config)
                              (string-listp (alist-vals tempmap))
                              (vl::vl-namedb-p db))))
  (let ((__function__ 'aig2c-maketemps))
    (declare (ignorable __function__))
    (b* (((when (hons-get x tempmap))
          (mv tempmap db))
         ((mv fresh-name db)
          (vl::vl-namedb-indexed-name (aig2c-config->prefix config)
                                      db))
         (tempmap (hons-acons x fresh-name tempmap))
         ((when (atom x)) (mv tempmap db))
         ((when (not (cdr x)))
          (aig2c-maketemps (car x)
                           config tempmap db))
         ((mv tempmap db)
          (aig2c-maketemps (car x)
                           config tempmap db))
         ((mv tempmap db)
          (aig2c-maketemps (cdr x)
                           config tempmap db)))
      (mv tempmap db))))

Theorem: vl-namedb-p-of-aig2c-maketemps.new-db

(defthm vl-namedb-p-of-aig2c-maketemps.new-db
  (implies (and (force (vl::vl-namedb-p db))
                (force (aig2c-config-p config)))
           (b* (((mv ?new-map ?new-db)
                 (aig2c-maketemps x config tempmap db)))
             (vl::vl-namedb-p new-db)))
  :rule-classes :rewrite)

Theorem: string-listp-of-alist-vals-of-aig2c-maketemps

(defthm string-listp-of-alist-vals-of-aig2c-maketemps
  (b* (((mv new-map ?new-db)
        (aig2c-maketemps x config tempmap db)))
    (implies (and (force (string-listp (alist-vals tempmap)))
                  (force (vl::vl-namedb-p db))
                  (force (aig2c-config-p config)))
             (string-listp (alist-vals new-map)))))

Theorem: aig2c-maketemps-monotonic

(defthm aig2c-maketemps-monotonic
  (b* (((mv new-map ?new-db)
        (aig2c-maketemps x config tempmap db)))
    (implies (subsetp-equal keys (alist-keys tempmap))
             (subsetp-equal keys (alist-keys new-map)))))