Filtering...

extra-operations

books/centaur/ubdds/extra-operations

Included Books

core
other
(in-package "ACL2")
include-book
(include-book "core")
local
(local (defun q-binop-induct
    (x y vals)
    (declare (xargs :verify-guards nil))
    (if (atom x)
      (list x y vals)
      (if (atom y)
        nil
        (if (car vals)
          (q-binop-induct (car x) (car y) (cdr vals))
          (q-binop-induct (cdr x) (cdr y) (cdr vals)))))))
other
(defsection cheap-and-expensive-arguments
  :parents (ubdd-constructors)
  :short "Sort arguments into those that we think are definitely cheap to evaluate
versus those that may be expensive."
  :long "<p>This is the same idea as in @(see q-ite).  Variables and quoted
constants are cheap to evaluate, so in associative/commutative operations like
@(see q-and) we prefer to evaluate them first.</p>"
  (defun cheap-and-expensive-arguments-aux
    (x cheap expensive)
    (declare (xargs :mode :program))
    (if (atom x)
      (mv cheap expensive)
      (if (or (quotep (car x)) (atom (car x)))
        (cheap-and-expensive-arguments-aux (cdr x)
          (cons (car x) cheap)
          expensive)
        (cheap-and-expensive-arguments-aux (cdr x)
          cheap
          (cons (car x) expensive)))))
  (defun cheap-and-expensive-arguments
    (x)
    (declare (xargs :mode :program))
    (mv-let (cheap expensive)
      (cheap-and-expensive-arguments-aux x nil nil)
      (mv (reverse cheap) (reverse expensive)))))
other
(defsection q-and
  :parents (ubdd-constructors)
  :short "@(call q-and) constructs a UBDD representing the conjunction of its
arguments."
  :long "<p>In the logic,</p>

@({
 (Q-AND)        = T
 (Q-AND X)      = X
 (Q-AND X Y)   = (Q-BINARY-AND X Y)
 (Q-AND X Y Z) = (Q-BINARY-AND X (Q-BINARY-AND Y Z))
 ... etc ...
})

<p>But as a special optimization, in the execution, when there is more than one
argument, we can sometimes "short-circuit" the computation and avoid
evaluating some arguments.  In particular, we classify the arguments as cheap
or expensive using @(see cheap-and-expensive-arguments).  We then arrange
things so that the cheap arguments are considered first.  If any cheap argument
is @('nil'), we can stop before any expensive arguments even need to be
computed.</p>"
  (defund q-binary-and
    (x y)
    (declare (xargs :guard t))
    (cond ((atom x) (if x
          (if (atom y)
            (if y
              t
              nil)
            y)
          nil))
      ((atom y) (if y
          x
          nil))
      ((hons-equal x y) x)
      (t (qcons (q-binary-and (car x) (car y))
          (q-binary-and (cdr x) (cdr y))))))
  (add-bdd-fn q-binary-and)
  (defun q-and-macro-logic-part
    (args)
    (declare (xargs :mode :program))
    (cond ((atom args) t)
      ((atom (cdr args)) (car args))
      (t `(q-binary-and ,(CAR ARGS)
          ,(Q-AND-MACRO-LOGIC-PART (CDR ARGS))))))
  (defun q-and-macro-exec-part
    (args)
    (declare (xargs :mode :program))
    (cond ((atom args) t)
      ((atom (cdr args)) (car args))
      (t `(let ((q-and-x-do-not-use-elsewhere ,(CAR ARGS)))
          (and q-and-x-do-not-use-elsewhere
            (prog2$ (last-chance-wash-memory)
              (q-binary-and q-and-x-do-not-use-elsewhere
                ,(Q-AND-MACRO-EXEC-PART (CDR ARGS)))))))))
  (defun q-and-macro-fn
    (args)
    (declare (xargs :mode :program))
    (cond ((atom args) t)
      ((atom (cdr args)) (car args))
      (t (mv-let (cheap expensive)
          (cheap-and-expensive-arguments args)
          (if (not expensive)
            (q-and-macro-logic-part cheap)
            (let ((reordered-args (append cheap expensive)))
              `(mbe :logic ,(Q-AND-MACRO-LOGIC-PART REORDERED-ARGS)
                :exec ,(Q-AND-MACRO-EXEC-PART REORDERED-ARGS))))))))
  (defmacro q-and (&rest args) (q-and-macro-fn args))
  (add-macro-alias q-and q-binary-and)
  (add-binop q-and q-binary-and)
  (local (in-theory (enable q-and)))
  (defthm ubddp-of-q-and
    (implies (and (force (ubddp x)) (force (ubddp y)))
      (equal (ubddp (q-and x y)) t))
    :hints (("Goal" :in-theory (enable ubddp))))
  (defthm eval-bdd-of-q-and
    (equal (eval-bdd (q-and x y) values)
      (and (eval-bdd x values) (eval-bdd y values)))
    :hints (("Goal" :in-theory (enable eval-bdd)
       :induct (q-binop-induct x y values)
       :expand (q-and x y))))
  (defthm canonicalize-q-and
    (implies (and (force (ubddp x)) (force (ubddp y)))
      (equal (q-and x y) (q-ite x y nil))))
  (add-to-ruleset canonicalize-to-q-ite '(canonicalize-q-and))
  (defthm q-and-of-nil
    (and (equal (q-and nil x) nil) (equal (q-and x nil) nil))
    :hints (("Goal" :in-theory (disable canonicalize-q-and))))
  (defthm q-and-of-t-slow
    (and (equal (q-and t x)
        (if (consp x)
          x
          (if x
            t
            nil)))
      (equal (q-and x t)
        (if (consp x)
          x
          (if x
            t
            nil))))
    :hints (("Goal" :in-theory (disable canonicalize-q-and))))
  (defthm q-and-of-t-aggressive
    (implies (force (ubddp x))
      (and (equal (q-and t x) x) (equal (q-and x t) x))))
  (defthm q-and-symmetric
    (equal (q-and x y) (q-and y x))
    :hints (("Goal" :in-theory (disable equal-by-eval-bdds canonicalize-q-and))))
  (memoize 'q-binary-and
    :condition '(and (consp x) (consp y))
    :commutative 'q-and-symmetric)
  (defthm q-and-of-self-slow
    (equal (q-and x x)
      (if (consp x)
        x
        (if x
          t
          nil))))
  (defthm q-and-of-self-aggressive
    (implies (force (ubddp x)) (equal (q-and x x) x)))
  (local (in-theory (disable q-and)))
  (local (defun test-q-and
      (a b c x y z)
      (declare (xargs :guard t
          :guard-hints (("Goal" :in-theory (disable (force))))))
      (list (q-and x y)
        (q-and x (q-not y))
        (q-and (q-not x) y)
        (q-and x y (q-not x) a b (q-ite y z c))))))
other
(defsection q-or
  :parents (ubdd-constructors)
  :short "@(call q-or) constructs a UBDD representing the disjunction of its
arguments."
  :long "<p>In the logic,</p>

@({
 (Q-OR)       = NIL
 (Q-OR X)     = X
 (Q-OR X Y)   = (Q-BINARY-OR X Y)
 (Q-OR X Y Z) = (Q-BINARY-OR X (Q-BINARY-OR Y Z))
})

<p>In the execution, we use the same sort of optimization as in @(see
q-and).</p>"
  (defund q-binary-or
    (x y)
    (declare (xargs :guard t))
    (cond ((atom x) (if x
          t
          (if (atom y)
            (if y
              t
              nil)
            y)))
      ((atom y) (if y
          t
          x))
      ((hons-equal x y) x)
      (t (let ((l (q-binary-or (car x) (car y))) (r (q-binary-or (cdr x) (cdr y))))
          (qcons l r)))))
  (add-bdd-fn q-binary-or)
  (defun q-or-macro-logic-part
    (args)
    (declare (xargs :mode :program))
    (cond ((atom args) nil)
      ((atom (cdr args)) (car args))
      (t `(q-binary-or ,(CAR ARGS)
          ,(Q-OR-MACRO-LOGIC-PART (CDR ARGS))))))
  (defun q-or-macro-exec-part
    (args)
    (declare (xargs :mode :program))
    (cond ((atom args) nil)
      ((atom (cdr args)) (car args))
      (t `(let ((q-or-x-do-not-use-elsewhere ,(CAR ARGS)))
          (if (eq t q-or-x-do-not-use-elsewhere)
            t
            (prog2$ (last-chance-wash-memory)
              (q-binary-or q-or-x-do-not-use-elsewhere
                ,(Q-OR-MACRO-EXEC-PART (CDR ARGS)))))))))
  (defun q-or-macro-fn
    (args)
    (declare (xargs :mode :program))
    (cond ((atom args) nil)
      ((atom (cdr args)) (car args))
      (t (mv-let (cheap expensive)
          (cheap-and-expensive-arguments args)
          (if (not expensive)
            (q-or-macro-logic-part cheap)
            (let ((reordered-args (append cheap expensive)))
              `(mbe :logic ,(Q-OR-MACRO-LOGIC-PART REORDERED-ARGS)
                :exec ,(Q-OR-MACRO-EXEC-PART REORDERED-ARGS))))))))
  (defmacro q-or (&rest args) (q-or-macro-fn args))
  (add-macro-alias q-or q-binary-or)
  (add-binop q-or q-binary-or)
  (local (in-theory (enable q-or)))
  (defthm ubddp-of-q-or
    (implies (and (force (ubddp x)) (force (ubddp y)))
      (equal (ubddp (q-or x y)) t))
    :hints (("Goal" :in-theory (enable ubddp))))
  (defthm eval-bdd-of-q-or
    (equal (eval-bdd (q-or x y) values)
      (or (eval-bdd x values) (eval-bdd y values)))
    :hints (("Goal" :in-theory (enable eval-bdd)
       :induct (q-binop-induct x y values)
       :expand (q-or x y))))
  (defthm canonicalize-q-or
    (implies (and (force (ubddp x)) (force (ubddp y)))
      (equal (q-or x y) (q-ite x t y))))
  (add-to-ruleset canonicalize-to-q-ite '(canonicalize-q-or))
  (defthm q-or-of-nil-slow
    (and (equal (q-or nil x)
        (if (consp x)
          x
          (if x
            t
            nil)))
      (equal (q-or x nil)
        (if (consp x)
          x
          (if x
            t
            nil)))))
  (defthm q-or-of-nil-aggressive
    (implies (force (ubddp x))
      (and (equal (q-or nil x) x) (equal (q-or x nil) x))))
  (defthm q-or-of-t
    (and (equal (q-or t x) t) (equal (q-or x t) t))
    :hints (("Goal" :in-theory (disable canonicalize-q-or))))
  (defthm q-or-symmetric
    (equal (q-or x y) (q-or y x))
    :hints (("Goal" :in-theory (disable canonicalize-q-or
         q-or-of-nil-aggressive
         equal-by-eval-bdds))))
  (memoize 'q-binary-or
    :condition '(and (consp x) (consp y))
    :commutative 'q-or-symmetric)
  (defthm q-or-of-self-slow
    (equal (q-or x x)
      (if (consp x)
        x
        (if x
          t
          nil))))
  (defthm q-or-of-self-aggressive
    (implies (force (ubddp x)) (equal (q-or x x) x)))
  (local (in-theory (disable q-or)))
  (local (defun test-q-or
      (a b c x y z)
      (declare (xargs :guard t))
      (list (q-or x y)
        (q-or x (q-not y))
        (q-or (q-not x) y)
        (q-or x y (q-not x) a b (q-ite y z c))))))
other
(defsection q-implies
  :parents (ubdd-constructors)
  :short "@(call q-implies) constructs a UBDD representing @('(implies x y)')."
  (defund q-implies-fn
    (x y)
    (declare (xargs :guard t))
    (cond ((atom x) (if x
          (if (atom y)
            (if y
              t
              nil)
            y)
          t))
      ((atom y) (if y
          t
          (q-not x)))
      ((hons-equal x y) t)
      (t (qcons (q-implies-fn (car x) (car y))
          (q-implies-fn (cdr x) (cdr y))))))
  (memoize 'q-implies-fn
    :condition '(and (consp x) (consp y)))
  (add-bdd-fn q-implies-fn)
  (defun q-implies-macro-fn
    (x y)
    (declare (xargs :mode :program))
    (cond ((and (or (quotep x) (atom x)) (or (quotep y) (atom y))) `(q-implies-fn ,X ,Y))
      ((or (quotep y) (atom y)) `(mbe :logic (q-implies-fn ,X ,Y)
          :exec (let ((q-implies-y-do-not-use-elsewhere ,Y))
            (if (eq t q-implies-y-do-not-use-elsewhere)
              t
              (prog2$ (last-chance-wash-memory)
                (q-implies-fn ,X q-implies-y-do-not-use-elsewhere))))))
      (t `(mbe :logic (q-implies-fn ,X ,Y)
          :exec (let ((q-implies-x-do-not-use-elsewhere ,X))
            (if (not q-implies-x-do-not-use-elsewhere)
              t
              (prog2$ (last-chance-wash-memory)
                (q-implies-fn q-implies-x-do-not-use-elsewhere ,Y))))))))
  (defmacro q-implies (x y) (q-implies-macro-fn x y))
  (add-macro-alias q-implies q-implies-fn)
  (local (in-theory (enable q-implies)))
  (defthm ubddp-of-q-implies
    (implies (and (force (ubddp x)) (force (ubddp y)))
      (equal (ubddp (q-implies x y)) t))
    :hints (("Goal" :in-theory (e/d (ubddp) (canonicalize-q-not)))))
  (defthm eval-bdd-of-q-implies
    (equal (eval-bdd (q-implies x y) values)
      (implies (eval-bdd x values) (eval-bdd y values)))
    :hints (("Goal" :in-theory (e/d (eval-bdd) (canonicalize-q-not))
       :induct (q-binop-induct x y values)
       :expand (q-implies x y))))
  (defthm canonicalize-q-implies
    (implies (and (force (ubddp x)) (force (ubddp y)))
      (equal (q-implies x y) (q-ite x y t))))
  (add-to-ruleset canonicalize-to-q-ite
    '(canonicalize-q-implies))
  (defthm q-implies-of-nil
    (and (equal (q-implies nil x) t)
      (equal (q-implies x nil) (q-not x)))
    :hints (("Goal" :in-theory (e/d (q-not) (canonicalize-q-not canonicalize-q-implies)))))
  (defthm q-implies-of-t-left-slow
    (equal (q-implies t x)
      (if (consp x)
        x
        (if x
          t
          nil)))
    :hints (("Goal" :in-theory (disable canonicalize-q-implies))))
  (defthm q-implies-of-t-left-aggressive
    (implies (force (ubddp x)) (equal (q-implies t x) x))
    :hints (("Goal" :in-theory (disable canonicalize-q-implies))))
  (defthm q-implies-of-t-right
    (equal (q-implies x t) t)
    :hints (("Goal" :in-theory (disable canonicalize-q-implies))))
  (defthm q-implies-of-self
    (equal (q-implies x x) t)
    :hints (("Goal" :in-theory (disable canonicalize-q-implies))))
  (local (in-theory (disable q-implies)))
  (local (defun test-q-implies
      (a b)
      (declare (xargs :guard t
          :guard-hints (("Goal" :in-theory (disable (force))))))
      (list (q-implies a b)
        (q-implies a (q-not b))
        (q-implies (q-not b) a)
        (q-implies (q-not a) (q-not b))))))
other
(defsection q-or-c2
  :parents (ubdd-constructors)
  :short "@(call q-or-c2) constructs a UBDD representing @('(or x (not y))')."
  (defund q-or-c2-fn
    (x y)
    (declare (xargs :guard t))
    (cond ((atom y) (if y
          x
          t))
      ((atom x) (if x
          t
          (q-not y)))
      ((hons-equal x y) t)
      (t (qcons (q-or-c2-fn (car x) (car y))
          (q-or-c2-fn (cdr x) (cdr y))))))
  (add-bdd-fn q-or-c2-fn)
  (defun q-or-c2-macro-fn
    (x y)
    (declare (xargs :mode :program))
    (cond ((and (or (quotep x) (atom x)) (or (quotep y) (atom y))) `(q-or-c2-fn ,X ,Y))
      ((or (quotep y) (atom y)) `(mbe :logic (q-or-c2-fn ,X ,Y)
          :exec (let ((q-or-c2-y-do-not-use-elsewhere ,Y))
            (if (not q-or-c2-y-do-not-use-elsewhere)
              t
              (prog2$ (last-chance-wash-memory)
                (q-or-c2-fn ,X q-or-c2-y-do-not-use-elsewhere))))))
      (t `(mbe :logic (q-or-c2-fn ,X ,Y)
          :exec (let ((q-or-c2-x-do-not-use-elsewhere ,X))
            (if (eq q-or-c2-x-do-not-use-elsewhere t)
              t
              (prog2$ (last-chance-wash-memory)
                (q-or-c2-fn q-or-c2-x-do-not-use-elsewhere ,Y))))))))
  (defmacro q-or-c2 (x y) (q-or-c2-macro-fn x y))
  (add-macro-alias q-or-c2 q-or-c2-fn)
  (local (in-theory (enable q-or-c2)))
  (memoize 'q-or-c2 :condition '(and (consp x) (consp y)))
  (defthm ubddp-of-q-or-c2
    (implies (and (force (ubddp x)) (force (ubddp y)))
      (equal (ubddp (q-or-c2 x y)) t))
    :hints (("Goal" :in-theory (enable ubddp))))
  (defthm eval-bdd-of-q-or-c2
    (equal (eval-bdd (q-or-c2 x y) values)
      (implies (eval-bdd y values) (eval-bdd x values)))
    :hints (("Goal" :in-theory (e/d (eval-bdd) (canonicalize-q-not))
       :induct (q-binop-induct x y values)
       :expand (q-or-c2 x y))))
  (defthm canonicalize-q-or-c2
    (implies (and (force (ubddp x)) (force (ubddp y)))
      (equal (q-or-c2 x y) (q-ite y x t))))
  (add-to-ruleset canonicalize-to-q-ite
    '(canonicalize-q-or-c2))
  (defthm q-or-c2-of-t
    (and (equal (q-or-c2 t x) t) (equal (q-or-c2 x t) x))
    :hints (("Goal" :in-theory (disable canonicalize-q-or-c2))))
  (defthm q-or-c2-of-nil
    (and (equal (q-or-c2 nil x) (q-not x))
      (equal (q-or-c2 x nil) t))
    :hints (("Goal" :in-theory (e/d (q-not) (canonicalize-q-not canonicalize-q-or-c2)))))
  (local (in-theory (disable q-or-c2)))
  (local (defun test-q-or-c2
      (a b)
      (declare (xargs :guard t))
      (list (q-or-c2 a b)
        (q-or-c2 a (q-not b))
        (q-or-c2 (q-not a) b)
        (q-or-c2 (q-not a) (q-not b))))))
other
(defsection q-and-c1
  :parents (ubdd-constructors)
  :short "@(call q-and-c1) constructs a UBDD representing @('(and (not x) y)')."
  (defund q-and-c1-fn
    (x y)
    (declare (xargs :guard t))
    (cond ((atom x) (if x
          nil
          y))
      ((atom y) (if y
          (q-not x)
          nil))
      ((hons-equal x y) nil)
      (t (qcons (q-and-c1-fn (car x) (car y))
          (q-and-c1-fn (cdr x) (cdr y))))))
  (memoize 'q-and-c1-fn :condition '(and (consp x) (consp y)))
  (add-bdd-fn q-and-c1-fn)
  (defun q-and-c1-macro-fn
    (x y)
    (declare (xargs :mode :program))
    (cond ((and (or (quotep x) (atom x)) (or (quotep y) (atom y))) `(q-and-c1-fn ,X ,Y))
      ((or (quotep y) (atom y)) `(mbe :logic (q-and-c1-fn ,X ,Y)
          :exec (let ((q-and-c1-y-do-not-use-elsewhere ,Y))
            (if (not q-and-c1-y-do-not-use-elsewhere)
              nil
              (prog2$ (last-chance-wash-memory)
                (q-and-c1-fn ,X q-and-c1-y-do-not-use-elsewhere))))))
      (t `(mbe :logic (q-and-c1-fn ,X ,Y)
          :exec (let ((q-and-c1-x-do-not-use-elsewhere ,X))
            (if (eq t q-and-c1-x-do-not-use-elsewhere)
              nil
              (prog2$ (last-chance-wash-memory)
                (q-and-c1-fn q-and-c1-x-do-not-use-elsewhere ,Y))))))))
  (defmacro q-and-c1 (x y) (q-and-c1-macro-fn x y))
  (add-macro-alias q-and-c1 q-and-c1-fn)
  (local (in-theory (enable q-and-c1)))
  (defthm ubddp-of-q-and-c1
    (implies (and (force (ubddp x)) (force (ubddp y)))
      (equal (ubddp (q-and-c1 x y)) t))
    :hints (("Goal" :in-theory (enable ubddp))))
  (defthm eval-bdd-of-q-and-c1
    (equal (eval-bdd (q-and-c1 x y) values)
      (if (eval-bdd x values)
        nil
        (eval-bdd y values)))
    :hints (("Goal" :in-theory (e/d (eval-bdd) (canonicalize-q-not))
       :induct (q-binop-induct x y values)
       :expand (q-and-c1 x y))))
  (defthm canonicalize-q-and-c1
    (implies (and (force (ubddp x)) (force (ubddp y)))
      (equal (q-and-c1 x y) (q-ite x nil y))))
  (add-to-ruleset canonicalize-to-q-ite
    '(canonicalize-q-and-c1))
  (defthm q-and-c1-of-nil
    (and (equal (q-and-c1 nil x) x)
      (equal (q-and-c1 x nil) nil))
    :hints (("Goal" :in-theory (disable canonicalize-q-and-c1))))
  (defthm q-and-c1-of-t
    (and (equal (q-and-c1 t x) nil)
      (equal (q-and-c1 x t) (q-not x)))
    :hints (("Goal" :in-theory (e/d (q-not) (canonicalize-q-and-c1 canonicalize-q-not)))))
  (local (in-theory (disable q-and-c1)))
  (local (defun test-q-and-c1
      (a b)
      (declare (xargs :guard t))
      (list (q-and-c1 a b)
        (q-and-c1 a (q-not b))
        (q-and-c1 (q-not a) b)
        (q-and-c1 (q-not a) (q-not b))))))
other
(defsection q-and-c2
  :parents (ubdd-constructors)
  :short "@(call q-and-c2) constructs a UBDD representing @('(and x (not y))')."
  (defund q-and-c2-fn
    (x y)
    (declare (xargs :guard t))
    (cond ((atom x) (if x
          (q-not y)
          nil))
      ((atom y) (if y
          nil
          x))
      ((hons-equal x y) nil)
      (t (qcons (q-and-c2-fn (car x) (car y))
          (q-and-c2-fn (cdr x) (cdr y))))))
  (memoize 'q-and-c2-fn :condition '(and (consp x) (consp y)))
  (add-bdd-fn q-and-c2-fn)
  (defun q-and-c2-macro-fn
    (x y)
    (declare (xargs :mode :program))
    (cond ((and (or (quotep x) (atom x)) (or (quotep y) (atom y))) `(q-and-c2-fn ,X ,Y))
      ((or (quotep y) (atom y)) `(mbe :logic (q-and-c2-fn ,X ,Y)
          :exec (let ((q-and-c2-y-do-not-use-elsewhere ,Y))
            (if (eq t q-and-c2-y-do-not-use-elsewhere)
              nil
              (prog2$ (last-chance-wash-memory)
                (q-and-c2-fn ,X q-and-c2-y-do-not-use-elsewhere))))))
      (t `(mbe :logic (q-and-c2-fn ,X ,Y)
          :exec (let ((q-and-c2-x-do-not-use-elsewhere ,X))
            (if (not q-and-c2-x-do-not-use-elsewhere)
              nil
              (prog2$ (last-chance-wash-memory)
                (q-and-c2-fn q-and-c2-x-do-not-use-elsewhere ,Y))))))))
  (defmacro q-and-c2 (x y) (q-and-c2-macro-fn x y))
  (add-macro-alias q-and-c2 q-and-c2-fn)
  (local (in-theory (enable q-and-c2)))
  (defthm ubddp-of-q-and-c2
    (implies (and (force (ubddp x)) (force (ubddp y)))
      (equal (ubddp (q-and-c2 x y)) t))
    :hints (("Goal" :in-theory (enable ubddp))))
  (defthm eval-bdd-of-q-and-c2
    (equal (eval-bdd (q-and-c2 x y) values)
      (if (eval-bdd y values)
        nil
        (eval-bdd x values)))
    :hints (("Goal" :in-theory (e/d (eval-bdd) (canonicalize-q-not))
       :induct (q-binop-induct x y values)
       :expand (q-and-c2 x y))))
  (defthm canonicalize-q-and-c2
    (implies (and (force (ubddp x)) (force (ubddp y)))
      (equal (q-and-c2 x y) (q-ite y nil x))))
  (add-to-ruleset canonicalize-to-q-ite
    '(canonicalize-q-and-c2))
  (defthm q-and-c2-of-nil-left
    (equal (q-and-c2 nil x) nil)
    :hints (("Goal" :in-theory (disable (force)))))
  (defthm q-and-c2-of-nil-right-slow
    (equal (q-and-c2 x nil)
      (if (consp x)
        x
        (if x
          t
          nil))))
  (defthm q-and-c2-of-nil-right-aggressive
    (implies (force (ubddp x)) (equal (q-and-c2 x nil) x)))
  (defthm q-and-c2-of-t
    (and (equal (q-and-c2 t x) (q-not x))
      (equal (q-and-c2 x t) nil))
    :hints (("Goal" :in-theory (disable (force)))))
  (local (in-theory (disable q-and-c2)))
  (local (defun test-q-and-c2
      (a b)
      (declare (xargs :guard t
          :guard-hints (("Goal" :in-theory (disable (force))))))
      (list (q-and-c2 a b)
        (q-and-c2 a (q-not b))
        (q-and-c2 (q-not a) b)
        (q-and-c2 (q-not a) (q-not b))))))
other
(defsection q-iff
  :parents (ubdd-constructors)
  :short "@(call q-iff) constructs a UBDD representing an equality/iff-equivalence."
  :long "<p>In the logic, for instance,</p>

@({
  (q-iff x1 x2 x3 x4) = (q-and (q-binary-iff x1 x2)
                               (q-binary-iff x1 x3)
                               (q-binary-iff x1 x4))
})

<p>We do not see how to use short-circuiting to improve upon @('(q-binary-iff x
y)'), since the answer depends upon both inputs in all cases.  But when we
implement the multiple-input @('q-iff') macro, we can at least take advantage
of the short-circuiting provided by @(see q-and).  We also reorder the inputs
so that cheap ones come first, hoping that we can avoid evaluating expensive
arguments.</p>"
  (defund q-binary-iff
    (x y)
    (declare (xargs :guard t))
    (cond ((atom x) (if x
          y
          (q-not y)))
      ((atom y) (if y
          x
          (q-not x)))
      ((hons-equal x y) t)
      (t (qcons (q-binary-iff (car x) (car y))
          (q-binary-iff (cdr x) (cdr y))))))
  (memoize 'q-binary-iff
    :condition '(and (consp x) (consp y)))
  (add-bdd-fn q-binary-iff)
  (defun q-iff-macro-guts
    (a x)
    (declare (xargs :mode :program))
    (if (consp x)
      (cons `(q-binary-iff ,A ,(CAR X))
        (q-iff-macro-guts a (cdr x)))
      nil))
  (defun q-iff-macro-fn
    (args)
    (declare (xargs :mode :program))
    (if (equal (len args) 2)
      `(prog2$ (last-chance-wash-memory)
        (q-binary-iff ,(CAR ARGS) ,(CADR ARGS)))
      (mv-let (cheap expensive)
        (cheap-and-expensive-arguments args)
        (let ((reordered-args (append cheap expensive)))
          `(let ((a-for-q-iff-do-not-use-elsewhere ,(CAR REORDERED-ARGS)))
            (prog2$ (last-chance-wash-memory)
              (q-and . ,(Q-IFF-MACRO-GUTS 'A-FOR-Q-IFF-DO-NOT-USE-ELSEWHERE (CDR REORDERED-ARGS)))))))))
  (defmacro q-iff
    (a b &rest args)
    (declare (xargs :guard (true-listp args)))
    (q-iff-macro-fn (list* a b args)))
  (add-macro-alias q-iff q-binary-iff)
  (local (in-theory (enable q-iff)))
  (defthm ubddp-of-q-iff
    (implies (and (force (ubddp x)) (force (ubddp y)))
      (equal (ubddp (q-iff x y)) t))
    :hints (("Goal" :in-theory (enable ubddp))))
  (defthm eval-bdd-of-q-iff
    (equal (eval-bdd (q-iff x y) values)
      (iff (eval-bdd x values) (eval-bdd y values)))
    :hints (("Goal" :in-theory (e/d (eval-bdd) (canonicalize-q-not))
       :induct (q-binop-induct x y values)
       :expand (q-iff x y))))
  (defthm canonicalize-q-iff
    (implies (and (force (ubddp x)) (force (ubddp y)))
      (equal (q-iff x y) (q-ite x y (q-ite y nil t)))))
  (add-to-ruleset canonicalize-to-q-ite '(canonicalize-q-iff))
  (local (in-theory (disable q-iff)))
  (local (defun test-q-iff
      (a b c d)
      (declare (xargs :guard t
          :guard-hints (("Goal" :in-theory (disable (force))))))
      (list (q-iff a b)
        (q-iff a b c (q-not b))
        (q-iff (q-not a) (q-not b) c d)))))
other
(defsection q-nand
  :parents (ubdd-constructors)
  :short "@(call q-nand) constructs a UBDD representing the NAND of its arguments."
  :long "<p>For instance:</p>
@({
 (q-nand)         = nil
 (q-nand a)       = (q-not a)
 (q-nand a b ...) = (q-not (q-and a b ...))
})

@(def q-nand)"
  (defmacro q-nand (&rest args) `(q-not (q-and . ,ARGS))))
other
(defsection q-nor
  :parents (ubdd-constructors)
  :short "@(call q-nor) constructs a UBDD representing the NOR of its arguments."
  :long "<p>For instance:</p>
@({
 (q-nor)         = t
 (q-nor a)       = (q-not a)
 (q-nor a b ...) = (q-not (q-or a b ...))
})

@(def q-nor)"
  (defmacro q-nor (&rest args) `(q-not (q-or . ,ARGS))))
other
(defsection q-xor
  :parents (ubdd-constructors)
  :short "@(call q-xor) constructs a UBDD representing the exclusive OR of its
arguments."
  (defund 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))))))
  (memoize 'q-binary-xor
    :condition '(and (consp x) (consp y)))
  (add-bdd-fn q-binary-xor)
  (defun q-xor-macro-fn
    (args)
    (declare (xargs :guard (consp args)))
    (if (atom (cdr args))
      (car args)
      `(prog2$ (last-chance-wash-memory)
        (q-binary-xor ,(CAR ARGS) ,(Q-XOR-MACRO-FN (CDR ARGS))))))
  (defmacro q-xor
    (a b &rest args)
    (q-xor-macro-fn (cons a (cons b args))))
  (add-macro-alias q-xor q-binary-xor)
  (add-binop q-xor q-binary-xor)
  (local (in-theory (enable q-xor)))
  (defthm ubddp-of-q-xor
    (implies (and (force (ubddp x)) (force (ubddp y)))
      (equal (ubddp (q-xor x y)) t))
    :hints (("Goal" :in-theory (enable ubddp))))
  (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)))
    :hints (("Goal" :in-theory (e/d (eval-bdd) (canonicalize-q-not))
       :induct (q-binop-induct x y values)
       :expand (q-xor x y))))
  (defthm q-xor-of-self
    (equal (q-xor x x) nil)
    :hints (("Goal" :in-theory (e/d (q-not) (equal-by-eval-bdds canonicalize-q-not)))))
  (defthm canonicalize-q-xor
    (implies (and (force (ubddp x)) (force (ubddp y)))
      (equal (q-xor x y) (q-ite x (q-not y) y))))
  (add-to-ruleset canonicalize-to-q-ite '(canonicalize-q-xor)))
other
(defsection qv
  :parents (ubdd-constructors)
  :short "@(call qv) constructs a UBDD which evaluates to true exactly when the
@('i')th BDD variable is true."
  (defund qv
    (i)
    (declare (xargs :guard t))
    (if (posp i)
      (let ((prev (qv (1- i))))
        (hons prev prev))
      (hons t nil)))
  (memoize 'qv)
  (add-bdd-fn qv)
  (local (in-theory (enable qv)))
  (defthm ubddp-qv
    (ubddp (qv i))
    :hints (("goal" :in-theory (enable ubddp))))
  (defthm eval-bdd-of-qv-and-nil
    (not (eval-bdd (qv i) nil))
    :hints (("Goal" :in-theory (enable eval-bdd))))
  (defthm eval-bdd-of-qv
    (equal (eval-bdd (qv i) lst)
      (if (nth i lst)
        t
        nil))
    :hints (("Goal" :in-theory (enable eval-bdd))))
  (local (defun qvs-ind
      (i j)
      (if (or (zp i) (zp j))
        i
        (qvs-ind (1- i) (1- j)))))
  (defthm qvs-equal
    (equal (equal (qv i) (qv j)) (equal (nfix i) (nfix j)))
    :hints (("Goal" :induct (qvs-ind i j)))))
other
(defsection eval-bdd-list
  :parents (ubdds)
  :short "Apply @(see eval-bdd) to a list of UBDDs."
  :long "<p>The resulting list is @(see hons)ed together.</p>

<p>BOZO why do we hons the list, I suspect it makes no sense to do so...</p>"
  (defund eval-bdd-list
    (x values)
    (declare (xargs :guard t))
    (if (consp x)
      (hons (eval-bdd (car x) values)
        (eval-bdd-list (cdr x) values))
      nil))
  (local (in-theory (enable eval-bdd-list)))
  (defthm eval-bdd-list-when-not-consp
    (implies (not (consp x))
      (equal (eval-bdd-list x values) nil)))
  (defthm eval-bdd-list-of-cons
    (equal (eval-bdd-list (cons a x) values)
      (cons (eval-bdd a values) (eval-bdd-list x values))))
  (defthmd consp-eval-bdd-list
    (equal (consp (eval-bdd-list x env)) (consp x))))
other
(defsection q-compose
  :parents (ubdd-constructors)
  :short "@(call q-compose) composes the UBDD @('x') with the list of UBDDs
@('l')."
  :long "<p>BOZO document what this is doing. Is it like sexpr compose?</p>"
  (defund q-compose
    (x l)
    (declare (xargs :guard t))
    (cond ((atom x) x)
      ((atom l) (q-compose (cdr x) nil))
      ((hons-equal (car x) (cdr x)) (q-compose (car x) (cdr l)))
      (t (q-ite (car l)
          (q-compose (car x) (cdr l))
          (q-compose (cdr x) (cdr l))))))
  (add-bdd-fn q-compose)
  (local (in-theory (enable q-compose)))
  (defthm ubddp-of-q-compose
    (implies (and (force (ubddp x)) (force (ubdd-listp l)))
      (equal (ubddp (q-compose x l)) t))
    :hints (("Goal" :in-theory (enable ubddp)))))
other
(defsection q-compose-list
  :parents (ubdd-constructors)
  :short "@(call q-compose-list) composes each UBDD in @('xs') with the list of
UBDDs @('l'), i.e., it maps @(see q-compose) across @('xs')."
  (defund q-compose-list
    (xs l)
    (declare (xargs :guard t))
    (if (atom xs)
      nil
      (cons (q-compose (car xs) l) (q-compose-list (cdr xs) l))))
  (local (in-theory (enable q-compose-list)))
  (defthm q-compose-list-when-not-consp
    (implies (not (consp xs)) (equal (q-compose-list xs l) nil)))
  (defthm q-compose-list-of-cons
    (equal (q-compose-list (cons x xs) l)
      (cons (q-compose x l) (q-compose-list xs l))))
  (defthm ubdd-listp-of-q-compose-list
    (implies (and (force (ubdd-listp xs)) (force (ubdd-listp l)))
      (equal (ubdd-listp (q-compose-list xs l)) t))))
other
(defsection q-and-is-nil
  :parents (ubdd-constructors)
  :short "@(call q-and-is-nil) determines whether @('(q-and x y)') is
always false."
  :long "<p>You could ask the same question in other ways, say for instance</p>

@({
 (not (q-and x y))
})

<p>But @('q-and-is-nil') is especially efficient and doesn't need to construct
an intermediate UBDD.</p>"
  (defund q-and-is-nil
    (x y)
    (declare (xargs :guard t))
    (cond ((eq x t) (eq y nil))
      ((atom x) t)
      ((eq y t) nil)
      ((atom y) t)
      (t (and (q-and-is-nil (qcar x) (qcar y))
          (q-and-is-nil (qcdr x) (qcdr y))))))
  (memoize 'q-and-is-nil
    :condition '(and (consp x) (consp y)))
  (local (in-theory (enable q-and-is-nil)))
  (defthm q-and-is-nil-removal
    (implies (and (force (ubddp x)) (force (ubddp y)))
      (equal (q-and-is-nil x y) (not (q-and x y))))
    :hints (("Goal" :induct (q-and-is-nil x y)
       :in-theory (e/d (q-and ubddp) (canonicalize-q-and equal-by-eval-bdds))))))
other
(defsection q-and-is-nilc2
  :parents (ubdd-constructors)
  :short "@(call q-and-is-nilc2) determines whether @('(q-and x (q-not y))') is
always false."
  :long "<p>This is like @(see q-and-is-nil).</p>"
  (defund q-and-is-nilc2
    (x y)
    (declare (xargs :guard t))
    (cond ((eq x t) (eq y t))
      ((atom x) t)
      ((eq y t) t)
      ((atom y) nil)
      (t (and (q-and-is-nilc2 (qcar x) (qcar y))
          (q-and-is-nilc2 (qcdr x) (qcdr y))))))
  (local (in-theory (enable q-and-is-nilc2)))
  (defthm q-and-is-nilc2-removal
    (implies (and (force (ubddp x)) (force (ubddp y)))
      (equal (q-and-is-nilc2 x y) (not (q-and x (q-not y)))))
    :hints (("Goal" :induct (q-and-is-nilc2 x y)
       :in-theory (e/d (q-and-c2 q-and-is-nilc2 ubddp)
         (canonicalize-q-and-c2 equal-by-eval-bdds
           canonicalize-q-not))))))
q-is-atomicfunction
(defund q-is-atomic
  (x)
  (declare (xargs :guard t))
  (if (atom x)
    (if x
      t
      nil)
    'not-atomic))
q-not-is-atomicfunction
(defund q-not-is-atomic
  (x)
  (declare (xargs :guard t))
  (if (atom x)
    (not x)
    'not-atomic))
q-not-is-atomic-removaltheorem
(defthm q-not-is-atomic-removal
  (implies (ubddp x)
    (equal (q-not-is-atomic x) (q-is-atomic (q-not x))))
  :hints (("Goal" :in-theory (enable q-not-is-atomic q-is-atomic q-ite q-not ubddp))))
atom-fixother
(defabbrev atom-fix
  (y)
  (if (atom y)
    y
    'not-atomic))
q-ite-is-atomicfunction
(defund q-ite-is-atomic
  (x y z)
  (declare (xargs :guard t))
  (cond ((null x) (atom-fix z))
    ((atom x) (atom-fix y))
    (t (let ((y (if (hons-equal x y)
             t
             y)) (z (if (hons-equal x z)
              nil
              z)))
        (cond ((hons-equal y z) (atom-fix y))
          ((and (eq y t) (eq z nil)) (atom-fix x))
          ((and (eq y nil) (eq z t)) (q-not-is-atomic x))
          (t (let ((a (q-ite-is-atomic (car x) (qcar y) (qcar z))) (d (q-ite-is-atomic (cdr x) (qcdr y) (qcdr z))))
              (cond ((or (eq a 'not-atomic) (eq d 'not-atomic)) 'not-atomic)
                ((equal a d) a)
                (t 'not-atomic)))))))))
encapsulate
(encapsulate nil
  (local (defthm lemma
      (implies (ubddp x)
        (equal (consp x)
          (if (equal x t)
            nil
            (if (equal x nil)
              nil
              t))))
      :hints (("Goal" :in-theory (enable ubddp)))))
  (local (defthm consp-q-ite
      (implies (and (ubddp x) (ubddp y) (ubddp z))
        (equal (consp (q-ite x y z))
          (and (not (equal (q-ite x y z) t))
            (not (equal (q-ite x y z) nil)))))))
  (local (defthm ubddp-consp-rws
      (implies (and (ubddp x) (consp x))
        (and (ubddp (car x)) (ubddp (cdr x))))
      :hints (("Goal" :in-theory (enable ubddp)))))
  (with-output :off (prove warning)
    :gag-mode nil
    (defthm q-ite-is-atomic-removal
      (implies (and (ubddp x) (ubddp y) (ubddp z))
        (equal (q-ite-is-atomic x y z) (q-is-atomic (q-ite x y z))))
      :hints (("Goal" :induct (q-ite-is-atomic x y z)
         :in-theory (e/d (q-is-atomic (:induction q-ite-is-atomic))
           (canonicalize-q-not equal-by-eval-bdds
             equal-of-booleans-rewrite
             |(q-ite non-nil y z)|
             default-car
             default-cdr
             (:type-prescription booleanp)
             (:type-prescription ubddp)
             (:type-prescription q-ite-is-atomic)
             (:type-prescription q-ite-fn)
             (:type-prescription q-is-atomic)
             q-not
             not
             lemma))
         :expand ((:free (y z) (q-ite x y z)) (:free (y z) (q-ite t y z))
           (:free (y z) (q-ite nil y z))
           (:free (y z) (q-ite-is-atomic x y z))
           (:free (y z) (q-ite-is-atomic t y z))
           (:free (y z) (q-ite-is-atomic nil y z)))
         :do-not-induct t
         :do-not '(generalize fertilize eliminate-destructors))))))
q-buffunction
(defun q-buf (x) (declare (xargs :guard t)) x)
in-theory
(in-theory (disable* (:ruleset canonicalize-to-q-ite)))
q-and-itemacro
(defmacro q-and-ite (x y) `(q-and ,X ,Y))
q-or-itemacro
(defmacro q-or-ite (x y) `(q-or ,X ,Y))
q-not-itemacro
(defmacro q-not-ite (x) `(q-not ,X))
q-implies-itemacro
(defmacro q-implies-ite (x y) `(q-implies ,X ,Y))
q-or-c2-itemacro
(defmacro q-or-c2-ite (x y) `(q-or-c2 ,X ,Y))
q-and-c1-itemacro
(defmacro q-and-c1-ite (x y) `(q-and-c1 ,X ,Y))
q-and-c2-itemacro
(defmacro q-and-c2-ite (x y) `(q-and-c2 ,X ,Y))
q-iff-itemacro
(defmacro q-iff-ite (x y) `(q-iff ,X ,Y))
q-xor-itemacro
(defmacro q-xor-ite (x y) `(q-xor ,X ,Y))
other
(defsection q-sat
  :parents (ubdds)
  :short "@(call q-sat) finds a satisfying assignment for the UBDD @('x'), if
one exists."
  :long "<p>Assuming @('x') is a well-formed UBDD, the only time there isn't
a satisfying assignment is when @('x') represents the constant false function,
i.e., when @('x') is @('nil').  In any other case it's easy to construct some
list of values for which @(see eval-bdd) returns true.</p>

<p>BOZO naming.  This shouldn't start with @('q-') since it's constructing a
list of values instead of a UBDD.</p>"
  (defund q-sat
    (x)
    (declare (xargs :guard t))
    (if (atom x)
      nil
      (if (eq (cdr x) nil)
        (cons t (q-sat (car x)))
        (cons nil (q-sat (cdr x))))))
  (local (in-theory (enable q-sat)))
  (defthm q-sat-correct
    (implies (and (ubddp x) x) (eval-bdd x (q-sat x)))
    :hints (("Goal" :in-theory (enable ubddp eval-bdd)))))
other
(defsection bdd-sat-dfs
  :parents (ubdds)
  :short "@(call bdd-sat-dfs) finds a satisfying assignment for the UBDD @('x'), if
one exists.  It works even if @('x') is not a well-formed UBDD, but it might be
slow in that case."
  (defund bdd-sat-dfs
    (x)
    (declare (xargs :guard t))
    (if (atom x)
      nil
      (let* ((a (car x)) (d (cdr x)))
        (cond ((and (atom a) a) '(t))
          ((and (atom d) d) '(nil))
          (t (let ((rec1 (bdd-sat-dfs a)))
              (if rec1
                (cons t rec1)
                (let ((rec2 (bdd-sat-dfs d)))
                  (and rec2 (cons nil rec2))))))))))
  (local (in-theory (enable bdd-sat-dfs)))
  (defthmd bdd-sat-dfs-produces-satisfying-assign
    (implies (bdd-sat-dfs x) (eval-bdd x (bdd-sat-dfs x)))
    :hints (("Goal" :in-theory (enable eval-bdd))))
  (local (in-theory (enable bdd-sat-dfs-produces-satisfying-assign)))
  (defthmd bdd-sat-dfs-not-satisfying-when-nil
    (implies (and (consp x) (not (bdd-sat-dfs x)))
      (not (eval-bdd x vars)))
    :hints (("Goal" :in-theory (enable eval-bdd))))
  (local (in-theory (enable bdd-sat-dfs-not-satisfying-when-nil)))
  (defthm bdd-sat-dfs-correct
    (implies (eval-bdd x vars) (eval-bdd x (bdd-sat-dfs x)))
    :hints (("Goal" :in-theory (enable eval-bdd)))))
other
(defsection q-sat-any
  :parents (ubdds)
  :short "@(call q-sat-any) finds an assignment that satisfies at least one
UBDD in the list of UBDDs @('x')."
  :long "<p>BOZO naming.  This shouldn't start with @('q-') since it's
constructing a list of values instead of a UBDD.</p>"
  (defund q-sat-any
    (a)
    (declare (xargs :guard t))
    (if (atom a)
      nil
      (if (eq (car a) nil)
        (q-sat-any (cdr a))
        (q-sat (car a))))))
other
(defsection ubdd-fix
  :parents (ubdds)
  :short "@(call ubdd-fix) constructs a valid @(see ubddp) that is treated
identically to @('x') under @(see eval-bdd)."
  :long "<p>This fixes up the tips of @('x') to be Booleans and handles any
collapsing of @('(t . t)') and @('(nil . nil)') nodes.  It is occasionally
useful in theorems to avoid @(see ubddp) hypotheses.</p>"
  (defund ubdd-fix
    (x)
    (declare (xargs :guard t))
    (if (atom x)
      (if x
        t
        nil)
      (if (and (atom (car x)) (atom (cdr x)) (iff (car x) (cdr x)))
        (if (car x)
          t
          nil)
        (qcons (ubdd-fix (car x)) (ubdd-fix (cdr x))))))
  (local (in-theory (enable ubdd-fix)))
  (memoize 'ubdd-fix :condition '(consp x))
  (defthm ubddp-ubdd-fix
    (ubddp (ubdd-fix x))
    :hints (("Goal" :in-theory (enable ubddp))))
  (defthm eval-bdd-ubdd-fix
    (equal (eval-bdd (ubdd-fix x) env) (eval-bdd x env))
    :hints (("Goal" :in-theory (enable eval-bdd))))
  (defthm ubdd-fix-x-is-x
    (implies (ubddp x) (equal (ubdd-fix x) x))
    :hints (("Goal" :in-theory (enable ubddp)))))