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

(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)))))

**Function: **

(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)))))