• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • 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
        • Q-and-is-nil
        • Cheap-and-expensive-arguments
        • Q-compose-list
        • Q-compose
        • Qv
        • 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
  • Testing-utilities
  • Math

• Ubdd-constructors

Q-or

(q-or &rest args) constructs a UBDD representing the disjunction of its arguments.

In the logic,

(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))

In the execution, we use the same sort of optimization as in q-and.

Definitions and Theorems

Function: q-binary-or

(defun 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)))))

Function: q-or-macro-logic-part

(defun q-or-macro-logic-part (args)
       (cond ((atom args) nil)
             ((atom (cdr args)) (car args))
             (t (cons 'q-binary-or
                      (cons (car args)
                            (cons (q-or-macro-logic-part (cdr args))
                                  'nil))))))

Function: q-or-macro-exec-part

(defun
 q-or-macro-exec-part (args)
 (cond
  ((atom args) nil)
  ((atom (cdr args)) (car args))
  (t
   (cons
    'let
    (cons
     (cons (cons 'q-or-x-do-not-use-elsewhere
                 (cons (car args) 'nil))
           'nil)
     (cons
      (cons
       'if
       (cons
        '(eq t q-or-x-do-not-use-elsewhere)
        (cons
         't
         (cons
          (cons
           'prog2$
           (cons
            '(last-chance-wash-memory)
            (cons
                 (cons 'q-binary-or
                       (cons 'q-or-x-do-not-use-elsewhere
                             (cons (q-or-macro-exec-part (cdr args))
                                   'nil)))
                 'nil)))
          'nil))))
      'nil))))))

Function: q-or-macro-fn

(defun
 q-or-macro-fn (args)
 (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)))
      (cons
       'mbe
       (cons ':logic
             (cons (q-or-macro-logic-part reordered-args)
                   (cons ':exec
                         (cons (q-or-macro-exec-part reordered-args)
                               'nil)))))))))))

Theorem: ubddp-of-q-or

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

Theorem: eval-bdd-of-q-or

(defthm eval-bdd-of-q-or
        (equal (eval-bdd (q-or x y) values)
               (or (eval-bdd x values)
                   (eval-bdd y values))))

Theorem: canonicalize-q-or

(defthm canonicalize-q-or
        (implies (and (force (ubddp x))
                      (force (ubddp y)))
                 (equal (q-or x y) (q-ite x t y))))

Theorem: q-or-of-nil-slow

(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)))))

Theorem: q-or-of-nil-aggressive

(defthm q-or-of-nil-aggressive
        (implies (force (ubddp x))
                 (and (equal (q-or nil x) x)
                      (equal (q-or x nil) x))))

Theorem: q-or-of-t

(defthm q-or-of-t
        (and (equal (q-or t x) t)
             (equal (q-or x t) t)))

Theorem: q-or-symmetric

(defthm q-or-symmetric
        (equal (q-or x y) (q-or y x)))

Function: q-binary-or-memoize-condition

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

Theorem: q-or-of-self-slow

(defthm q-or-of-self-slow
        (equal (q-or x x)
               (if (consp x) x (if x t nil))))

Theorem: q-or-of-self-aggressive

(defthm q-or-of-self-aggressive
        (implies (force (ubddp x))
                 (equal (q-or x x) x)))