		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))))