		Search-engine friendly clone of the ACL2 documentation.

Aig-semantics

Aig-eval-alist

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

Signature
(aig-eval-alist x env) → vals-alist
Arguments: x — The AIG alist to evaluate. This does not need to be a fast alist.; env — The environment to use; see aig-eval.
Returns: vals-alist — An ordinary (slow) alist that binds the same keys to the values of their associated AIGs.

Definitions and Theorems

Function: aig-eval-alist

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

Theorem: hons-assoc-equal-aig-eval-alist

(defthm hons-assoc-equal-aig-eval-alist
        (equal (hons-assoc-equal key (aig-eval-alist x env))
               (and (hons-assoc-equal key x)
                    (cons key
                          (aig-eval (cdr (hons-assoc-equal key x))
                                    env)))))

Subtopics

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