		Search-engine friendly clone of the ACL2 documentation.

Ubdd-constructors

Cheap-and-expensive-arguments

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.

Definitions and Theorems

Function: cheap-and-expensive-arguments-aux

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

Function: cheap-and-expensive-arguments

(defun cheap-and-expensive-arguments (x)
       (mv-let (cheap expensive)
               (cheap-and-expensive-arguments-aux x nil nil)
               (mv (reverse cheap)
                   (reverse expensive))))