		Search-engine friendly clone of the ACL2 documentation.

Aignet-comb-transforms

Balance

Apply DAG-aware AND tree balancing to the network.

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

Note: This implementation is heavily based on the one in ABC, developed and maintained at Berkeley by Alan Mishchenko.

Settings for the transform can be tweaked using the config input, which is a balance-config object.

Definitions and Theorems

Function: balance

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

Theorem: num-ins-of-balance

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

Theorem: num-regs-of-balance

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

Theorem: num-outs-of-balance

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

Theorem: balance-comb-equivalent

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

Theorem: normalize-input-of-balance

(defthm normalize-input-of-balance
  (implies (syntaxp (not (equal aignet2 ''nil)))
           (equal (balance aignet aignet2 config)
                  (balance aignet nil config))))

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

(defthm balance-of-balance-config-fix-config
  (equal (balance aignet
                  aignet2 (balance-config-fix config))
         (balance aignet aignet2 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 aignet2 config)
                  (balance aignet aignet2 config-equiv)))
  :rule-classes :congruence)

Subtopics

Aignet-balance-find-xor-pairing-rec
Aignet-balance-find-pairing-rec
Aignet-balance-outs
Aignet-balance-nxsts
Aignet-balance-find-xor-pairing
Balance-config
Aignet-balance-build-superxor-rec
Aignet-balance-find-pairing
Aignet-balance-build-supergate-rec
Aignet-balance-build-supergate
Aignet-balance-build-superxor
Cancel-parity-lits
Find-max-level
Balance-core
Balance!: Like observability-fix, but overwrites the original network instead of returning a new one.
Aignet-update-node-level
Remove-duplicate-lits
Supergate-has-contradiction
Lit-in-bounds
Supergate-has-contradiction-top
Print-aignet-levels
Litp-for-levels
Lit-list-for-levels
Levels-sort-<