• 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
        • Def-gl-boolean-constraint
        • Gl-mbe
        • Bvec
          • Scdr
          • Bfr-list->s
          • Bfr-eval-list
          • Bfr-scons
          • Bfr-ucons
          • Bfr-list->u
          • Bfr-sterm
          • Bfr-snorm
          • Pbfr-list-depends-on
          • V2i
          • N2v
          • V2n
          • S-endp
          • I2v
          • First/rest/end
          • Bool->sign
        • 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

• Bvec

Bfr-list->u

Unsigned interpretation of a BFR list under some environment.

Signature

(bfr-list->u x env) → *

Arguments

x — BFR List to interpret as an unsigned number.

env — Environment to evaluate the BFRs under.

Definitions and Theorems

Function: bfr-list->u

(defun bfr-list->u (x env)
  (declare (xargs :guard t))
  (let ((__function__ 'bfr-list->u))
    (declare (ignorable __function__))
    (if (atom x)
        0
      (logcons (bool->bit (bfr-eval (car x) env))
               (bfr-list->u (cdr x) env)))))

Theorem: bfr-list->u-of-list-fix

(defthm bfr-list->u-of-list-fix
  (equal (bfr-list->u (list-fix x) env)
         (bfr-list->u x env)))

Theorem: bfr-list->u-type

(defthm bfr-list->u-type
  (natp (bfr-list->u x env))
  :rule-classes :type-prescription)

Theorem: bfr-list->u-of-set-non-dep

(defthm bfr-list->u-of-set-non-dep
  (implies
       (and (not (pbfr-list-depends-on k p x))
            (bfr-eval p env)
            (bfr-eval p (bfr-set-var k v env)))
       (equal (bfr-list->u x
                           (bfr-param-env p (bfr-set-var k v env)))
              (bfr-list->u x (bfr-param-env p env)))))