		Search-engine friendly clone of the ACL2 documentation.

Heap<

Heap<-with-hashes

Variant of heap< which uses pre-computed hashes.

Signature
(heap<-with-hashes x y hash-x hash-y) → *

Logically, this variant of heap< just ignores the hash-x and hash-y arguments, but in execution, these hash values are used instead of calculated new hashe values. This may be more efficient when used to avoid recalculating hashes.

For instance, instead of (and (heap< x y) (heap< y z)), one may do:

(let ((hash-x (hash x))
      (hash-y (hash y))
      (hash-z (hash z)))
  (and (heap< x y hash-x hash-y)
       (heap< y z hash-y hash-z)))

This performs just one call of (hash y) instead of two.

Definitions and Theorems

Function: heap<-with-hashes$inline

(defun heap<-with-hashes$inline (x y hash-x hash-y)
  (declare (type (unsigned-byte 32) hash-x)
           (type (unsigned-byte 32) hash-y)
           (xargs :type-prescription
                  (booleanp (heap<-with-hashes x y hash-x hash-y)))
           (optimize (speed 3) (safety 0)))
  (declare (xargs :guard (and (unsigned-byte-p 32 hash-x)
                              (unsigned-byte-p 32 hash-y)
                              (int= (hash x) hash-x)
                              (int= (hash y) hash-y))))
  (mbe :logic (or (< (hash x) (hash y))
                  (and (equal (hash x) (hash y))
                       (<< x y)))
       :exec (or (< hash-x hash-y)
                 (and (int= hash-x hash-y) (<< x y)))))