		Search-engine friendly clone of the ACL2 documentation.

Aig-and

Aig-binary-and

(aig-binary-and x y) constructs an AIG representing (and x y).

Signature
(aig-binary-and x y) → *

Definitions and Theorems

Function: aig-binary-and

(defun aig-binary-and (x y)
  (declare (xargs :guard t))
  (let ((__function__ 'aig-binary-and))
    (declare (ignorable __function__))
    (b* (((mv status arg1 arg2)
          (aig-and-main x y))
         ((when (eq status :subterm)) arg1)
         ((when (eq status :reduced))
          (aig-binary-and arg1 arg2)))
      (hons arg1 arg2))))

Theorem: aig-and-constants

(defthm aig-and-constants
  (and (equal (aig-binary-and nil x) nil)
       (equal (aig-binary-and x nil) nil)
       (equal (aig-binary-and x t) x)
       (equal (aig-binary-and t x) x)))

Theorem: aig-eval-and

(defthm aig-eval-and
  (equal (aig-eval (aig-binary-and x y) env)
         (and (aig-eval x env)
              (aig-eval y env))))