		Search-engine friendly clone of the ACL2 documentation.

Aig-constructors

Aig-not

(aig-not x) constructs an AIG representing (not x).

Signature
(aig-not x) → aig

This could be implemented as (hons x nil), but we at least take care to fold constants and avoid creating double negatives.

Definitions and Theorems

Function: aig-not

(defun aig-not (x)
       (declare (xargs :guard t))
       (let ((__function__ 'aig-not))
            (declare (ignorable __function__))
            (cond ((eq x nil) t)
                  ((eq x t) nil)
                  ((and (not (aig-atom-p x))
                        (eq (cdr x) nil))
                   (car x))
                  (t (hons x nil)))))

Theorem: aig-eval-not

(defthm aig-eval-not
        (equal (aig-eval (aig-not x) env)
               (not (aig-eval x env))))