		Search-engine friendly clone of the ACL2 documentation.

Balance

Balance!

Like observability-fix, but overwrites the original network instead of returning a new one.

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

Definitions and Theorems

Function: balance!

(defun balance! (aignet config)
 (declare (xargs :stobjs (aignet)))
 (declare (xargs :guard (balance-config-p config)))
 (let ((__function__ 'balance!))
   (declare (ignorable __function__))
   (b*
     (((local-stobjs aignet-tmp)
       (mv aignet aignet-tmp))
      (- (cw "Balance input: ")
         (print-aignet-levels aignet))
      (aignet-tmp (balance-core aignet aignet-tmp config))
      (aignet (aignet-prune-comb aignet-tmp aignet
                                 (balance-config->gatesimp config)))
      (- (cw "Balance output: ")
         (print-aignet-levels aignet)))
     (mv aignet aignet-tmp))))

Theorem: num-ins-of-balance!

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

Theorem: num-regs-of-balance!

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

Theorem: num-outs-of-balance!

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

Theorem: balance!-comb-equivalent

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

Theorem: balance!-of-balance-config-fix-config

(defthm balance!-of-balance-config-fix-config
  (equal (balance! aignet (balance-config-fix config))
         (balance! aignet config)))

Theorem: balance!-balance-config-equiv-congruence-on-config

(defthm balance!-balance-config-equiv-congruence-on-config
  (implies (balance-config-equiv config config-equiv)
           (equal (balance! aignet config)
                  (balance! aignet config-equiv)))
  :rule-classes :congruence)