		Search-engine friendly clone of the ACL2 documentation.

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.