		Search-engine friendly clone of the ACL2 documentation.

Aig-eval

Aig-env-lookup-missing-action

Configurable warnings about missing variables in AIG evaluation.

Ordinarily aig-eval treats any variables that are not bound in the environment as having value t. But a missing bindings could be the result of a bug in your program, so by default aig-eval is set up to print a warning if this happens.

(aig-env-lookup-missing-action val) allows you to control whether these warnings are printed, and also whether break$ should be called. The valid actions are:

nil, silently bind the variable to t,
:warn (the default), print a warning but do not break$, and
:break, to print the warning and then call break$.

Definitions and Theorems

Function: aig-env-lookup-missing-quiet

(defun aig-env-lookup-missing-quiet (name)
       (declare (xargs :guard t) (ignore name))
       nil)

Function: aig-env-lookup-missing-complain

(defun
 aig-env-lookup-missing-complain (name)
 (declare (xargs :guard t))
 (and
  *aig-env-lookup-warn-missing-binding*
  (cw
   "WARNING: Missing variable binding ~x0 in AIG-ENV-LOOKUP; ~
              assigning T~%"
   name)))

Function: aig-env-lookup-missing-break

(defun
 aig-env-lookup-missing-break (name)
 (declare (xargs :guard t))
 (and
  *aig-env-lookup-warn-missing-binding*
  (prog2$
   (cw
    "WARNING: Missing variable binding ~x0 in ~x1; assigning ~
                      T. To avoid this break, run ~x2, where action is NIL or ~
                      :WARN.~%"
    name 'aig-env-lookup
    '(aig-env-lookup-missing-action action))
   (break$))))