		Search-engine friendly clone of the ACL2 documentation.

Constprop

Constprop-once

Signature
(constprop-once aignet gatesimp aignet2) → new-aignet2
Arguments: aignet — Input aignet.; gatesimp — Guard (gatesimp-p gatesimp).; aignet2 — New aignet -- will be emptied.

Definitions and Theorems

Function: constprop-once

(defun constprop-once (aignet gatesimp aignet2)
  (declare (xargs :stobjs (aignet aignet2)))
  (declare (xargs :guard (gatesimp-p gatesimp)))
  (declare (xargs :guard (and (equal (num-outs aignet) 1)
                              (equal (num-regs aignet) 0))))
  (let ((__function__ 'constprop-once))
    (declare (ignorable __function__))
    (b* (((mv out-lit aignet2)
          (aignet-lit-constprop (outnum->fanin 0 aignet)
                                aignet gatesimp aignet2)))
      (aignet-add-out out-lit aignet2))))

Theorem: stype-count-of-constprop-once

(defthm stype-count-of-constprop-once
  (b* ((?new-aignet2 (constprop-once 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-once-preserves-comb-equiv

(defthm constprop-once-preserves-comb-equiv
  (b* ((?new-aignet2 (constprop-once 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-once

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

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

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

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

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

Theorem: constprop-once-of-gatesimp-fix-gatesimp

(defthm constprop-once-of-gatesimp-fix-gatesimp
  (equal (constprop-once aignet (gatesimp-fix gatesimp)
                         aignet2)
         (constprop-once aignet gatesimp aignet2)))

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

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

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

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

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

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