• 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
  • Debugging
  • Projects
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Testing-utilities
  • Math

• Ubdd-constructors

Q-and-c2

(q-and-c2 x y) constructs a UBDD representing (and x (not y)).

Definitions and Theorems

Function: q-and-c2-fn

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

Function: q-and-c2-fn-memoize-condition

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

Function: q-and-c2-macro-fn

(defun
 q-and-c2-macro-fn (x y)
 (cond
  ((and (or (quotep x) (atom x))
        (or (quotep y) (atom y)))
   (cons 'q-and-c2-fn
         (cons x (cons y 'nil))))
  ((or (quotep y) (atom y))
   (cons
    'mbe
    (cons
     ':logic
     (cons
      (cons 'q-and-c2-fn
            (cons x (cons y 'nil)))
      (cons
       ':exec
       (cons
        (cons
         'let
         (cons
          (cons (cons 'q-and-c2-y-do-not-use-elsewhere
                      (cons y 'nil))
                'nil)
          (cons
           (cons
            'if
            (cons
             '(eq t q-and-c2-y-do-not-use-elsewhere)
             (cons
              'nil
              (cons
               (cons
                'prog2$
                (cons
                 '(last-chance-wash-memory)
                 (cons
                  (cons 'q-and-c2-fn
                        (cons x '(q-and-c2-y-do-not-use-elsewhere)))
                  'nil)))
               'nil))))
           'nil)))
        'nil))))))
  (t
   (cons
    'mbe
    (cons
     ':logic
     (cons
      (cons 'q-and-c2-fn
            (cons x (cons y 'nil)))
      (cons
       ':exec
       (cons
        (cons
         'let
         (cons
          (cons (cons 'q-and-c2-x-do-not-use-elsewhere
                      (cons x 'nil))
                'nil)
          (cons
           (cons
            'if
            (cons
             '(not q-and-c2-x-do-not-use-elsewhere)
             (cons
              'nil
              (cons
               (cons
                'prog2$
                (cons
                  '(last-chance-wash-memory)
                  (cons (cons 'q-and-c2-fn
                              (cons 'q-and-c2-x-do-not-use-elsewhere
                                    (cons y 'nil)))
                        'nil)))
               'nil))))
           'nil)))
        'nil))))))))

Theorem: ubddp-of-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)))

Theorem: eval-bdd-of-q-and-c2

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

Theorem: canonicalize-q-and-c2

(defthm canonicalize-q-and-c2
        (implies (and (force (ubddp x))
                      (force (ubddp y)))
                 (equal (q-and-c2 x y) (q-ite y nil x))))

Theorem: q-and-c2-of-nil-left

(defthm q-and-c2-of-nil-left
        (equal (q-and-c2 nil x) nil))

Theorem: q-and-c2-of-nil-right-slow

(defthm q-and-c2-of-nil-right-slow
        (equal (q-and-c2 x nil)
               (if (consp x) x (if x t nil))))

Theorem: q-and-c2-of-nil-right-aggressive

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

Theorem: q-and-c2-of-t

(defthm q-and-c2-of-t
        (and (equal (q-and-c2 t x) (q-not x))
             (equal (q-and-c2 x t) nil)))