		Search-engine friendly clone of the ACL2 documentation.

Propagate

Propagation-sigma

Determine what wires to use for one round of propagation.

Signature
(propagation-sigma x limits) → sigma
Arguments: x — Guard (vl-module-p x).; limits — Guard (propagate-limits-p limits).
Returns: sigma — Type (vl-sigma-p sigma), given (force (vl-module-p x)).

Definitions and Theorems

Function: propagation-sigma

(defun propagation-sigma (x limits)
 (declare (xargs :guard (and (vl-module-p x)
                             (propagate-limits-p limits))))
 (let ((__function__ 'propagation-sigma))
  (declare (ignorable __function__))
  (b* (((vl-module x) x)
       (candidates (candidates-for-propagation x.assigns limits))
       (too-hard (too-hard-to-propagate x))
       (candidates (remove-each-from-alist too-hard candidates))
       (must-wait
            (mergesort (vl-exprlist-names (alist-vals candidates))))
       (candidates (remove-each-from-alist must-wait candidates))
       (- (cw "  - Final candidates: ~&0~%"
              (mergesort (alist-keys candidates)))))
    candidates)))

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

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

Subtopics

Remove-each-from-alist: BOZO, terrible, inefficient.