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

Create the assignments for AIG constant and variable nodes.

Signature

(aig2c-prologue input-init tempmap config code) → new-code

Arguments

input-init — Mapping from every AIG variable to a C code fragment that should be used to initialize it.
    Guard (string-listp (alist-vals input-init)).

tempmap — Fast alist mapping every AIG variable (and other nodes) to the temporary variable name to use.
    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-prologue

(defun aig2c-prologue (input-init tempmap config code)
  (declare (xargs :guard (and (string-listp (alist-vals input-init))
                              (string-listp (alist-vals tempmap))
                              (aig2c-config-p config)
                              (character-listp code))))
  (let ((__function__ 'aig2c-prologue))
    (declare (ignorable __function__))
    (b* (((when (atom input-init)) code)
         ((when (atom (car input-init)))
          (aig2c-prologue (cdr input-init)
                          tempmap config code))
         (var (caar input-init))
         (c-rhs (cdar input-init))
         (c-lhs (cdr (hons-get var tempmap)))
         ((unless c-lhs)
          (aig2c-prologue (cdr input-init)
                          tempmap config code))
         (code (str::revappend-chars "  " code))
         (code (str::revappend-chars (aig2c-config->type config)
                                     code))
         (code (str::revappend-chars " " code))
         (code (str::revappend-chars c-lhs code))
         (code (str::revappend-chars " = " code))
         (code (str::revappend-chars c-rhs code))
         (code (list* #\Newline #\; code)))
      (aig2c-prologue (cdr input-init)
                      tempmap config code))))

Theorem: character-listp-of-aig2c-prologue

(defthm character-listp-of-aig2c-prologue
 (implies
    (force (character-listp code))
    (b* ((new-code (aig2c-prologue input-init tempmap config code)))
      (character-listp new-code)))
 :rule-classes :rewrite)