• 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-and

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

In the logic,

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

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 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.

Definitions and Theorems

Function: q-binary-and

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

Function: q-and-macro-logic-part

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

Function: q-and-macro-exec-part

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

Function: q-and-macro-fn

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

Theorem: ubddp-of-q-and

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

Theorem: eval-bdd-of-q-and

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

Theorem: canonicalize-q-and

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

Theorem: q-and-of-nil

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

Theorem: q-and-of-t-slow

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

Theorem: q-and-of-t-aggressive

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

Theorem: q-and-symmetric

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

Function: q-binary-and-memoize-condition

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

Theorem: q-and-of-self-slow

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

Theorem: q-and-of-self-aggressive

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