Faig-restrict
(faig-restrict x sigma) performs variable substitution throughout the
FAIG x, replacing any variables bound in sigma with their
corresponding values.
- Signature
(faig-restrict x sigma) → *
See aig-restrict; the env should be a fast alist and
you will want to clear the memoize table for aig-restrict when you are
done using the env.
Definitions and Theorems
Function: faig-restrict
(defun faig-restrict (x sigma)
(declare (xargs :guard t))
(let ((__function__ 'faig-restrict))
(declare (ignorable __function__))
(if (atom x)
'(t . t)
(cons (aig-restrict (car x) sigma)
(aig-restrict (cdr x) sigma)))))
Subtopics
- Faig-restrict-thms
- Basic theorems about faig-restrict.
- Faig-restrict-alist
- (faig-restrict-alist x sigma) substitutes into an FAIG alist (an alist
binding keys to FAIGs).
- Faig-restrict-alists
- (faig-restrict-alists x sigma) substitutes into a list of FAIG alists.
