(aig-vars x) returns the variables of the AIG
(aig-vars x) → vars
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.
The variable collection strategy used by
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.
(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))))))
(defthm aig-var-listp-aig-vars (aig-var-listp (aig-vars x)))
(defthm true-listp-aig-vars (true-listp (aig-vars x)) :rule-classes :type-prescription)
(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)))