• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
      • 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-cp-ev
              • Bfr-eval-cp
              • Bfr-patterns
              • Bfr-reasoning-mode
              • Bfr-eval-patterns
            • 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-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
      • Witness-cp
      • Ccg
      • Install-not-normalized
      • Rewrite$
      • Removable-runes
      • Fgl
      • Efficiency
      • Rewrite-bounds
      • Bash
      • Def-dag-measure
      • Bdd
      • Remove-hyps
      • Contextual-rewriting
      • Simp
      • Rewrite$-hyps
      • Bash-term-to-dnf
      • Use-trivial-ancestors-check
      • Minimal-runes
      • Clause-processor-tools
      • Fn-is-body
      • Without-subsumption
      • Rewrite-equiv-hint
      • Def-bounds
      • Rewrite$-context
      • Try-gl-concls
      • Hint-utils
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
    • Math
    • Testing-utilities
  • Bfr

Bfr-reasoning

Clause processor for ACL2::witness-style BFR reasoning.

Tries to apply the bfr-eval-cp clause processor when goals are stable-under-simplificationp. Typical usage:

:hints ((bfr-reasoning [:or-hint t]))

Subtopics

Bfr-cp-ev
Basic evaluator for meta-reasoning about bfr-eval.
Bfr-eval-cp
The actual clause processor for bfr-reasoning.
Bfr-patterns
Patterns for recognizing functions that return BFRs.
Bfr-reasoning-mode
Turn bfr-reasoning on or off in the default-hints.
Bfr-eval-patterns
Patterns for recognizing bfr-eval calls.