		Search-engine friendly clone of the ACL2 documentation.

Aig-substitution

Aig-partial-eval-alist

(aig-partial-eval-alist x env) partially evaluates an AIG Alist (an alist binding keys to AIGs).

Signature
(aig-partial-eval-alist x env) → aig-alist
Arguments: x — Alist binding names to AIGs. This doesn't need to be a fast alist.; env — Fast alist binding variables to Booleans, as in aig-partial-eval.
Returns: aig-alist — Ordinary (slow) alist with the same keys as x, and values formed by restricting each aig with aig-partial-eval.

Definitions and Theorems

Function: aig-partial-eval-alist

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

Theorem: alistp-of-aig-partial-eval-alist

(defthm alistp-of-aig-partial-eval-alist
  (alistp (aig-partial-eval-alist x env)))

Subtopics

Aig-partial-eval-alist-thms: Basic theorems about aig-partial-eval-alist.