		Search-engine friendly clone of the ACL2 documentation.

Aig-other

Aig-print

Convert an AIG into an ACL2-like S-expression.

Signature
(aig-print x) → sexpr
Arguments: x — An AIG.
Returns: sexpr — A s-expression with AND and NOT calls.

We generally don't imagine using this for anything other than one-off debugging. Note that the S-expressions you generate this way can easily be too large to print.

Definitions and Theorems

Function: aig-print

(defun
 aig-print (x)
 (declare (xargs :guard t))
 (let
  ((__function__ 'aig-print))
  (declare (ignorable __function__))
  (aig-cases
      x
      :true t
      :false nil
      :var x
      :inv (cons 'not
                 (cons (aig-print (car x)) 'nil))
      :and (let* ((a (aig-print (car x)))
                  (d (aig-print (cdr x))))
                 (cons 'and
                       (append (if (and (consp a) (eq (car a) 'and))
                                   (cdr a)
                                   (list a))
                               (if (and (consp d) (eq (car d) 'and))
                                   (cdr d)
                                   (list d))))))))

Function: aig-print-memoize-condition

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