• 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-nxsts

Signature

(aignet-balance-nxsts 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-nxsts

(defun aignet-balance-nxsts (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-regs 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-nxsts))
   (declare (ignorable __function__))
   (b* (((when (mbe :logic (zp (- (num-regs aignet) (nfix n)))
                    :exec (eql n (num-regs aignet))))
         (mv mark copy levels aignet2 strash))
        ((mv ?lit mark copy levels aignet2 strash)
         (aignet-balance-rec (lit-id (regnum->nxst n aignet))
                             config aignet mark
                             copy refcounts levels aignet2 strash)))
     (aignet-balance-nxsts (1+ (lnfix n))
                           config aignet mark
                           copy refcounts levels aignet2 strash))))

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

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

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

(defthm aignet-copies-in-bounds-of-aignet-balance-nxsts
 (b* (((mv ?new-mark ?new-copy
           ?new-levels ?new-aignet2 ?new-strash)
       (aignet-balance-nxsts 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-nxsts

(defthm levels-length-of-aignet-balance-nxsts
 (b* (((mv ?new-mark ?new-copy
           ?new-levels ?new-aignet2 ?new-strash)
       (aignet-balance-nxsts 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-nxsts

(defthm mark-length-of-aignet-balance-nxsts
 (b* (((mv ?new-mark ?new-copy
           ?new-levels ?new-aignet2 ?new-strash)
       (aignet-balance-nxsts 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-nxsts

(defthm copy-length-of-aignet-balance-nxsts
 (b* (((mv ?new-mark ?new-copy
           ?new-levels ?new-aignet2 ?new-strash)
       (aignet-balance-nxsts 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-nxsts

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

Theorem: aignet-output-fanins-marked-preserved-of-aignet-balance-nxsts

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

Theorem: nxst-fanin-marked-of-aignet-balance-nxsts

(defthm nxst-fanin-marked-of-aignet-balance-nxsts
 (b* (((mv ?new-mark ?new-copy
           ?new-levels ?new-aignet2 ?new-strash)
       (aignet-balance-nxsts n config aignet mark
                             copy refcounts levels aignet2 strash)))
   (implies (and (<= (nfix n) (nfix m))
                 (< (nfix m) (num-regs aignet)))
            (equal (nth (lit-id (lookup-reg->nxst m aignet))
                        new-mark)
                   1))))

Theorem: aignet-nxst-fanins-marked-of-aignet-balance-nxsts

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

Theorem: aignet-balance-nxsts-correct

(defthm aignet-balance-nxsts-correct
 (b* (((mv ?new-mark ?new-copy
           ?new-levels ?new-aignet2 ?new-strash)
       (aignet-balance-nxsts 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-nxsts-correct-all-evals

(defthm aignet-balance-nxsts-correct-all-evals
 (b* (((mv ?new-mark ?new-copy
           ?new-levels ?new-aignet2 ?new-strash)
       (aignet-balance-nxsts 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-nxsts

(defthm stype-counts-of-aignet-balance-nxsts
 (b* (((mv ?new-mark ?new-copy
           ?new-levels ?new-aignet2 ?new-strash)
       (aignet-balance-nxsts 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-nxsts-of-nfix-n

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

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

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

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

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

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

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