• Top
    • Documentation
    • Books
    • Recursion-and-induction
    • Boolean-reasoning
    • Debugging
    • Projects
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
    • Testing-utilities
    • Math
      • Arithmetic
      • Bit-vectors
        • Sparseint
          • Sparseint-impl
          • Sparseint-p
          • Sparseint-binary-bittest
          • Sparseint-concatenate
          • Sparseint-binary-bitop
          • Sparseint-bitite
          • Sparseint-fix
          • Sparseint$-binary-minus
          • Sparseint-trailing-1-count-from
          • Sparseint-trailing-0-count-from
          • Sparseint-equal
          • Sparseint-test-bitorc2
          • Sparseint-test-bitorc1
          • Sparseint-test-bitnand
          • Sparseint-test-bitandc2
          • Sparseint-test-bitandc1
          • Sparseint-test-bitand
          • Sparseint-rightshift
          • Sparseint-bitcount-from
          • Sparseint-test-bitxor
          • Sparseint-test-bitor
          • Sparseint-test-bitnor
          • Sparseint-test-biteqv
          • Sparseint-compare
          • Sparseint-binary-minus
          • Sparseint-sign-ext
          • Sparseint-plus
          • Sparseint-bitandc2
          • Sparseint-bitandc1
          • Sparseint-bitand
          • Sparseint$-leaf-bitlimit
            • Sparseint-bitxor
            • Sparseint-bitorc2
            • Sparseint-bitorc1
            • Sparseint-bitor
            • Sparseint-bitnor
            • Sparseint-bitnand
            • Sparseint-biteqv
            • Sparseint-ash
            • Sparseint-<
            • Sparseint-bit
            • Sparseint-trailing-1-count
            • Sparseint-trailing-0-count
            • Sparseint-unary-minus
            • Sparseint-length
            • Sparseint-bitnot
            • Sparseint-bitcount
            • Int-to-sparseint
            • Sparseint-val
          • Bitops
          • Bv
          • Ihs
          • Rtl
        • Algebra
    • Sparseint

    Sparseint$-leaf-bitlimit

    Limit on the size (in bits) of sparseint leaves.

    This constant sets a tradeoff between representation efficiency of a single element versus opportunities for structure sharing between multiple elements. If the bitlimit is small, then we can potentially share structure more granularly among objects. However, if it is so small that the bignums on the leaves are dwarfed in size by the conses used to create the tree nodes, then this is unlikely to be efficient.

    Absent empirical evidence, we currently set the limit to 256, which we think is likely to be the size of a tree node in most 64-bit Lisps (i.e., two conses, 128 bits each).

    We wrap the constant *sparseint$-leaf-bitlimit* in a macro so that if dereferencing that global variable becomes a performance consideration, we can change the macro to just return the value instead of the constant. We use a defconst in the first place to make it easy to experiment with different values by redefining the constant.