		Search-engine friendly clone of the ACL2 documentation.

Aig-eval

Aig-env-lookup

Look up the value of an AIG variable in an environment.

Signature
(aig-env-lookup x env) → *
Arguments: x — Variable to look up.; env — Fast alist mapping variables to values.

Unbound variables are given the default value t instead of nil because this makes theorems about faig evaluation work out more nicely (it makes unbound FAIG variables evaluate to X).

Definitions and Theorems

Function: aig-env-lookup

(defun
 aig-env-lookup (x env)
 (declare (xargs :guard t))
 (let
   ((__function__ 'aig-env-lookup))
   (declare (ignorable __function__))
   (let ((look (hons-get x env)))
        (if look (and (cdr look) t)
            (mbe :logic t
                 :exec (if *aig-env-lookup-warn-missing-binding*
                           (prog2$ (aig-env-lookup-missing-output x)
                                   t)
                           t))))))