(aig-vars x) returns the variables of the AIG X.
(aig-vars x) → vars
- vars — An ordered set of AIG variables (atoms).
Note: variable collection can be surprisingly tricky to do
efficiently. For a good background discussion that describes various
approaches to the problem and ways to avoid needing to collect variables, see
aig-vars is a slow but simple way to collect the variables that occur
within an AIG, and we adopt it as our normal form for talking about the
variables of an AIG. That is, when we introduce other, faster algorithms for
collecting variables, we always relate them back to aig-vars.
The variable collection strategy used by aig-vars is to memoize the
whole computation; this implicitly records, for every AND node, the exact set
of variables that are found under that node. We use ordinary std/osets
as our variable set representation so that merging these sets is linear at each
node. The overall complexity is then O(n^2) in the size of the AIG.
This approach records the full variable information for every AND node
throughout the AIG. This takes a lot of memory, and often you do not need
nearly this much information. In practice, functions like aig-vars-1pass are often much more practical.
Definitions and Theorems
(defun aig-vars (x)
(declare (xargs :guard t))
(let ((__function__ 'aig-vars))
(declare (ignorable __function__))
:var (mbe :logic (set::insert x nil)
:exec (hons x nil))
:inv (aig-vars (car x))
:and (set::union (aig-vars (car x))
(aig-vars (cdr x))))))
(aig-var-listp (aig-vars x)))
(true-listp (aig-vars x))
(defthm setp-aig-vars (set::setp (aig-vars x)))
(defun aig-vars-memoize-condition (x)
(declare (ignorable x)
(xargs :guard 't))
(and (consp x) (cdr x)))
- Theorems about aig-vars from centaur/aig/aig-vars.
- Faster, raw Lisp implementation of aig-vars.
- Faster, raw Lisp implementation of aig-vars, with
under-the-hood memoization; kind of nasty.