		Search-engine friendly clone of the ACL2 documentation.

Constprop

Aignet-constprop-stats

Signature
(aignet-constprop-stats n constmarks litclasses aignet unmapped const input gate) → nothing
Arguments: n — Guard (natp n).; unmapped — Guard (natp unmapped).; const — Guard (natp const).; input — Guard (natp input).; gate — Guard (natp gate).

Definitions and Theorems

Function: aignet-constprop-stats

(defun aignet-constprop-stats (n constmarks litclasses
                                 aignet unmapped const input gate)
 (declare (xargs :stobjs (constmarks litclasses aignet)))
 (declare (xargs :guard (and (natp n)
                             (natp unmapped)
                             (natp const)
                             (natp input)
                             (natp gate))))
 (declare
    (xargs :guard (and (<= n (num-fanins aignet))
                       (<= (num-fanins aignet)
                           (lits-length litclasses))
                       (<= (num-fanins aignet)
                           (bits-length constmarks))
                       (ec-call (litclasses-orderedp litclasses)))))
 (let ((__function__ 'aignet-constprop-stats))
  (declare (ignorable __function__))
  (b*
   (((when (mbe :logic (zp (- (num-fanins aignet) (nfix n)))
                :exec (int= n (num-fanins aignet))))
     (cw
      "Constprop stats:~%Total inputs: ~x0 Unmapped: ~x1 Const: ~x2 Other input: ~x3 Gate: ~x4~%"
      (+ (num-ins aignet) (num-regs aignet))
      unmapped const input gate))
    ((unless (eql (id->type n aignet) (in-type)))
     (aignet-constprop-stats (1+ (lnfix n))
                             constmarks litclasses
                             aignet unmapped const input gate))
    (norm-lit (id-normal-form n constmarks litclasses))
    ((when (eql norm-lit (make-lit n 0)))
     (aignet-constprop-stats (1+ (lnfix n))
                             constmarks
                             litclasses aignet (1+ (lnfix unmapped))
                             const input gate))
    (type (id->type (lit->var norm-lit) aignet))
    ((when (eql type (const-type)))
     (aignet-constprop-stats (1+ (lnfix n))
                             constmarks litclasses
                             aignet unmapped (1+ (lnfix const))
                             input gate))
    ((when (eql type (in-type)))
     (aignet-constprop-stats
          (1+ (lnfix n))
          constmarks litclasses
          aignet unmapped const (1+ (lnfix input))
          gate)))
   (aignet-constprop-stats (1+ (lnfix n))
                           constmarks litclasses aignet unmapped
                           const input (1+ (lnfix gate))))))