		Search-engine friendly clone of the ACL2 documentation.

Aig-constructors

Aig-xor

(aig-xor x y) constructs an AIG representing (xor x y).

Signature
(aig-xor x y) → aig

Definitions and Theorems

Function: aig-xor

(defun aig-xor (x y)
  (declare (xargs :guard t))
  (let ((__function__ 'aig-xor))
    (declare (ignorable __function__))
    (aig-or (aig-and x (aig-not y))
            (aig-and y (aig-not x)))))

Theorem: aig-eval-xor

(defthm aig-eval-xor
  (equal (aig-eval (aig-xor x y) env)
         (xor (aig-eval x env)
              (aig-eval y env))))