• Top
  • Documentation
  • Books
  • Boolean-reasoning
    • Ipasir
    • Aignet
    • Aig
      • Aig-constructors
      • Aig-vars
      • Aig-sat
      • Bddify
      • Aig-substitution
      • Aig-other
        • Best-aig
        • Aig2c
          • Aig2c-config-p
          • Aig2c-compile
          • Aig2c-maketemps
          • Aig2c-main
          • Aig2c-prologue
          • Aig2c-maketemps-list
          • Aig2c-epilogue
          • Aig2c-main-list
        • Expr-to-aig
        • Aiger-write
        • Aig-random-sim
        • Aiger-read
        • Aig-print
        • Aig-cases
      • Aig-semantics
      • Aig-and-count
    • Satlink
    • Truth
    • Ubdds
    • Bdd
    • Faig
    • Bed
    • 4v
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Aig2c

Aig2c-maketemps-list

Create the temporary C code variable names for a whole list of AIGs.

Signature

(aig2c-maketemps-list x config tempmap db) 
  → 
(mv new-map new-db)

Arguments

x — AIG list to process.

config — Guard (aig2c-config-p config).

tempmap — Guard (string-listp (alist-vals tempmap)).

db — Guard (vl::vl-namedb-p db).

Returns

new-db — Type (vl::vl-namedb-p new-db), given (and (force (vl::vl-namedb-p db)) (force (aig2c-config-p config))).

This just extends aig2c-maketemps to an AIG list.

Definitions and Theorems

Function: aig2c-maketemps-list

(defun aig2c-maketemps-list (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-list))
    (declare (ignorable __function__))
    (b* (((when (atom x)) (mv tempmap db))
         ((mv tempmap db)
          (aig2c-maketemps (car x)
                           config tempmap db)))
      (aig2c-maketemps-list (cdr x)
                            config tempmap db))))

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

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

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

(defthm string-listp-of-alist-vals-of-aig2c-maketemps-list
  (b* (((mv new-map ?new-db)
        (aig2c-maketemps-list 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-list-monotonic

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