		Search-engine friendly clone of the ACL2 documentation.

Prune

Prune!

Like prune, but overwrites the original network instead of returning a new one.

Signature
(prune! aignet config) → new-aignet
Arguments: aignet — Input aignet -- will be replaced with transformation result.; config — Guard (prune-config-p config).

Definitions and Theorems

Function: prune!

(defun prune! (aignet config)
 (declare (xargs :stobjs (aignet)))
 (declare (xargs :guard (prune-config-p config)))
 (let ((__function__ 'prune!))
  (declare (ignorable __function__))
  (b* (((local-stobjs aignet-tmp)
        (mv aignet aignet-tmp))
       (aignet-tmp (aignet-raw-copy aignet aignet-tmp))
       (aignet (aignet-prune-comb aignet-tmp aignet
                                  (prune-config->gatesimp config))))
    (mv aignet aignet-tmp))))

Theorem: num-ins-of-prune!

(defthm num-ins-of-prune!
  (b* ((?new-aignet (prune! aignet config)))
    (equal (stype-count :pi new-aignet)
           (stype-count :pi aignet))))

Theorem: num-regs-of-prune!

(defthm num-regs-of-prune!
  (b* ((?new-aignet (prune! aignet config)))
    (equal (stype-count :reg new-aignet)
           (stype-count :reg aignet))))

Theorem: num-outs-of-prune!

(defthm num-outs-of-prune!
  (b* ((?new-aignet (prune! aignet config)))
    (equal (stype-count :po new-aignet)
           (stype-count :po aignet))))

Theorem: prune!-comb-equivalent

(defthm prune!-comb-equivalent
  (b* ((?new-aignet (prune! aignet config)))
    (comb-equiv new-aignet aignet)))