• 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-floor-ss-aux
          • Bfr-integer-length-s1
          • Bfr-mod-ss-aux
          • Bfr-logapp-russ
          • Bfr-sign-abs-not-s
          • Bfr-ash-ss
          • Bfr-+-ss
          • Bfr-truncate-ss
          • Bfr-logapp-nus-aux
          • Bfr-ite-bss-fn-aux
          • Bfr-rem-ss
          • Bfr-mod-ss
          • Bfr-logbitp-n2v
          • Bfr-logapp-nus
          • Bfr-logapp-nss
          • Bfr-ite-bvv-fn-aux
          • Bfr-<-=-ss
          • Bfr-*-ss
          • Bfr-logxor-ss
          • Bfr-logior-ss
          • Bfr-logeqv-ss
          • Bfr-logand-ss
          • Bfr-ite-bvv-fn
          • Bfr-ite-bss-fn
          • Bfr-floor-ss
          • Bfr-expt-su
          • Bfr-logtail-ns
          • Bfr-loghead-nu
          • Bfr-loghead-ns
          • Bfr-logext-ns
          • Bfr-integer-length-s
          • Syntactically-true-p
          • Int-set-sign
          • Bfr-unary-minus-s
          • Bfr-lognot-s
          • Bfr-=-ss
          • Bfr-<-ss
          • Bfr-abs-s
          • Syntactically-zero-p
          • Bfr-=-uu
          • S-take
          • Integer-length-bound-s
          • Bfr-sign-s
          • Non-int-fix
          • Maybe-integer
          • All-nil
        • Bfr
        • 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$
    • Fgl
    • Removable-runes
    • 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

• Reference

Symbolic-arithmetic

Internal operations for computing on symbolic bit vectors.

Naming convention:

• B stands for a boolean variable.
• S stands for a signed bvec.
• U stands for an unsigned bvec.
• V stands for a generic bvec where signedness doesn't matter.
• N stands for a known natural constant.

For instance, bfr-ite-bss-fn has bss, indicating that it's for computing:

(ite Boolean Signed-Bvec Signed-Bvec)

Subtopics

Bfr-floor-ss-aux

Bfr-integer-length-s1

Bfr-mod-ss-aux

Bfr-logapp-russ

Bfr-sign-abs-not-s

Bfr-ash-ss

Bfr-+-ss

Bfr-truncate-ss

Bfr-logapp-nus-aux

Bfr-ite-bss-fn-aux

Bfr-rem-ss

Bfr-mod-ss

Bfr-logbitp-n2v

Bfr-logapp-nus

Bfr-logapp-nss

Bfr-ite-bvv-fn-aux

Bfr-<-=-ss

Bfr-*-ss

Bfr-logxor-ss

Bfr-logior-ss

Bfr-logeqv-ss

Bfr-logand-ss

Bfr-ite-bvv-fn

Bfr-ite-bss-fn

Bfr-floor-ss

Bfr-expt-su

Bfr-logtail-ns

Bfr-loghead-nu

Bfr-loghead-ns

Bfr-logext-ns

Bfr-integer-length-s

Syntactically-true-p

Int-set-sign

Change the sign bit of an integer to a new value.

Bfr-unary-minus-s

Bfr-lognot-s

Bfr-=-ss

Bfr-<-ss

Bfr-abs-s

Syntactically-zero-p

Bfr-=-uu

S-take

Integer-length-bound-s

Bfr-sign-s

Non-int-fix

Identity for non-integers; coerces any integers to nil.

Maybe-integer

All-nil