Sort arguments into those that we think are definitely cheap to evaluate versus those that may be expensive.
This is the same idea as in q-ite. Variables and quoted constants are cheap to evaluate, so in associative/commutative operations like q-and we prefer to evaluate them first.
(defun cheap-and-expensive-arguments-aux (x cheap expensive) (if (atom x) (mv cheap expensive) (if (or (quotep (car x)) (atom (car x))) (cheap-and-expensive-arguments-aux (cdr x) (cons (car x) cheap) expensive) (cheap-and-expensive-arguments-aux (cdr x) cheap (cons (car x) expensive)))))
(defun cheap-and-expensive-arguments (x) (mv-let (cheap expensive) (cheap-and-expensive-arguments-aux x nil nil) (mv (reverse cheap) (reverse expensive))))