		Search-engine friendly clone of the ACL2 documentation.

Constprop

Constprop-iter

Signature
(constprop-iter iters aignet gatesimp aignet2) → new-aignet2
Arguments: iters — Guard (posp iters).; aignet — input aignet.; gatesimp — Guard (gatesimp-p gatesimp).; aignet2 — New aignet -- will be emptied.

Definitions and Theorems

Function: constprop-iter

(defun constprop-iter (iters aignet gatesimp aignet2)
 (declare (xargs :stobjs (aignet aignet2)))
 (declare (xargs :guard (and (posp iters)
                             (gatesimp-p gatesimp))))
 (declare (xargs :guard (and (equal (num-outs aignet) 1)
                             (equal (num-regs aignet) 0))))
 (let ((__function__ 'constprop-iter))
  (declare (ignorable __function__))
  (b*
   (((when (eql (lposfix iters) 1))
     (time$ (constprop-once aignet gatesimp aignet2)
            :msg "   - constprop-once: ~st seconds, ~sa bytes.~%"))
    ((local-stobjs aignet-tmp)
     (mv aignet-tmp aignet2))
    (aignet-tmp (constprop-iter (1- (lposfix iters))
                                aignet gatesimp aignet-tmp))
    (- (cw "Constprop iteration ~x0:"
           (1- (lposfix iters)))
       (print-aignet-stats "" aignet-tmp))
    (aignet2
     (time$ (constprop-once aignet-tmp gatesimp aignet2)
            :msg "   - constprop-once: ~st seconds, ~sa bytes.~%")))
   (mv aignet-tmp aignet2))))

Theorem: stype-count-of-constprop-iter

(defthm stype-count-of-constprop-iter
 (b* ((?new-aignet2 (constprop-iter iters aignet gatesimp aignet2)))
   (and (equal (stype-count :pi new-aignet2)
               (stype-count :pi aignet))
        (equal (stype-count :reg new-aignet2)
               (stype-count :reg aignet))
        (equal (stype-count :po new-aignet2) 1)
        (equal (stype-count :nxst new-aignet2)
               0)
        (equal (stype-count :const new-aignet2)
               0))))

Theorem: constprop-iter-preserves-comb-equiv

(defthm constprop-iter-preserves-comb-equiv
 (b* ((?new-aignet2 (constprop-iter iters aignet gatesimp aignet2)))
   (implies (and (equal (stype-count :po aignet) 1)
                 (equal (stype-count :reg aignet) 0))
            (comb-equiv new-aignet2 aignet))))

Theorem: normalize-inputs-of-constprop-iter

(defthm normalize-inputs-of-constprop-iter
 (b* nil
   (implies
        (syntaxp (not (equal aignet2 ''nil)))
        (equal (constprop-iter iters aignet gatesimp aignet2)
               (let ((aignet2 nil))
                 (constprop-iter iters aignet gatesimp aignet2))))))

Theorem: constprop-iter-of-pos-fix-iters

(defthm constprop-iter-of-pos-fix-iters
  (equal (constprop-iter (pos-fix iters)
                         aignet gatesimp aignet2)
         (constprop-iter iters aignet gatesimp aignet2)))

Theorem: constprop-iter-pos-equiv-congruence-on-iters

(defthm constprop-iter-pos-equiv-congruence-on-iters
  (implies
       (pos-equiv iters iters-equiv)
       (equal (constprop-iter iters aignet gatesimp aignet2)
              (constprop-iter iters-equiv aignet gatesimp aignet2)))
  :rule-classes :congruence)

Theorem: constprop-iter-of-node-list-fix-aignet

(defthm constprop-iter-of-node-list-fix-aignet
  (equal (constprop-iter iters (node-list-fix aignet)
                         gatesimp aignet2)
         (constprop-iter iters aignet gatesimp aignet2)))

Theorem: constprop-iter-node-list-equiv-congruence-on-aignet

(defthm constprop-iter-node-list-equiv-congruence-on-aignet
  (implies
       (node-list-equiv aignet aignet-equiv)
       (equal (constprop-iter iters aignet gatesimp aignet2)
              (constprop-iter iters aignet-equiv gatesimp aignet2)))
  :rule-classes :congruence)

Theorem: constprop-iter-of-gatesimp-fix-gatesimp

(defthm constprop-iter-of-gatesimp-fix-gatesimp
  (equal (constprop-iter iters aignet (gatesimp-fix gatesimp)
                         aignet2)
         (constprop-iter iters aignet gatesimp aignet2)))

Theorem: constprop-iter-gatesimp-equiv-congruence-on-gatesimp

(defthm constprop-iter-gatesimp-equiv-congruence-on-gatesimp
  (implies
       (gatesimp-equiv gatesimp gatesimp-equiv)
       (equal (constprop-iter iters aignet gatesimp aignet2)
              (constprop-iter iters aignet gatesimp-equiv aignet2)))
  :rule-classes :congruence)

Theorem: constprop-iter-of-node-list-fix-aignet2

(defthm constprop-iter-of-node-list-fix-aignet2
  (equal (constprop-iter iters
                         aignet gatesimp (node-list-fix aignet2))
         (constprop-iter iters aignet gatesimp aignet2)))

Theorem: constprop-iter-node-list-equiv-congruence-on-aignet2

(defthm constprop-iter-node-list-equiv-congruence-on-aignet2
  (implies
       (node-list-equiv aignet2 aignet2-equiv)
       (equal (constprop-iter iters aignet gatesimp aignet2)
              (constprop-iter iters aignet gatesimp aignet2-equiv)))
  :rule-classes :congruence)