• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
    • Ipasir
    • Aignet
    • Aig
      • Aig-constructors
      • Aig-vars
      • Aig-sat
      • Bddify
      • Aig-substitution
        • Aig-partial-eval
        • Aig-restrict
        • Aig-compose
        • Aig-restrict-alist
        • Aig-partial-eval-alist
        • Aig-compose-alist
          • Aig-compose-alist-thms
        • Aig-restrict-alists
        • Aig-compose-alists
        • Aig-restrict-list
        • Aig-partial-eval-list
        • Aig-compose-list
      • Aig-other
      • 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
  • Testing-utilities
  • Math

• Aig-substitution

Aig-compose-alist

(aig-compose-alist x sigma) composes into an AIG Alist (an alist binding keys to AIGs).

Signature

(aig-compose-alist x sigma) → aig-alist

Arguments

x — Alist binding names to AIGs. This doesn't need to be a fast alist.

sigma — Fast alist binding variables to replacement AIGs, as in aig-compose.

Returns

aig-alist — Ordinary (slow) alist with the same keys as x, and values formed by restricting each aig with aig-compose.

Definitions and Theorems

Function: aig-compose-alist

(defun aig-compose-alist (x sigma)
       (declare (xargs :guard t))
       (let ((__function__ 'aig-compose-alist))
            (declare (ignorable __function__))
            (cond ((atom x) nil)
                  ((atom (car x))
                   (aig-compose-alist (cdr x) sigma))
                  (t (cons (cons (caar x)
                                 (aig-compose (cdar x) sigma))
                           (aig-compose-alist (cdr x) sigma))))))

Subtopics

Aig-compose-alist-thms

Basic theorems about aig-compose-alist.