• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Testing-utilities
  • Math
    • Arithmetic
    • Bit-vectors
      • Sparseint
      • Bitops
        • Bitops/merge
        • Bitops-compatibility
        • Bitops-books
        • Logbitp-reasoning
        • Bitops/signed-byte-p
        • Fast-part-select
        • Bitops/integer-length
        • Bitops/extra-defs
        • Install-bit
        • Trailing-0-count
        • Bitops/defaults
        • Logbitp-mismatch
        • Trailing-1-count
        • Bitops/rotate
        • Bitops/equal-by-logbitp
          • Open-logbitp-of-const-meta
          • Equal-by-logbitp
          • Equal-by-logbitp-hint
          • Equal-by-logbitp-hammer
        • Bitops/ash-bounds
        • Bitops/fast-logrev
        • Limited-shifts
        • Bitops/part-select
        • Bitops/parity
        • Bitops/saturate
        • Bitops/part-install
        • Bitops/logbitp-bounds
        • Bitops/ihsext-basics
        • Bitops/fast-rotate
        • Bitops/fast-logext
        • Bitops/ihs-extensions
      • Bv
      • Ihs
      • Rtl
    • Algebra

• Bitops/equal-by-logbitp
• Logbitp

Open-logbitp-of-const-meta

Rewrite terms like (logbitp foo 7) to (or (not (natp foo)) (member-equal foo '(0 1 2))).

This meta rule targets terms of the form

(logbitp term const)

where const is a quoted constant, typically a number. We know that such a term can only be true when term happens to be one of the bit positions that has a 1 bit set in const, so we can split into cases based on which bits of const are set.

Note that this rule basically is going to split into n cases, where n is the number of 1 bits in const! Because of this we keep it disabled. But if you see a logbitp term applied to a constant, you might want to consider enabling this rule.

Definitions and Theorems

Theorem: lbpc-ev-constraint-0

(defthm
 lbpc-ev-constraint-0
 (implies (and (consp x)
               (syntaxp (not (equal a ''nil)))
               (not (equal (car x) 'quote)))
          (equal (lbpc-ev x a)
                 (lbpc-ev (cons (car x)
                                (kwote-lst (lbpc-ev-lst (cdr x) a)))
                          nil))))

Theorem: lbpc-ev-constraint-1

(defthm lbpc-ev-constraint-1
        (implies (symbolp x)
                 (equal (lbpc-ev x a)
                        (and x (cdr (assoc-equal x a))))))

Theorem: lbpc-ev-constraint-2

(defthm lbpc-ev-constraint-2
        (implies (and (consp x) (equal (car x) 'quote))
                 (equal (lbpc-ev x a) (cadr x))))

Theorem: lbpc-ev-constraint-3

(defthm
     lbpc-ev-constraint-3
     (implies (and (consp x) (consp (car x)))
              (equal (lbpc-ev x a)
                     (lbpc-ev (caddr (car x))
                              (pairlis$ (cadr (car x))
                                        (lbpc-ev-lst (cdr x) a))))))

Theorem: lbpc-ev-constraint-4

(defthm lbpc-ev-constraint-4
        (implies (not (consp acl2::x-lst))
                 (equal (lbpc-ev-lst acl2::x-lst a)
                        nil)))

Theorem: lbpc-ev-constraint-5

(defthm lbpc-ev-constraint-5
        (implies (consp acl2::x-lst)
                 (equal (lbpc-ev-lst acl2::x-lst a)
                        (cons (lbpc-ev (car acl2::x-lst) a)
                              (lbpc-ev-lst (cdr acl2::x-lst) a)))))

Theorem: lbpc-ev-constraint-6

(defthm lbpc-ev-constraint-6
        (implies (and (not (consp x)) (not (symbolp x)))
                 (equal (lbpc-ev x a) nil)))

Theorem: lbpc-ev-constraint-7

(defthm lbpc-ev-constraint-7
        (implies (and (consp x)
                      (not (consp (car x)))
                      (not (symbolp (car x))))
                 (equal (lbpc-ev x a) nil)))

Theorem: lbpc-ev-constraint-8

(defthm lbpc-ev-constraint-8
        (implies (and (consp x) (equal (car x) 'logbitp))
                 (equal (lbpc-ev x a)
                        (logbitp (lbpc-ev (cadr x) a)
                                 (lbpc-ev (caddr x) a)))))

Theorem: lbpc-ev-constraint-9

(defthm lbpc-ev-constraint-9
        (implies (and (consp x) (equal (car x) 'not))
                 (equal (lbpc-ev x a)
                        (not (lbpc-ev (cadr x) a)))))

Theorem: lbpc-ev-constraint-10

(defthm lbpc-ev-constraint-10
        (implies (and (consp x) (equal (car x) 'if))
                 (equal (lbpc-ev x a)
                        (if (lbpc-ev (cadr x) a)
                            (lbpc-ev (caddr x) a)
                            (lbpc-ev (cadddr x) a)))))

Theorem: lbpc-ev-constraint-11

(defthm lbpc-ev-constraint-11
        (implies (and (consp x) (equal (car x) 'equal))
                 (equal (lbpc-ev x a)
                        (equal (lbpc-ev (cadr x) a)
                               (lbpc-ev (caddr x) a)))))

Theorem: lbpc-ev-constraint-12

(defthm lbpc-ev-constraint-12
        (implies (and (consp x) (equal (car x) 'natp))
                 (equal (lbpc-ev x a)
                        (natp (lbpc-ev (cadr x) a)))))

Theorem: lbpc-ev-constraint-13

(defthm lbpc-ev-constraint-13
        (implies (and (consp x) (equal (car x) 'zp))
                 (equal (lbpc-ev x a)
                        (zp (lbpc-ev (cadr x) a)))))

Theorem: lbpc-ev-constraint-14

(defthm lbpc-ev-constraint-14
        (implies (and (consp x)
                      (equal (car x) 'member-equal))
                 (equal (lbpc-ev x a)
                        (member-equal (lbpc-ev (cadr x) a)
                                      (lbpc-ev (caddr x) a)))))

Function: bits-between

(defun bits-between (n m x)
       (declare (xargs :guard (and (natp n)
                                   (natp m)
                                   (<= n m)
                                   (integerp x))))
       (let* ((n (lnfix n)) (m (lnfix m)))
             (cond ((mbe :logic (zp (- m n)) :exec (= m n))
                    nil)
                   ((logbitp n x)
                    (cons n (bits-between (+ n 1) m x)))
                   (t (bits-between (+ n 1) m x)))))

Function: enumerate-logbitps

(defun enumerate-logbitps (x)
       (declare (xargs :guard (integerp x)))
       (bits-between 0 (integer-length x) x))

Function: open-logbitp-of-const

(defun
 open-logbitp-of-const (term)
 (declare (xargs :guard (pseudo-termp term)))
 (case-match
  term
  (('logbitp x ('quote const . &) . &)
   (cond
    ((or (not (integerp const)) (= const 0))
     ''nil)
    ((= const -1) ''t)
    ((natp const)
     (cons
      'if
      (cons
       (cons 'natp (cons x 'nil))
       (cons
        (cons
         'if
         (cons
          (cons
           'member-equal
           (cons x
                 (cons (cons 'quote
                             (cons (enumerate-logbitps const) 'nil))
                       'nil)))
          '('t 'nil)))
        (cons (cons 'quote
                    (cons (logbitp 0 const) 'nil))
              'nil)))))
    (t
     (cons
      'if
      (cons
       (cons 'natp (cons x 'nil))
       (cons
        (cons
         'not
         (cons
          (cons
           'member-equal
           (cons
               x
               (cons (cons 'quote
                           (cons (enumerate-logbitps (lognot const))
                                 'nil))
                     'nil)))
          'nil))
        (cons (cons 'quote
                    (cons (logbitp 0 const) 'nil))
              'nil)))))))
  (& term)))

Theorem: open-logbitp-of-const-meta

(defthm open-logbitp-of-const-meta
        (equal (lbpc-ev x a)
               (lbpc-ev (open-logbitp-of-const x) a))
        :rule-classes ((:meta :trigger-fns (logbitp))))

Function: open-logbitp-of-const-lite

(defun
 open-logbitp-of-const-lite (term)
 (declare (xargs :guard (pseudo-termp term)))
 (case-match
  term
  (('logbitp x ('quote const . &) . &)
   (cond
    ((or (not (integerp const)) (= const 0))
     ''nil)
    ((= const -1) ''t)
    ((natp const)
     (let ((len (1- (integer-length const))))
          (if (equal const (ash 1 len))
              (if (= len 0)
                  (cons 'zp (cons x 'nil))
                  (cons 'equal
                        (cons x
                              (cons (cons 'quote (cons len 'nil))
                                    'nil))))
              term)))
    (t
     (let*
      ((const (lognot const))
       (len (1- (integer-length const))))
      (if
       (equal const (ash 1 len))
       (if
         (= len 0)
         (cons 'not
               (cons (cons 'zp (cons x 'nil)) 'nil))
         (cons 'not
               (cons (cons 'equal
                           (cons x
                                 (cons (cons 'quote (cons len 'nil))
                                       'nil)))
                     'nil)))
       term)))))
  (& term)))

Theorem: open-logbitp-of-const-lite-meta

(defthm open-logbitp-of-const-lite-meta
        (equal (lbpc-ev x a)
               (lbpc-ev (open-logbitp-of-const-lite x)
                        a))
        :rule-classes ((:meta :trigger-fns (logbitp))))