Aig-restrict
(aig-restrict x sigma) performs variable substitution throughout the
AIG x, replacing any variables bound in sigma with their
corresponding values.
- Signature
(aig-restrict x sigma) → aig
- Arguments
- x — The AIG to restrict.
- sigma — A fast alist binding variables to replacement AIGs.
- Returns
- aig — Modified version of x where all variables bound in sigma are
replaced, and any unmentioned variables are left unchanged.
The name sigma is intended to evoke the notion of substitution
lists in logic. Any variables that are not mentioned in sigma are left
unchanged. When all of the variables in x are bound in sigma, and
all of the values are Boolean, this is equivalent to aig-eval.
This function is memoized. You should typically free its memo table
after you are done with whatever sigma you are using, to avoid excessive
memory usage. (We don't use :forget t because you often want to restrict
several related AIGs.)
Definitions and Theorems
Function: aig-restrict
(defun aig-restrict (x sigma)
(declare (xargs :guard t))
(let ((__function__ 'aig-restrict))
(declare (ignorable __function__))
(aig-cases x :true t :false nil :var
(let ((a (hons-get x sigma)))
(if a (cdr a) x))
:inv
(aig-not (aig-restrict (car x) sigma))
:and
(let ((a (aig-restrict (car x) sigma)))
(and a
(aig-and a (aig-restrict (cdr x) sigma)))))))
Function: aig-restrict-memoize-condition
(defun aig-restrict-memoize-condition (x sigma)
(declare (ignorable x sigma)
(xargs :guard 't))
(and (consp x) (cdr x)))
Theorem: aig-eval-of-aig-restrict
(defthm aig-eval-of-aig-restrict
(equal (aig-eval (aig-restrict x al1) al2)
(aig-eval x
(append (aig-eval-alist al1 al2) al2))))
Subtopics
- Aig-restrict-thms
- Basic theorems about aig-restrict.
