		Search-engine friendly clone of the ACL2 documentation.

Alphorder

Fast-alphorder

Probably faster alternative to alphorder.

(fast-alphorder x y) is logically the same as ACL2's built-in alphorder, but it is probably usually faster on real set elements.

Conjecture: most "real" ACL2 objects are mainly built up from integers, symbols, and strings. That is, non-integer numbers and characters are probably somewhat rare.

ACL2's built-in alphorder first checks whether the elements are real or complex numbers, then characters, then finally strings or symbols. This order isn't great if the conjecture above is true. It seems especially unfortunate as real/rationalp and complex/complex-rationalp seem to be relatively expensive. For instance, in CCL the following loop:

(loop for a in
  '("foo" 3 #a 'foo (expt 2 80) 1/3 (complex 3 4))
   do (format t "---- ~a ------~%" a)
      (time (loop for i fixnum from 1 to 1000000000
               do (stringp a)))
      (time (loop for i fixnum from 1 to 1000000000
               do (integerp a)))
      (time (loop for i fixnum from 1 to 1000000000
               do (symbolp a)))
      (time (loop for i fixnum from 1 to 1000000000
               do (characterp a)))
      (time (loop for i fixnum from 1 to 1000000000
               do (real/rationalp a)))
      (time (loop for i fixnum from 1 to 1000000000
                do (complex/complex-rationalp a))))

Appears to indicate that:

characterp is the very fastest (~.7 seconds)
symbolp is the next fastest (~1 second)
integerp and stringp are the next fastest (~1.6 seconds)
complex/complex-rationalp is slower (~3.6 seconds)
real/rationalp is much slower (4-6 seconds seconds)

The fast-alphorder function just rearranges things so that we first check for integers, strings, and symbols, which optimizes for our expected data distribution and avoids these expensive checks. This seems to give us a nice speedup for our expected kinds of data:

(loop for elem in
  '( (1 . 2)                 ; 1.004 sec vs .769 sec
     ("foo" . "bar")         ; 6.03 sec vs. 4.72 sec
     (foo . bar)             ; 7.55 sec vs. 5.705 sec
     (foo . foo)             ; 19.65 sec vs. .87 sec
     (#\a . #\b) )           ; 2.276 sec vs 1.03 sec
  do
  (let ((a (car elem))
        (b (cdr elem)))
    (format t "---- ~a vs. ~a ------~%" a b)
    (time (loop for i fixnum from 1 to 100000000
             do (alphorder a b)))
    (time (loop for i fixnum from 1 to 100000000
             do (fast-alphorder a b)))))

Definitions and Theorems

Function: fast-alphorder

(defun fast-alphorder (x y)
 (declare (xargs :guard (and (atom x) (atom y))))
 (mbe
   :logic (alphorder x y)
   :exec (cond ((integerp x)
                (cond ((integerp y) (<= x y))
                      ((real/rationalp y) (<= x y))
                      (t t)))
               ((symbolp x)
                (if (symbolp y)
                    (or (eq x y) (not (symbol< y x)))
                  (not (or (integerp y)
                           (stringp y)
                           (characterp y)
                           (real/rationalp y)
                           (complex/complex-rationalp y)))))
               ((stringp x)
                (cond ((stringp y) (and (string<= x y) t))
                      ((integerp y) nil)
                      ((symbolp y) t)
                      (t (not (or (characterp y)
                                  (real/rationalp y)
                                  (complex/complex-rationalp y))))))
               ((characterp x)
                (cond ((characterp y)
                       (<= (char-code x) (char-code y)))
                      (t (not (or (integerp y)
                                  (real/rationalp y)
                                  (complex/complex-rationalp y))))))
               ((real/rationalp x)
                (cond ((integerp y) (<= x y))
                      ((real/rationalp y) (<= x y))
                      (t t)))
               ((real/rationalp y) nil)
               ((complex/complex-rationalp x)
                (cond ((complex/complex-rationalp y)
                       (or (< (realpart x) (realpart y))
                           (and (= (realpart x) (realpart y))
                                (<= (imagpart x) (imagpart y)))))
                      (t t)))
               ((or (symbolp y)
                    (stringp y)
                    (characterp y)
                    (complex/complex-rationalp y))
                nil)
               (t (bad-atom<= x y)))))