• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
      • Gl
        • Term-level-reasoning
        • Glmc
        • Other-resources
        • Optimization
        • Reference
          • Def-gl-thm
          • Shape-specs
          • Symbolic-objects
          • Gl-aside
          • Def-gl-param-thm
          • Symbolic-arithmetic
          • Bfr
            • Pbfr-depends-on
            • Bfr-varname-p
            • Bfr-varname-fix
            • Bfr-to-param-space
            • Bfr-depends-on
            • Aig-var-fix
            • Bfr-reasoning
            • Bfr-andc2
            • Bfr-andc1
            • Bfr-unparam-env
            • Bfr-set-var
            • Bfr-nor
            • Bfr-nand
            • Bfr-mode
            • Bfr-equiv
            • Bfr-xor
            • Bfr-iff
            • Bfr-eval
            • Bfr-param-env
            • Bfr-lookup
            • Bfr-env-equiv
            • Bfr-and
            • Bfr-var
            • Bfr-or
              • Bfr-binary-or
              • Bfr-or-macro-exec-part
              • Bfr-or-macro-logic-part
            • Bfr-not
            • Bfr-ite
            • Bdd-mode-or-p-true
            • Aig-mode-or-p-true
            • Bfr-case
          • Def-gl-boolean-constraint
          • Gl-mbe
          • Bvec
          • Flex-bindings
          • Auto-bindings
          • Gl-interp
          • Gl-set-uninterpreted
          • Def-gl-clause-processor
          • Def-glcp-ctrex-rewrite
          • ACL2::always-equal
          • Gl-hint
          • Def-gl-rewrite
          • Def-gl-branch-merge
          • Gl-force-check
          • Gl-concretize
          • Gl-assert
          • Gl-param-thm
          • Gl-simplify-satlink-mode
          • Gl-satlink-mode
          • Gl-bdd-mode
          • Gl-aig-bddify-mode
          • Gl-fraig-satlink-mode
        • Debugging
        • Basic-tutorial
      • Esim
      • Vl2014
      • Sv
      • Fgl
      • Vwsim
      • Vl
      • X86isa
      • Svl
      • Rtl
    • Software-verification
    • Math
    • Testing-utilities
  • Bfr

Bfr-or

(bfr-or x1 x2 ...) constructs the OR of these BFRs.

Macro: bfr-or

(defmacro bfr-or (&rest args)
  (cons 'mbe
        (cons ':logic
              (cons (bfr-or-macro-logic-part args)
                    (cons ':exec
                          (cons (bfr-or-macro-exec-part args)
                                'nil))))))

Subtopics

Bfr-binary-or
Bfr-or-macro-exec-part
Bfr-or-macro-logic-part