• 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-main

Create the assignments for a single AIG.

Signature

(aig2c-main x seen tempmap config code) → (mv new-code seen)

Arguments

x — The AIG we are compiling.

seen — Fast alist mapping AIG nodes we've already compiled to T.

tempmap — Fast alist mapping every AIG node to its C variable name.
    Guard (string-listp (alist-vals tempmap)).

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

code — The C code fragment we are building, a character list in reverse order (e.g., for use with str::revappend-chars).
    Guard (character-listp code).

Returns

new-code — Type (character-listp new-code), given (force (character-listp code)).

Definitions and Theorems

Function: aig2c-main

(defun aig2c-main (x seen tempmap config code)
 (declare (xargs :guard (and (string-listp (alist-vals tempmap))
                             (aig2c-config-p config)
                             (character-listp code))))
 (let ((__function__ 'aig2c-main))
   (declare (ignorable __function__))
   (b*
    ((name (cdr (hons-get x tempmap)))
     ((unless name)
      (raise "AIG node isn't bound!")
      (mv code seen))
     ((when (atom x)) (mv code seen))
     ((when (hons-get x seen))
      (mv code seen))
     (seen (hons-acons x t seen))
     ((mv code seen)
      (aig2c-main (car x)
                  seen tempmap config code))
     ((mv code seen)
      (if (cdr x)
          (aig2c-main (cdr x)
                      seen tempmap config code)
        (mv code seen)))
     (code (list* #\Space #\Space code))
     (code (str::revappend-chars (aig2c-config->type config)
                                 code))
     (code (cons #\Space code))
     (code (str::revappend-chars name code))
     (code (list* #\Space #\= #\Space code))
     (car-name (cdr (hons-get (car x) tempmap)))
     ((unless car-name)
      (raise "AIG node for CAR isn't bound!")
      (mv code seen))
     ((unless (cdr x))
      (b* ((code (str::revappend-chars (aig2c-config->op-not config)
                                       code))
           (code (str::revappend-chars car-name code))
           (code (list* #\Newline #\; code)))
        (mv code seen)))
     (cdr-name (cdr (hons-get (cdr x) tempmap)))
     ((unless cdr-name)
      (raise "AIG node for CDR isn't bound!")
      (mv code seen))
     (code (str::revappend-chars car-name code))
     (code (cons #\Space code))
     (code (str::revappend-chars (aig2c-config->op-and config)
                                 code))
     (code (cons #\Space code))
     (code (str::revappend-chars cdr-name code))
     (code (list* #\Newline #\; code)))
    (mv code seen))))

Theorem: character-listp-of-aig2c-main.new-code

(defthm character-listp-of-aig2c-main.new-code
  (implies (force (character-listp code))
           (b* (((mv ?new-code ?seen)
                 (aig2c-main x seen tempmap config code)))
             (character-listp new-code)))
  :rule-classes :rewrite)