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