• Top
  • Documentation
  • Books
  • Boolean-reasoning
    • Ipasir
    • Aignet
      • Base-api
      • Aignet-construction
      • Representation
      • Aignet-copy-init
      • Aignet-simplify-with-tracking
      • Aignet-simplify-marked-with-tracking
      • Aignet-cnf
      • Aignet-simplify-marked
      • Aignet-complete-copy
      • Aignet-transforms
        • Aignet-output-ranges
        • Aignet-comb-transforms
          • Fraig
          • Parametrize
          • Observability-fix
          • Constprop
          • Apply-m-assumption-n-output-output-transform-default
          • Balance
            • 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!
            • 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-<
          • Apply-n-output-comb-transform-default
          • Apply-comb-transform-default
          • Obs-constprop
          • Rewrite
          • Comb-transform
          • Abc-comb-simplify
          • Prune
          • Rewrite!
          • M-assumption-n-output-comb-transform->name
          • N-output-comb-transform->name
          • Comb-transform->name
          • N-output-comb-transformlist
          • M-assumption-n-output-comb-transformlist
          • Comb-transformlist
          • Apply-comb-transform
        • Aignet-m-assumption-n-output-transforms
        • Aignet-n-output-comb-transforms
      • Aignet-eval
      • Semantics
      • Aignet-read-aiger
      • Aignet-write-aiger
      • Aignet-abc-interface
      • Utilities
    • Aig
    • Satlink
    • Truth
    • Ubdds
    • Bdd
    • Faig
    • Bed
    • 4v
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Balance

Aignet-balance-outs

Signature

(aignet-balance-outs n config aignet mark 
                     copy refcounts levels aignet2 strash) 
 
  → 
(mv new-mark new-copy new-levels new-aignet2 new-strash)

Arguments

n — Guard (natp n).

config — Guard (balance-config-p config).

aignet — input.

mark — completed nodes.

copy — mapping from input to output.

refcounts — for input network.

levels — for output network.

aignet2 — output.

strash — for output network.

Definitions and Theorems

Function: aignet-balance-outs

(defun aignet-balance-outs (n config aignet mark
                              copy refcounts levels aignet2 strash)
 (declare
      (xargs :stobjs (aignet mark
                             copy refcounts levels aignet2 strash)))
 (declare (xargs :guard (and (natp n)
                             (balance-config-p config))))
 (declare
  (xargs
    :guard
    (and (<= n (num-outs aignet))
         (<= (num-fanins aignet)
             (lits-length copy))
         (non-exec (ec-call (aignet-copies-in-bounds copy aignet2)))
         (<= (num-fanins aignet)
             (bits-length mark))
         (<= (num-fanins aignet)
             (u32-length refcounts))
         (<= (num-fanins aignet2)
             (u32-length levels)))))
 (let ((__function__ 'aignet-balance-outs))
  (declare (ignorable __function__))
  (b* (((when (mbe :logic (zp (- (num-outs aignet) (nfix n)))
                   :exec (eql n (num-outs aignet))))
        (mv mark copy levels aignet2 strash))
       (- (and (>= (balance-config->verbosity-level config)
                   1)
               (b* (((local-stobjs u32arr) (mv blah u32arr))
                    (u32arr (resize-u32 (num-fanins aignet) u32arr))
                    ((mv supergate &)
                     (lit-collect-supergate
                          (outnum->fanin n aignet)
                          t nil
                          (balance-config->supergate-limit config)
                          nil u32arr aignet)))
                 (cw "Input supergate size: ~x0~%"
                     (len supergate))
                 (cw "Gate numbers: ~x0~%"
                     (count-gates-list supergate aignet))
                 (mv nil u32arr))))
       ((mv ?lit mark copy levels aignet2 strash)
        (aignet-balance-rec (lit-id (outnum->fanin n aignet))
                            config aignet mark
                            copy refcounts levels aignet2 strash))
       (- (and (>= (balance-config->verbosity-level config)
                   1)
               (b* (((local-stobjs u32arr) (mv blah u32arr))
                    (u32arr (resize-u32 (num-fanins aignet2)
                                        u32arr))
                    ((mv supergate &)
                     (lit-collect-supergate
                          lit t nil
                          (balance-config->supergate-limit config)
                          nil u32arr aignet2)))
                 (cw "Output supergate size: ~x0~%"
                     (len supergate))
                 (cw "Gate numbers: ~x0~%"
                     (count-gates-list supergate aignet2))
                 (mv nil u32arr)))))
    (aignet-balance-outs (1+ (lnfix n))
                         config aignet mark
                         copy refcounts levels aignet2 strash))))

Theorem: aignet-extension-p-of-aignet-balance-outs

(defthm aignet-extension-p-of-aignet-balance-outs
  (b* (((mv ?new-mark ?new-copy
            ?new-levels ?new-aignet2 ?new-strash)
        (aignet-balance-outs n config aignet mark
                             copy refcounts levels aignet2 strash)))
    (aignet-extension-p new-aignet2 aignet2)))

Theorem: aignet-copies-in-bounds-of-aignet-balance-outs

(defthm aignet-copies-in-bounds-of-aignet-balance-outs
  (b* (((mv ?new-mark ?new-copy
            ?new-levels ?new-aignet2 ?new-strash)
        (aignet-balance-outs n config aignet mark
                             copy refcounts levels aignet2 strash)))
    (implies (aignet-copies-in-bounds copy aignet2)
             (aignet-copies-in-bounds new-copy new-aignet2))))

Theorem: levels-length-of-aignet-balance-outs

(defthm levels-length-of-aignet-balance-outs
  (b* (((mv ?new-mark ?new-copy
            ?new-levels ?new-aignet2 ?new-strash)
        (aignet-balance-outs n config aignet mark
                             copy refcounts levels aignet2 strash)))
    (implies (and (<= (num-fanins aignet2) (len levels))
                  (aignet-copies-in-bounds copy aignet2))
             (< (fanin-count new-aignet2)
                (len new-levels))))
  :rule-classes :linear)

Theorem: mark-length-of-aignet-balance-outs

(defthm mark-length-of-aignet-balance-outs
  (b* (((mv ?new-mark ?new-copy
            ?new-levels ?new-aignet2 ?new-strash)
        (aignet-balance-outs n config aignet mark
                             copy refcounts levels aignet2 strash)))
    (implies (<= (num-fanins aignet) (len mark))
             (equal (len new-mark) (len mark)))))

Theorem: copy-length-of-aignet-balance-outs

(defthm copy-length-of-aignet-balance-outs
  (b* (((mv ?new-mark ?new-copy
            ?new-levels ?new-aignet2 ?new-strash)
        (aignet-balance-outs n config aignet mark
                             copy refcounts levels aignet2 strash)))
    (implies (<= (num-fanins aignet) (len copy))
             (equal (len new-copy) (len copy)))))

Theorem: marks-remain-set-of-aignet-balance-outs

(defthm marks-remain-set-of-aignet-balance-outs
  (b* (((mv ?new-mark ?new-copy
            ?new-levels ?new-aignet2 ?new-strash)
        (aignet-balance-outs n config aignet mark
                             copy refcounts levels aignet2 strash)))
    (implies (equal (nth m mark) 1)
             (equal (nth m new-mark) 1))))

Theorem: output-fanin-marked-of-aignet-balance-outs

(defthm output-fanin-marked-of-aignet-balance-outs
  (b* (((mv ?new-mark ?new-copy
            ?new-levels ?new-aignet2 ?new-strash)
        (aignet-balance-outs n config aignet mark
                             copy refcounts levels aignet2 strash)))
    (implies
         (and (<= (nfix n) (nfix m))
              (< (nfix m) (num-outs aignet)))
         (equal (nth (lit-id (fanin 0 (lookup-stype m :po aignet)))
                     new-mark)
                1))))

Theorem: aignet-output-fanins-marked-of-aignet-balance-outs

(defthm aignet-output-fanins-marked-of-aignet-balance-outs
  (b* (((mv ?new-mark ?new-copy
            ?new-levels ?new-aignet2 ?new-strash)
        (aignet-balance-outs n config aignet mark
                             copy refcounts levels aignet2 strash)))
    (implies (zp n)
             (aignet-output-fanins-marked new-mark aignet))))

Theorem: aignet-balance-outs-correct

(defthm aignet-balance-outs-correct
 (b* (((mv ?new-mark ?new-copy
           ?new-levels ?new-aignet2 ?new-strash)
       (aignet-balance-outs n config aignet mark
                            copy refcounts levels aignet2 strash)))
  (implies
      (and (marked-lit-copies-equiv
                mark copy aignet aignet2 invals regvals)
           (aignet-copies-in-bounds copy aignet2))
      (marked-lit-copies-equiv new-mark new-copy
                               aignet new-aignet2 invals regvals))))

Theorem: aignet-balance-outs-correct-all-evals

(defthm aignet-balance-outs-correct-all-evals
 (b* (((mv ?new-mark ?new-copy
           ?new-levels ?new-aignet2 ?new-strash)
       (aignet-balance-outs n config aignet mark
                            copy refcounts levels aignet2 strash)))
  (implies
   (and (marked-lit-copies-equiv-all-evals mark copy aignet aignet2)
        (aignet-copies-in-bounds copy aignet2))
   (marked-lit-copies-equiv-all-evals
        new-mark new-copy aignet new-aignet2))))

Theorem: stype-counts-of-aignet-balance-outs

(defthm stype-counts-of-aignet-balance-outs
  (b* (((mv ?new-mark ?new-copy
            ?new-levels ?new-aignet2 ?new-strash)
        (aignet-balance-outs n config aignet mark
                             copy refcounts levels aignet2 strash)))
    (implies (and (not (equal (stype-fix stype) (and-stype)))
                  (not (equal (stype-fix stype) (xor-stype))))
             (equal (stype-count stype new-aignet2)
                    (stype-count stype aignet2)))))

Theorem: aignet-balance-outs-of-nfix-n

(defthm aignet-balance-outs-of-nfix-n
 (equal (aignet-balance-outs (nfix n)
                             config aignet mark
                             copy refcounts levels aignet2 strash)
        (aignet-balance-outs n config aignet mark
                             copy refcounts levels aignet2 strash)))

Theorem: aignet-balance-outs-nat-equiv-congruence-on-n

(defthm aignet-balance-outs-nat-equiv-congruence-on-n
 (implies
   (nat-equiv n n-equiv)
   (equal
        (aignet-balance-outs n config aignet mark
                             copy refcounts levels aignet2 strash)
        (aignet-balance-outs n-equiv config aignet mark
                             copy refcounts levels aignet2 strash)))
 :rule-classes :congruence)

Theorem: aignet-balance-outs-of-balance-config-fix-config

(defthm aignet-balance-outs-of-balance-config-fix-config
 (equal (aignet-balance-outs n (balance-config-fix config)
                             aignet mark
                             copy refcounts levels aignet2 strash)
        (aignet-balance-outs n config aignet mark
                             copy refcounts levels aignet2 strash)))

Theorem: aignet-balance-outs-balance-config-equiv-congruence-on-config

(defthm
      aignet-balance-outs-balance-config-equiv-congruence-on-config
 (implies
   (balance-config-equiv config config-equiv)
   (equal
        (aignet-balance-outs n config aignet mark
                             copy refcounts levels aignet2 strash)
        (aignet-balance-outs n config-equiv aignet mark
                             copy refcounts levels aignet2 strash)))
 :rule-classes :congruence)