		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.