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

(q-iff a b &rest args) constructs a UBDD representing an equality/iff-equivalence.

In the logic, for instance,

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

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 q-and. We also reorder the inputs so that cheap ones come first, hoping that we can avoid evaluating expensive arguments.

Definitions and Theorems

Function: q-binary-iff

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

Function: q-binary-iff-memoize-condition

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

Function: q-iff-macro-guts

(defun q-iff-macro-guts (a x)
       (if (consp x)
           (cons (cons 'q-binary-iff
                       (cons a (cons (car x) 'nil)))
                 (q-iff-macro-guts a (cdr x)))
           nil))

Function: q-iff-macro-fn

(defun
 q-iff-macro-fn (args)
 (if
  (equal (len args) 2)
  (cons 'prog2$
        (cons '(last-chance-wash-memory)
              (cons (cons 'q-binary-iff
                          (cons (car args)
                                (cons (cadr args) 'nil)))
                    'nil)))
  (mv-let
   (cheap expensive)
   (cheap-and-expensive-arguments args)
   (let
    ((reordered-args (append cheap expensive)))
    (cons
     'let
     (cons
      (cons (cons 'a-for-q-iff-do-not-use-elsewhere
                  (cons (car reordered-args) 'nil))
            'nil)
      (cons
       (cons
        'prog2$
        (cons
         '(last-chance-wash-memory)
         (cons
           (cons 'q-and
                 (q-iff-macro-guts 'a-for-q-iff-do-not-use-elsewhere
                                   (cdr reordered-args)))
           'nil)))
       'nil)))))))

Theorem: ubddp-of-q-iff

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

Theorem: eval-bdd-of-q-iff

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

Theorem: canonicalize-q-iff

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