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.