		Search-engine friendly clone of the ACL2 documentation.

Lexorder

Fast-lexorder

Probably faster alternative to lexorder.

(fast-lexorder x y) is logically the same as ACL2's built-in (lexorder x y), but is probably usually faster because:

it rearranges the check as in fast-alphorder, and
it inlines the alphorder comparisons

This seems to give us a nice speedup:

(loop for elem in
  '( (1 . 2)                                  ;  1.238 vs 0.835
     ("foo" . "bar")                          ;  6.525 vs 4.833
     (foo . bar)                              ;  8.044 vs 5.860
     (foo . foo)                              ; 19.895 vs 0.983 !
     (#\a . #\b)                              ;  2.548 vs 1.140
     (("foo" . 1) . ("bar" . 1))              ;  9.661 vs 7.903
     ((:foo "foo" . 1) . (:foo "bar" . 1)))   ; 10.064 vs 8.456
  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 (lexorder a b)))
    (time (loop for i fixnum from 1 to 100000000
             do (fast-lexorder a b)))))

Definitions and Theorems

Function: fast-lexorder

(defun fast-lexorder (x y)
 (declare (xargs :guard t))
 (cond
    ((atom x)
     (if (atom y)
         (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)))
       t))
    ((atom y) nil)
    ((equal (car x) (car y))
     (fast-lexorder (cdr x) (cdr y)))
    (t (fast-lexorder (car x) (car y)))))

Theorem: fast-lexorder-is-lexorder

(defthm fast-lexorder-is-lexorder
  (equal (fast-lexorder x y)
         (lexorder x y)))