		Search-engine friendly clone of the ACL2 documentation.

Bfr-mode

Determine the current bfr mode we are using.

GL users should generally not use this.

(bfr-mode) is an attachable function which is typically attached to either bfr-aig or bfr-bdd. When it returns true, we are to use aigs, otherwise we use ubdds.

Definition: bfr-mode

(encapsulate ((bfr-mode nil t))
  (with-output :off summary (logic))
  (with-output :summary-off
               (:other-than acl2::redundant)
               (local (defun bfr-mode nil
                        (declare (ignorable))
                        nil))))

Definitions and Theorems

Function: bfr-aig

(defun bfr-aig nil
  (declare (xargs :guard t))
  t)

Function: bfr-bdd

(defun bfr-bdd nil
  (declare (xargs :guard t))
  nil)