		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))))))