• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
    • Math
      • 100-theorems
      • Arithmetic
      • Bit-vectors
        • Sparseint
        • Bitops
        • Bv
        • Ihs
          • Logops-definitions
            • Logops-byte-functions
            • Defword
            • Defbytetype
            • Logext
            • Logrev
            • Loghead
            • Logops-bit-functions
            • Logtail
            • Logapp
            • Logsat
            • Binary--
            • Logcdr
            • Logcar
            • Logbit
            • Logextu
            • Logcons
            • Lshu
            • Logrpl
            • Ashu
            • Logmaskp
            • Lognotu
            • Logmask
            • Imod
            • Ifloor
            • Bfix
            • Bitmaskp
            • Logite
            • Expt2
            • Zbp
            • *logops-functions*
              • Word/bit-macros
              • Logops-definitions-theory
              • Logops-functions
              • Lbfix
              • Logextu-guard
              • Lshu-guard
              • Logtail-guard
              • Logrpl-guard
              • Logrev-guard
              • Lognotu-guard
              • Logmask-guard
              • Loghead-guard
              • Logext-guard
              • Logbit-guard
              • Logapp-guard
              • Ashu-guard
            • Math-lemmas
            • Ihs-theories
            • Ihs-init
            • Logops
          • Rtl
        • Algebra
      • Testing-utilities
    • Logops-definitions

    *logops-functions*

    A list of all functions considered to be part of the theory of logical operations on numbers.

    Definition: *logops-functions*

    (defconst *logops-functions*
      '(binary-logior binary-logxor
                      binary-logand binary-logeqv lognand
                      lognor logandc1 logandc2 logorc1 logorc2
                      lognot logtest logbitp ash logcount
                      integer-length bitp signed-byte-p
                      unsigned-byte-p logcar$inline
                      logcdr$inline logcons$inline
                      logbit$inline logmask$inline
                      logmaskp loghead$inline logtail$inline
                      logapp logrpl logext logrev1
                      logrev$inline logsat lognotu$inline
                      logextu$inline ashu lshu bspp
                      bsp-size bsp-position rdb wrb rdb-test
                      rdb-field wrb-field b-not$inline
                      b-and$inline b-ior$inline b-xor$inline
                      b-eqv$inline b-nand$inline b-nor$inline
                      b-andc1$inline b-andc2$inline
                      b-orc1$inline b-orc2$inline))