		Search-engine friendly clone of the ACL2 documentation.

Propagate

Propagate-expr-limits-okp

Check whether an expression is simple enough to propagate.

Signature
(propagate-expr-limits-okp x limits) → okp
Arguments: x — Guard (vl-expr-p x).; limits — Guard (propagate-limits-p limits).
Returns: okp — Type (booleanp okp).

Definitions and Theorems

Function: propagate-expr-limits-okp

(defun propagate-expr-limits-okp (x limits)
 (declare (xargs :guard (and (vl-expr-p x)
                             (propagate-limits-p limits))))
 (let ((__function__ 'propagate-expr-limits-okp))
  (declare (ignorable __function__))
  (b*
   (((propagate-limits limits) limits)
    ((unless limits.max-ops) t)
    (ops (vl-expr-ops x))
    (ops (set-difference-eq ops
                            '(:vl-bitselect :vl-partselect-colon))))
   (< (len ops) limits.max-ops))))

Theorem: booleanp-of-propagate-expr-limits-okp

(defthm booleanp-of-propagate-expr-limits-okp
  (b* ((okp (propagate-expr-limits-okp x limits)))
    (booleanp okp))
  :rule-classes :type-prescription)