• 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

Find-max-level

Signature

(find-max-level n max-idx curr-max levels) → max

Arguments

n — Guard (natp n).

max-idx — Guard (natp max-idx).

curr-max — Guard (natp curr-max).

Returns

max — Type (natp max).

Definitions and Theorems

Function: find-max-level

(defun find-max-level (n max-idx curr-max levels)
  (declare (xargs :stobjs (levels)))
  (declare (xargs :guard (and (natp n)
                              (natp max-idx)
                              (natp curr-max))))
  (declare (xargs :guard (and (<= max-idx (u32-length levels))
                              (<= n max-idx))))
  (let ((__function__ 'find-max-level))
    (declare (ignorable __function__))
    (b* (((when (mbe :logic (zp (- (nfix max-idx) (nfix n)))
                     :exec (eql max-idx n)))
          (lnfix curr-max))
         (next-max (max (lnfix curr-max)
                        (get-u32 n levels))))
      (find-max-level (1+ (lnfix n))
                      max-idx next-max levels))))

Theorem: natp-of-find-max-level

(defthm natp-of-find-max-level
  (b* ((max (find-max-level n max-idx curr-max levels)))
    (natp max))
  :rule-classes :type-prescription)

Theorem: find-max-level-of-nfix-n

(defthm find-max-level-of-nfix-n
  (equal (find-max-level (nfix n)
                         max-idx curr-max levels)
         (find-max-level n max-idx curr-max levels)))

Theorem: find-max-level-nat-equiv-congruence-on-n

(defthm find-max-level-nat-equiv-congruence-on-n
  (implies (nat-equiv n n-equiv)
           (equal (find-max-level n max-idx curr-max levels)
                  (find-max-level n-equiv max-idx curr-max levels)))
  :rule-classes :congruence)

Theorem: find-max-level-of-nfix-max-idx

(defthm find-max-level-of-nfix-max-idx
  (equal (find-max-level n (nfix max-idx)
                         curr-max levels)
         (find-max-level n max-idx curr-max levels)))

Theorem: find-max-level-nat-equiv-congruence-on-max-idx

(defthm find-max-level-nat-equiv-congruence-on-max-idx
  (implies (nat-equiv max-idx max-idx-equiv)
           (equal (find-max-level n max-idx curr-max levels)
                  (find-max-level n max-idx-equiv curr-max levels)))
  :rule-classes :congruence)

Theorem: find-max-level-of-nfix-curr-max

(defthm find-max-level-of-nfix-curr-max
  (equal (find-max-level n max-idx (nfix curr-max)
                         levels)
         (find-max-level n max-idx curr-max levels)))

Theorem: find-max-level-nat-equiv-congruence-on-curr-max

(defthm find-max-level-nat-equiv-congruence-on-curr-max
  (implies (nat-equiv curr-max curr-max-equiv)
           (equal (find-max-level n max-idx curr-max levels)
                  (find-max-level n max-idx curr-max-equiv levels)))
  :rule-classes :congruence)