Aig-partial-eval
(aig-partial-eval x env) evaluates x, an AIG, under the partial
environment env, producing a new AIG as a result.
- Signature
(aig-partial-eval x env) → aig
- Arguments
- x — The AIG to partially evaluate.
- env — A fast alist that (typically) binds some of the variables in x to
Boolean values.
- Returns
- aig — Modified version of x obtained by replacing bound variables with their
values and doing basic constant propagation.
In ordinary AIG evaluation with aig-eval, any variables that
are missing from env are just assumed to have a default value. Because of
this, every variable can be given a Boolean value and we can evaluate the whole
AIG to produce a Boolean result.
In partial evaluation, variables that aren't bound in env are left
alone. Because of this, the result of a partial evaluation is a typically a
reduced AIG instead of a Boolean.
Another way to do partial evaluations is with aig-restrict. In fact,
the only difference between aig-restrict and aig-partial-eval is that
aig-partial-eval Boolean-fixes the values in the alist as it looks them
up. This has logically nice properties, e.g., since we never replace a
variable by a subtree, only by a Boolean, we know unconditionally that the
variables of the resulting AIG are a subset of the variables of the
original.
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-partial-eval
(defun aig-partial-eval (x env)
(declare (xargs :guard t))
(let ((__function__ 'aig-partial-eval))
(declare (ignorable __function__))
(aig-cases x :true t :false nil :var
(let ((a (hons-get x env)))
(if a (and (cdr a) t) x))
:inv
(aig-not (aig-partial-eval (car x) env))
:and
(let ((a (aig-partial-eval (car x) env)))
(and a
(aig-and a (aig-partial-eval (cdr x) env)))))))
Function: aig-partial-eval-memoize-condition
(defun aig-partial-eval-memoize-condition (x env)
(declare (ignorable x env)
(xargs :guard 't))
(and (consp x) (cdr x)))
Subtopics
- Aig-partial-eval-thms
- Basic theorems about aig-partial-eval.
