Aig-eval
(aig-eval x env) gives the semantics of aigs: it gives the
Boolean value of the AIG x under the environment env.
- Signature
(aig-eval x env) → *
- Arguments
- x — The AIG to evaluate.
- env — A fast alist that binds variables to values. Typically it should bind
every variable in x to some Boolean value. When this isn't the case,
variables are assigned the default value t; see aig-env-lookup.
This function is memoized. You should typically free its
memo table after you are done with whatever env you are using, to avoid
excessive memory usage. (We don't use :forget t because you often want to
evaluate several related AIGs.)
Definitions and Theorems
Function: aig-eval
(defun aig-eval (x env)
(declare (xargs :guard t))
(let ((__function__ 'aig-eval))
(declare (ignorable __function__))
(aig-cases x
:true t
:false nil
:var (aig-env-lookup x env)
:inv (not (aig-eval (car x) env))
:and (and (aig-eval (car x) env)
(aig-eval (cdr x) env)))))
Function: aig-eval-memoize-condition
(defun aig-eval-memoize-condition (x env)
(declare (ignorable x env)
(xargs :guard 't))
(and (consp x) (cdr x)))
Subtopics
- Aig-env-lookup-missing-action
- Configurable warnings about missing variables in AIG evaluation.
- Aig-env-lookup
- Look up the value of an AIG variable in an environment.
- Aig-alist-lookup
- Look up the value of an AIG variable in an environment.
- Aig-eval-thms
- Basic theorems about aig-eval.
- Aig-env-lookup-missing-output
- Stub for warnings about missing variables in AIG evaluation.
