		Search-engine friendly clone of the ACL2 documentation.

Propagate

Candidates-for-propagation

Gather initial candidates for propagation.

Signature
(candidates-for-propagation x limits) → sigma
Arguments: x — Guard (vl-assignlist-p x).; limits — Guard (propagate-limits-p limits).
Returns: sigma — Binds each identifier (lhs) to its replacement (rhs).
Type (vl-sigma-p sigma), given (force (vl-assignlist-p x)).

We're basically just looking for assignments like:

assign identifier = expr;

These are just initial candidates, and later we'll eliminate some of them because propagation would be too hard.

Definitions and Theorems

Function: candidates-for-propagation

(defun candidates-for-propagation (x limits)
  (declare (xargs :guard (and (vl-assignlist-p x)
                              (propagate-limits-p limits))))
  (let ((__function__ 'candidates-for-propagation))
    (declare (ignorable __function__))
    (b* (((when (atom x)) nil)
         ((vl-assign x1) (car x))
         ((when (and (vl-idexpr-p x1.lvalue)
                     (propagate-expr-limits-okp x1.expr limits)))
          (cons (cons (vl-idexpr->name x1.lvalue)
                      x1.expr)
                (candidates-for-propagation (cdr x)
                                            limits))))
      (candidates-for-propagation (cdr x)
                                  limits))))

Theorem: vl-sigma-p-of-candidates-for-propagation

(defthm vl-sigma-p-of-candidates-for-propagation
  (implies (force (vl-assignlist-p x))
           (b* ((sigma (candidates-for-propagation x limits)))
             (vl-sigma-p sigma)))
  :rule-classes :rewrite)

Theorem: alistp-of-candidates-for-propagation

(defthm alistp-of-candidates-for-propagation
  (alistp (candidates-for-propagation x limits)))