Aig-compose
(aig-compose x sigma) performs variable substitution throughout the AIG
x, unconditionally replacing every variable in x with its
binding in sigma.
- Signature
(aig-compose x sigma) → aig
- Arguments
- x — The AIG to compose into.
- sigma — A fast alist that should bind variables to replacement AIGs.
- Returns
- aig — Modified version of x where every variable is replaced with its
binding in sigma or t if it has no binding.
The name sigma is intended to evoke the notion of substitution
lists in logic. This operation is similar to aig-restrict, except that
whereas aig-restrict leaves unbound variables alone, aig-compose
replaces them with t. This has the logically nice property that the
variables after composition are just the variables in the AIGs of
sigma.
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 compose
several related AIGs.)
Definitions and Theorems
Function: aig-compose
(defun aig-compose (x sigma)
(declare (xargs :guard t))
(let ((__function__ 'aig-compose))
(declare (ignorable __function__))
(aig-cases x :true t :false
nil :var (aig-alist-lookup x sigma)
:inv
(aig-not (aig-compose (car x) sigma))
:and
(let ((a (aig-compose (car x) sigma)))
(and a
(aig-and a (aig-compose (cdr x) sigma)))))))
Function: aig-compose-memoize-condition
(defun aig-compose-memoize-condition (x sigma)
(declare (ignorable x sigma)
(xargs :guard 't))
(and (consp x) (cdr x)))
Subtopics
- Aig-compose-thms
- Basic theorems about aig-compose.
