# Aig-vars

`(aig-vars x)` returns the variables of the AIG X.

- Signature
(aig-vars x) → vars

- Returns
`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
4v-sexpr-vars.

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

**Function: **aig-vars

(defun aig-vars (x)
(declare (xargs :guard t))
(let ((__function__ 'aig-vars))
(declare (ignorable __function__))
(aig-cases x
:true nil
:false nil
: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))))))

**Theorem: **aig-var-listp-aig-vars

(defthm aig-var-listp-aig-vars
(aig-var-listp (aig-vars x)))

**Theorem: **true-listp-aig-vars

(defthm true-listp-aig-vars
(true-listp (aig-vars x))
:rule-classes :type-prescription)

**Theorem: **setp-aig-vars

(defthm setp-aig-vars
(set::setp (aig-vars x)))

**Function: **aig-vars-memoize-condition

(defun aig-vars-memoize-condition (x)
(declare (ignorable x)
(xargs :guard 't))
(and (consp x) (cdr x)))

### Subtopics

- Aig-vars-thms
- Theorems about aig-vars from centaur/aig/aig-vars.
- Aig-vars-1pass
- Faster, raw Lisp implementation of aig-vars.
- Aig-vars-fast
- Faster, raw Lisp implementation of aig-vars, with
under-the-hood memoization; kind of nasty.