• Top
  • Documentation
  • Books
  • Boolean-reasoning
    • Ipasir
    • Aignet
    • Aig
    • Satlink
    • Truth
    • Ubdds
      • Equal-by-eval-bdds
      • Ubdd-constructors
        • Q-and
        • Q-ite
        • Q-or
        • Q-implies
        • Q-iff
        • Q-and-c2
        • Q-and-c1
        • Q-or-c2
        • Q-not
        • Q-ite-fn
        • Q-xor
        • Cheap-and-expensive-arguments
        • Q-and-is-nil
        • Q-compose-list
        • Qv
        • Q-compose
        • Q-and-is-nilc2
        • Q-nor
        • Q-nand
      • Eval-bdd
      • Ubddp
      • Ubdd-fix
      • Q-sat
      • Bdd-sat-dfs
      • Eval-bdd-list
      • Qcdr
      • Qcar
      • Q-sat-any
      • Canonicalize-to-q-ite
      • Ubdd-listp
      • Qcons
    • Bdd
    • Faig
    • Bed
    • 4v
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Ubdd-constructors

Q-xor

(q-xor a b &rest args) constructs a UBDD representing the exclusive OR of its arguments.

Definitions and Theorems

Function: q-binary-xor

(defun q-binary-xor (x y)
  (declare (xargs :guard t))
  (cond ((atom x) (if x (q-not y) y))
        ((atom y) (if y (q-not x) x))
        ((hons-equal x y) nil)
        (t (qcons (q-binary-xor (car x) (car y))
                  (q-binary-xor (cdr x) (cdr y))))))

Function: q-binary-xor-memoize-condition

(defun q-binary-xor-memoize-condition (x y)
  (declare (ignorable x y)
           (xargs :guard 't))
  (and (consp x) (consp y)))

Function: q-xor-macro-fn

(defun q-xor-macro-fn (args)
  (declare (xargs :guard (consp args)))
  (if (atom (cdr args))
      (car args)
    (cons 'prog2$
          (cons '(last-chance-wash-memory)
                (cons (cons 'q-binary-xor
                            (cons (car args)
                                  (cons (q-xor-macro-fn (cdr args))
                                        'nil)))
                      'nil)))))

Theorem: ubddp-of-q-xor

(defthm ubddp-of-q-xor
  (implies (and (force (ubddp x))
                (force (ubddp y)))
           (equal (ubddp (q-xor x y)) t)))

Theorem: eval-bdd-of-q-xor

(defthm eval-bdd-of-q-xor
  (equal (eval-bdd (q-xor x y) values)
         (if (eval-bdd x values)
             (not (eval-bdd y values))
           (eval-bdd y values))))

Theorem: q-xor-of-self

(defthm q-xor-of-self
  (equal (q-xor x x) nil))

Theorem: canonicalize-q-xor

(defthm canonicalize-q-xor
  (implies (and (force (ubddp x))
                (force (ubddp y)))
           (equal (q-xor x y)
                  (q-ite x (q-not y) y))))