• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
    • Gl
    • Witness-cp
    • Ccg
    • Install-not-normalized
    • Rewrite$
    • Fgl
      • Fgl-rewrite-rules
      • Fgl-function-mode
      • Fgl-object
      • Fgl-solving
      • Fgl-handling-if-then-elses
      • Fgl-getting-bits-from-objects
      • Fgl-primitive-and-meta-rules
      • Fgl-counterexamples
      • Fgl-interpreter-overview
      • Fgl-correctness-of-binding-free-variables
      • Fgl-debugging
      • Fgl-testbenches
      • Def-fgl-boolean-constraint
      • Fgl-stack
      • Fgl-rewrite-tracing
      • Def-fgl-param-thm
      • Def-fgl-thm
      • Fgl-fast-alist-support
      • Fgl-array-support
      • Advanced-equivalence-checking-with-fgl
      • Fgl-fty-support
      • Fgl-internals
        • Symbolic-arithmetic
          • Aabf-floor-ss-aux
          • Aabf-logapp-russ
          • Aabf-integer-length-s1
          • Aabf-mod-ss-aux
          • Aabf-ite-bss-fn-aux
          • Aabf-sign-abs-not-s
          • Aabf-ite-buu-fn-aux
          • Aabf-ash-ss
          • Aabf-<-=-ss
          • Aabf-+-ss
          • Aabf-truncate-ss
          • Aabf-rem-ss
          • Aabf-mod-ss
          • Aabf-logbitp-n2v
          • Aabf-ite-buu-fn
          • Aabf-ite-bss-fn
          • Aabf-expt-su
          • Aabf-*-ss
          • Aabf-logxor-ss
          • Aabf-logior-ss
          • Aabf-logeqv-ss
          • Aabf-logand-ss
          • Aabf-floor-ss
          • Aabf-logapp-nss-aux
          • Aabf-unary-minus-s
          • Aabf-signext-nss
          • Aabf-logapp-nss
          • Aabf-integer-length-s
          • Aabf-=-ss
          • Aabf-<-ss
          • Aabf-abs-s
          • Aabf-syntactically-zero-p
          • Aabf-scons
          • Aabf-logtail-ns
          • Aabf-loghead-ns
          • Aabf-logext-ns
          • Aabf-syntactically-false-p
          • Aabf-lognot-s
          • Int->aabflist
          • Aabf-ucons
          • Aabf-syntactically-true-p
          • Aabf-syntactically-signext-p
          • Aabf-syntactically-neg1-p
          • Aabf-sign-s
          • Aabf-integer-length-bound-s
          • Int-set-sign
          • Aabf-car
          • Aabf-first/rest/end
          • Non-int-fix
          • Maybe-integer
        • Bfr
        • Fgl-interpreter-state
    • 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

• Fgl-internals

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

Aabf-floor-ss-aux

Aabf-logapp-russ

Aabf-integer-length-s1

Aabf-mod-ss-aux

Aabf-ite-bss-fn-aux

Aabf-sign-abs-not-s

Aabf-ite-buu-fn-aux

Aabf-ash-ss

Aabf-<-=-ss

Aabf-+-ss

Aabf-truncate-ss

Aabf-rem-ss

Aabf-mod-ss

Aabf-logbitp-n2v

Aabf-ite-buu-fn

Aabf-ite-bss-fn

Aabf-expt-su

Aabf-*-ss

Aabf-logxor-ss

Aabf-logior-ss

Aabf-logeqv-ss

Aabf-logand-ss

Aabf-floor-ss

Aabf-logapp-nss-aux

Aabf-unary-minus-s

Aabf-signext-nss

Aabf-logapp-nss

Aabf-integer-length-s

Aabf-=-ss

Aabf-<-ss

Aabf-abs-s

Aabf-syntactically-zero-p

Aabf-scons

Aabf-logtail-ns

Aabf-loghead-ns

Aabf-logext-ns

Aabf-syntactically-false-p

Aabf-lognot-s

Int->aabflist

Aabf-ucons

Aabf-syntactically-true-p

Aabf-syntactically-signext-p

Aabf-syntactically-neg1-p

Aabf-sign-s

Aabf-integer-length-bound-s

Int-set-sign

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

Aabf-car

Aabf-first/rest/end

Non-int-fix

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

Maybe-integer