• 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
              • Aignet-parametrize-output-ranges
              • Aignet-parametrize-copy-set-regs
              • Aignet-parametrize-copy-set-ins
              • Aignet-parametrize-collect-bdd-order-aux
              • Aignet-parametrize-collect-bdd-order
              • Aignet-output-range-conjoin-ubdds
              • Aignet-output-range-collect-in/reg-ubdd-order
              • Aignet-finish-reg-ubdd-order
              • Aignet-finish-in-ubdd-order
              • Aignet-copy-dfs-output-range
              • Aignet-parametrize-m-n
              • Aignet-node-to-ubdd
              • Aignet-output-range-to-ubdds
              • Ubdd-to-aignet
              • Aignet-parametrize-copy-init
              • Parametrize-config
              • Parametrize-output-type
              • Ubdd-arr-to-param-space
              • Copy-lits-compose
              • Bitarr-range-1bit-indices
              • Bitarr-range-count
              • Aignet-count-ubdd-branches-wrap
              • Ubdd-to-aignet-memo-ok
              • Aignet-node-to-ubdd-build-cond
              • Copy-lits-compose-in-place
              • Bitarr-range-set
              • Ubdd/level
              • Ubdd-arr
                • Set-ubdd
                • Resize-ubdds
                • Get-ubdd
                • Ubdds-length
              • Ubdd-arr-max-depth
              • Aignet-count-ubdd-branches
              • Ubdd-negate-cond
              • Ubdd-apply-gate
              • Aignet-node-to-ubdd-short-circuit-cond
              • Bits->bools
              • Eval-ubddarr
              • Ubdd-to-aignet-memo
              • Parametrize-output-type-map
              • Lubdd-fix
            • Observability-fix
            • Constprop
            • Apply-m-assumption-n-output-output-transform-default
            • Balance
            • 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
  • Parametrize

Ubdd-arr

Abstract stobj: logically this just represents a list of |ACL2|::|UBDDP|s, but it is implemented as an array.

This is a simple abstract stobj array, introduced by def-1d-arr.

Definition: ubdd-arr

(defabsstobj ubdd-arr
  :foundation ubdd-arr$c
  :recognizer (ubdd-arrp :exec ubdd-arr$cp
                         :logic ubdd-arr$ap)
  :creator (create-ubdd-arr :exec create-ubdd-arr$c
                            :logic create-ubdd-arr$a)
  :corr-fn ubdd-arr$corr
  :exports ((ubdds-length :exec ubdds$c-length
                          :logic ubdds$a-length)
            (get-ubdd :exec ubdds$ci
                      :logic ubdds$ai)
            (set-ubdd :exec update-ubdds$ci
                      :logic update-ubdds$ai)
            (resize-ubdds :exec resize-ubdds$c
                          :logic resize-ubdds$a)))

Subtopics

Set-ubdd
Modify the nth element of the ubdd-arr array.
Resize-ubdds
Change the length of the ubdd-arr array.
Get-ubdd
Read the nth element of the ubdd-arr array.
Ubdds-length
Get the length of the ubdd-arr array.