		Search-engine friendly clone of the ACL2 documentation.

Aig-and

Aig-and-dumb

(aig-and-dumb x y) is a simpler alternative to aig-and.

Signature
(aig-and-dumb x y) → aig

This does far fewer reductions than aig-and. We fold constants and collapse x & x and x & ~x, but that's it.

Definitions and Theorems

Function: aig-and-dumb

(defun aig-and-dumb (x y)
  (declare (xargs :guard t))
  (let ((__function__ 'aig-and-dumb))
    (declare (ignorable __function__))
    (cond ((or (eq x nil) (eq y nil)) nil)
          ((eq x t) y)
          ((eq y t) x)
          ((hons-equal x y) x)
          ((aig-negation-p x y) nil)
          (t (hons x y)))))

Theorem: aig-eval-of-aig-and-dumb

(defthm aig-eval-of-aig-and-dumb
  (equal (aig-eval (aig-and-dumb x y) env)
         (and (aig-eval x env)
              (aig-eval y env))))

Theorem: aig-and-dumb-of-constants

(defthm aig-and-dumb-of-constants
  (and (equal (aig-and-dumb nil x) nil)
       (equal (aig-and-dumb x nil) nil)
       (equal (aig-and-dumb x t) x)
       (equal (aig-and-dumb t x) x)))