		Search-engine friendly clone of the ACL2 documentation.

Parametrize

Ubdd-apply-gate

Signature
(ubdd-apply-gate xor f0-ubdd f1-ubdd) → gate
Arguments: f0-ubdd — Guard (acl2::ubddp f0-ubdd).; f1-ubdd — Guard (acl2::ubddp f1-ubdd).
Returns: gate — Type (acl2::ubddp gate).

Definitions and Theorems

Function: ubdd-apply-gate

(defun ubdd-apply-gate (xor f0-ubdd f1-ubdd)
  (declare (xargs :guard (and (acl2::ubddp f0-ubdd)
                              (acl2::ubddp f1-ubdd))))
  (let ((__function__ 'ubdd-apply-gate))
    (declare (ignorable __function__))
    (if xor (acl2::q-xor (lubdd-fix f0-ubdd)
                         (lubdd-fix f1-ubdd))
      (acl2::q-and (lubdd-fix f0-ubdd)
                   (lubdd-fix f1-ubdd)))))

Theorem: ubddp-of-ubdd-apply-gate

(defthm ubddp-of-ubdd-apply-gate
  (b* ((gate (ubdd-apply-gate xor f0-ubdd f1-ubdd)))
    (acl2::ubddp gate))
  :rule-classes :rewrite)

Theorem: eval-of-ubdd-apply-gate

(defthm eval-of-ubdd-apply-gate
 (b* ((?gate (ubdd-apply-gate xor f0-ubdd f1-ubdd)))
  (equal
     (acl2::eval-bdd gate env)
     (bit->bool (let ((f0 (bool->bit (acl2::eval-bdd f0-ubdd env)))
                      (f1 (bool->bit (acl2::eval-bdd f1-ubdd env))))
                  (b-ite (bool->bit xor)
                         (b-xor f0 f1)
                         (b-and f0 f1)))))))